I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute E ng in ee ring   ( I J E CE )   Vo l.   7 ,   No .   4 A u g u s t   201 7 ,   p p .   2 1 9 2 ~ 2 2 0 5   I SS N:  2 0 8 8 - 8708 DOI : 1 0 . 1 1 5 9 1 / i j ec e . v7 i 4 . p p 2 1 9 2 - 2205          2192       J o ur na l ho m ep a g e h ttp : //ia e s jo u r n a l.c o m/o n lin e/in d ex . p h p /I JE C E   Funct io na Verifi ca tion o L a rg e - in tegers  C ir cu its  u sing  a    Co si m ula tion - ba sed Appro a ch       Nej m e dd i ne  Ali m i 1 ,   Yo un es  L a hb ib 2 ,   M o hs en  M a chho ut 4 ,   Ra ched  T o ur k i 5   1 F a c u lt y   o f   S c ien c e s o f   T u n is,   Un iv e rsit y   o f   T u n is  El   M a n a r,   2 0 9 2   El   M a n a T u n is,   T u n isia   2 Na ti o n a E n g in e e rin g   S c h o o l   o f   Ca rth a g e ,   Un iv e rsit y   o f   Ca rth a g e ,   2 0 3 5   C h a rg u ia II  T u n is,   T u n isia   1, 2, 4, 5 El e c tro n ics   a n d   M icro - El e c tr o n ics   L a b o ra to ry   (E.   µ.  E.   L ),   F a c u lt y   o f   S c ien c e s o f   M o n a stir,   Un i v e rsit y   o f   M o n a stir,   5 0 0 0   M o n a stir,   T u n isia       Art icle  I nfo     AB ST RAC T     A r ticle  his to r y:   R ec eiv ed   No v   2 8 ,   2 0 1 6   R ev i s ed   A p r   2 6 ,   2 0 1 7   A cc ep ted   Ma y   1 0 ,   2 0 1 7       Cr y p to g ra p h y   a n d   c o m p u tatio n a a lg e b ra   d e sig n a re   c o m p lex   s y st e m b a se d   o n   m o d u lar  a rit h m e ti c   a n d   b u il d   o n   m u lt i - lev e m o d u les   w h e re   b it - w id th   is  g e n e ra ll y   larg e th a n   6 4 - b it .   Be c a u se   o f   th e ir  p a rti c u larity ,   su c h   d e sig n p o se   a   re a c h a ll e n g e   f o v e ri f ica ti o n ,   i n   p a rt   b e c a u se   larg e - in teg e r‘s  f u n c ti o n a re   n o su p p o r ted   i n   a c tu a h a rd w a r e   d e sc rip ti o n   lan g u a g e (HD L s),   th e re f o re   li m it in g   th e   HD L   tes tb e n c h   u ti l i ty .   In   a n o t h e h a n d ,   h ig h - lev e v e rif ic a ti o n   a p p ro a c h   p r o v e d   it e f f icie n c y   in   th e   las d e c a d e   o v e HD tes tb e n c h   tec h n iq u e   b y   ra isin g   th e   latter  a a   h ig h e a b stra c t io n   lev e l.   In   t h is   w o rk ,   we   p ro p o se   a   h ig h - lev e p latf o rm   t o   v e rify   su c h   d e sig n s,  b y   lev e r a g in g   th e   c a p a b il it ies   o f   a   p o p u lar t o o l   (M a t lab /S im u li n k to   m e e th e   re q u ire m e n ts  o f   a   c y c le   a c c u ra te   v e rif i c a ti o n   w it h o u b i t - siz e   re strictio n a n d   in   m u lt i - lev e l   in sid e   th e   d e sig n   a rc h it e c tu re .   T h e   p ro p o se d   h ig h - lev e p l a tf o r m   is   a u g m e n ted   b y   a n   a ss e rti o n - b a se d   v e rif ica ti o n   to   c o m p lete   th e   v e rif ic a ti o n   c o v e ra g e .   T h e   p latf o r m   e x p e ri m e n tal  re su lt o f   th e   tes tca se   p ro v id e d   g o o d   e v id e n c e   o f   it s p e rf o r m a n c e   a n d   re - u sa b i li ty .   K ey w o r d :   Ass er tio n - b ased   v er i f icat io n   Co - s i m u lat io n   C r y p to g r ap h y   Har d w ar d escr ip tio n   lan g u ag e   Hig h - lev el  v er i f icatio n   L ar g e - i n te g er   Ma tlab /Si m u l in k     Co p y rig h ©   2017   In s t it u te o A d v a n c e d   E n g i n e e rin g   a n d   S c ien c e .     Al rig h ts  re se rv e d .   C o r r e s p o nd ing   A uth o r :   Nej m ed d in A l i m i,    E lectr o n ics an d   Mic r o - E lectr o n ics  L ab o r ato r y   ( E .   µ.   E .   L ) ,   Facu lt y   o f   Sc ien ce s   o f   Mo n a s t ir ,   Un iv er s it y   o f   Mo n as tir ,   Av e n u d l ' E n v ir o n n e m en -   5000   M o n asti r ,   T u n is ia.   E m ail:  n ej m ed d in e. ali m i @ f s t. u t m . tn       1.   I NT RO D UCT I O N   L ar g e - i n te g er   ar ith m etic  i s   s et  o f   o p er atio n s   li k ad d itio n ,   m u lt ip licatio n ,   m o d u lar   r ed u ctio n ,   etc   th at  in v o l v es   i n te g er s   lar g er   th a n   th n at iv w o r d   s ize  o f   t h g en er al  p u r p o s p r o ce s s o r s ,   t y p icall y ,   6 4 - b it.  Dep en d in g   o n   th tar g et  ap p li ca tio n   r eq u ir e m en t s ,   i n te g er   o p er an d s   m a y   h av e   1 6 3 - b it,  1 9 2   b it,  5 1 2 - b it,  1 0 2 4 - b it  o f   len g t h ,   an d   m o r e.   On p lace   w h er lar g in te g er s   ar u s ed   is   cr y p to g r ap h y ,   esp ec iall y   in   t h p u b lic - k e y   f a m il y   li k R S A   [ 1 ]   an d   E ll ip tic  C u r v C r y p to g r ap h y   [ 2 ] ,   [ 3 ] .   L ar g in te g er s   ar also   u s ed   in   co m p le x   r esear ch ,   h ig h   p er f o r m a n ce   c o m p u ti n g   ( HP C )   a n d   co m p u t atio n al  al g eb r a.   L ar g e   in teg er s   o p er atio n s   k n o w   a   co n tin u o u s   d ev elo p m e n i n   m at h e m a tical  al g o r ith m s   [4 - 6] .   Har d w ar e - b ased   i m p le m en tatio n s   o f   s u c h   alg o r ith m s   h a v p r o v ed   to   b m o r ef f icie n t h a n   eq u i v al en s o f t w ar e s   p r o g r a m s   i n   t er m s   o f   s p ee d   an d   r eso u r ce s   u s ag e.   T h is   is   m ai n l y   d u to   ex p lo r in g   n e w   d esi g n   ar c h itectu r e s   [7 - 12] .   Su ch   d esig n s   ar g e n er all y   w r itte n   i n   h ar d w ar d escr ip tio n   lan g u ag e s   ( HD L s ) .   To   v er if y   t h at  a   d esig n   w o r k s   as  in ten d ed ,   t w o   tec h n o lo g ie s   ar co m m o n l y   u s ed Si m u la tio n - b ased   v er if ica tio n   a n d   f o r m al  v er if i ca tio n .   T h s i m u latio n - b ased   v er if icat io n   is   t h tec h n iq u e   g en er all y   u s ed   f o r   co m p le x   d esi g n s .   Fo r m al  v er if icatio n ,   w h ic h   co n s is t s   in   m a th e m atica ll y   ch ec k i n g   t h f u n ctio n al   co r r ec tn es s   o f   th d esi g n ,   is   g e n er all y   u s e d   to   v er if y   s m al d esig n s   an d   co r n er   ca s es.  Ho w e v er   in   t h last   d ec ad e,   f o r m al  v er if ica tio n   to o ls   h a v s ee n   th eir   ca p ac ity   to   v er if y   m o r co m p lex   d esi g n s   i m p r o v ed   to   s o m ex te n t,  in   p ar t,  b ec au s o f   it s   co u p li n g   w it h   s i m u lat io n   ( d y n a m ic  f o r m al   v er if ica tio n )   a n d   th s tan d a r d izatio n   o f   s o m Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F u n ctio n a V erif ica tio n   o f La r g e - in teg ers   C ir cu its   u s in g   a   C o s imu la tio n - b a s ed   A p p r o a c h   ( N ejme d d in A limi )   2193   ass er tio n   lan g u ag e s .   T h g o al  w as  to   m a k a   co m p le m en ta r y   tec h n o lo g y   to   th e   s i m u late d - b ased   o n s o   t h at   th o v er all  v er if icat io n   m eth o d o lo g y   co u ld   b en h a n ce d .     R eg ar d in g   s i m u lat io n - b ased   v er if ica tio n ,   r u n n i n g   test b e n c h   i n   a n   HD L   s i m u lato r   is   th co m m o n   ap p r o ac h   to   v er if y   h ar d w ar e   d esig n s   an d   HD L   p ac k a g e s   ( e. g .   VHDL ,   Ver ilo g ,   etc . )   p r o v id r an g o f   f u n ctio n s   i n te n d ed   to   h elp   w r itin g   test b e n ch s .   B u t,  t o   th b est  o f   o u r   k n o w led g e ,   a m o n g   th o s p ac k a g es  as   w ell   as  f u n ct io n al  v er i f icatio n   f r a m e w o r k s   ( e. g .   Sp ec m a n ,   J o v e,   etc . ) ,   th er is   n o   d ed icate d   A p p licatio n   P r o g r am m i n g   I n ter f ac ( A P I )     s u p p o r t in g   lar g e - i n te g er s   o p er atio n s .   A   w o r k ar o u n d   co n s i s ts   o n   v er if y i n g   ag ain s eq u iv a len t   p r o g r a m   w r itte n   at   h i g h - le v el  la n g u ag e.   S u ch   p r o g r a m s   ar r u n   o n   s o f t w ar es  ca l led   C o m p u ter   A lg eb r S y s te m s   ( C A S)   t h at  s u p p o r ts   n o n - l i m i ted   p r ec is io n   lik e   M A P L E ,   M A T HE MA T I C A   a n d   th GM P   lib r ar y .   I n   ad d itio n   to   C A S ,   t h er ex i s t   a   n u m b er   o f   d o m ain - s p ec if i lib r ar ies  l ik e   C r y p to ++   an d   MI R A C L   t h at  s u p p le m e n tr a d itio n al  h i g h   l ev e p r o g r a m m i n g   la n g u a g es   w it h   lar g e - i n teg er   s u p p o r to   tar g et  s p ec if ic  d o m a in s   li k cr y p to g r ap h y .   A lt h o u g h   u s i n g   C A S   a n d     s p ec i f ic  lib r ar ies  to   v er if y   HDL   d e s ig n s   m a y   m ee t h f u n c tio n al  v er if icatio n   p u r p o s f o r   v er y   b asic  a n d   u n it - le v el  d esig n s ,   it  r e m ai n s   i n s u f f icie n f o r   m o r co m p le x   d esi g n s I n   f ac t b ec au s e   th v er if i ca t io n   f lo w   is   d is j o in ed   ( DUV   an d   C A S   ar n o r a n   s i m u lta n eo u s l y ) ,   t h v er i f ca tio n   an d   i n ter ac t io n   w it h   t h Des ig n   Un d er   Ver if ica tio n   ( DUV)   is   li m ited .   On   t h e   o th er   h an d ,   th e   lar g e - in te g er   d ata  to   b u s ed   as  s ti m u li   to   DUV   an d   C A S   h as  to   b co n s ta n t   an d   s to r ed   b ef o r eh an d .   T h er ef o r e,   g u id ed   test b en c h s   tec h n iq u es  w i th   d y n a m ic   u p d ated   s ti m u li   ca n n o t b ap p lied .     C o - s i m u lat in g   DUV  a n d   its   R ef er en ce   Mo d el  r eq u ir es a n   ef f icien t c o m m u n icatio n   b et w ee n   th h ig h - lev el  test b e n ch   a n d   th HD L   s i m u lato r .   I n   th is   co n tex t,  s o m w o r k s   h a v b ee n   d o n e.   Fo r   ex a m p le,   th e   co s i m u latio n   o f   VHD L   d esi g n s   an d   C - b ased   test b en c h   u s i n g   th e   Fo r eig n   L a n g u a g I n ter f ac ( FL I )   p r o v id ed   b y   Mo d elSi m   s i m u la to r   w a s   p r o p o s ed   in   [ 1 3 ] .   Sim i lar   p r o j ec ts   b ased   o n   FL I   an d /o r   P L I   ( f o r   Ver ilo g )   an d   w r itte n   i n   o th er   h ig h - le v el  la n g u a g es  ( e. g .   P y t h o n )   w er p r o p o s ed   in   [ 1 4 ]   an d   [ 1 5 ] .   Ho w e v er   b ec au s e   s u c h   lan g u a g es  ar ar ch itect u r lim ited   s ize,   lar g e - i n teg er   s u p p o r in   n o s u p p o r ted   n ativ el y .   I n   th o th er   h an d ,   f o r m al  v er if icatio n   tec h n iq u e s   f o r   lar g e - i n te g er   HD L   w er e   ap p lied     in   s i m p le  ca s es  i n     [ 1 6 ] ,   [ 1 7 ] .   Desp ite  th eir   p r o v ed   p er f o r m a n ce ,   t h o s f r a m e w o r k s   r e m ai n   i n s u f f icien to   v er if y   lar g e - in te g e r   HDL   d e s ig n s   o f   ce r tain   c o m p le x it y   i n   s tan d alo n e .   I n   a n o th er   h a n d ,   s o m e   w o r k s   o n   lar g e - i n teg er s   u s i n g   M atlab /Si m u li n k ,   t h p o w er f u p air   o f   n u m er ica co m p u ti n g   an d   s i m u la tio n   s o f t war es ,   h av b ee n   co n d u cted   in   t h d esig n   f ield .   As  ex a m p le s ,   in   [ 1 8 ] [ 2 0 ]   au th o r s   s p ee d ed   u p   h ar d w ar i m p le m en tatio n s   o f   cr y p to g r ap h ic  d esig n s   b y   m o d elli n g   th s c h e m es  i n   S i m u li n k   an d   g en er ati n g   s y n th e s izab le  HD L   u s i n g   d ed icate d   to o ls   lik HD L   co d er .   E x a m p le o f   w o r k i n g   ar o u n d   th s ize  r es tr ictio n   h as  b ee n   r ep o r ted   i n   [ 1 8 ] , w h er au t h o rs   d iv id ed   th lar g o p er an d s   in to   s m al l er   s ize   to   ta k ad v a n ta g e   o f   h ar d w ar e   DSP s   m u l tip lic atio n   ca p ab ilit ies   i n   t h tar g et  FP GA .   I n   t h s a m e   co n tex t,  i n   [ 1 9 ] ,   a u th o r s   u s ed   s p ec if ic  m u l tip licatio n   al g o r ith m   w i th   p r o p er ty   o f   s p litt i n g   u p   o p er an d s   in to   s m al s ize  w o r d s .   W h ile   in   [ 2 0 ] ,   au th o r s   b o u n d ed   th o p er an d   s izes  to   o r d in ar y   b it - le n g th   to   o p ti m ize  th e   HDL   co d g en er atio n   i n   o r d er   to   ac h ie v ef f icie n th r o u g h p u t.  I n   v er i f icatio n ,   Ma tlab   w as   s ep ar atel y   u s ed   to   v er if y   E C C   ( E llip tic  C u r v C r y p to g r ap h y )   d esi g n s   in    [ 2 1 ]   a nd   [ 2 2 ]   b u n o   d etai ls   on   t h e   ev al u atio n   p r o ce s s   or   th in ter f ac in g   w it h   t h HD L   d esi g n   w er g iv e n .   T h r ee   ch allen g e s   ar s till   to   t ak f o r   d esig n s   in v o lv in g   lar g e - in te g er s h o w   to   s u p p o r h ar d w ar e   d esig n   test b e n ch   w i th o u s ize  r estrictio n   Ho w   to   p er f o r m   v er if icatio n   f o r   co m p lex   d esi g n s   w h er o p er atio n s   r u n   at  d if f er en lev el s ,   an d   h o w   to   s et  t h v er i f icatio n   s tr u ct u r to   v er if y   th f u ll   d esig n ?    In   th i s   p ap er ,   w h ic h   is   r ev i s ed   an d   e x te n d ed   v er s io n   o f   t h w o r k   p r esen ted   i n   [ 2 3 ] ,   w tr y   to   d r a w   a   p ath   f o r   s o lu tio n   to   t h o s ch alle n g e s   b y   in tr o d u ci n g   h i g h - le v el   s i m u latio n - b ased   v er i f icatio n   p latf o r m   b ased   o n   Ma tlab   an d   Si m u li n k B esid es  g e n er atin g   s ti m u l an d   m o n ito r in g   t h v er if ica tio n   f lo w ,   lar g i n te g er s   tr an s ac ti o n s   an d   p r o ce s s i n g   ar s u p p o r t ed   wi t h i n   t h p r o p o s ed   p latf o r m .   T h p latf o r m   f ea t u r es  h i g h   lev e l   g e n er at io n   o f   te s tb en c h ,   a   cr o s s - le v el  an d   a   c y c le - ac c u r ate  v er if icatio n .   Fu r t h er m o r e,   Ma tlab s   s u p p o r f o r   lar g e - i n teg er ,   u s i n g   it s     Var i ab le  P r ec is io n   I n te g er   A r ith m etic  ( VP I )   p ac k ag e,   i s   e x p lo ited T o   co m p lete  t h v er i f icatio n   o f   g i v e n   d esig n ,   th c o n tr o l lo g ic  p ar o f   DUV  is   v er i f ied   f o r m all y   u s in g   t h s a m HD L   s i m u lato r .   T h r est  o f   th p ap er   is   o r g an is ed   as  f o llo w s ,   s ec tio n   2   d etails  t h p r o p o s ed   p latf o r m   w h er t h e   v er if ica tio n   s tr u ctu r e d ata  tr an s f o r m atio n   ac r o s s   s tag e s   an d   th p r o ce s s   o f   s ettin g s   a n d   co n tr o llin g   th e   p latf o r m   ar e   e x p lai n ed I n   s e ctio n   3 ,   d etailed   t e s tcase  is   g i v en   to   ill u s tr ate  th e   w o r k i n g   o f   t h p lat f o r m   f o llo w ed   b y   r es u lt s   an d   d is c u s s io n .   Fi n all y ,   co n clu s io n   w i t h   f u t u r w o r k s   e n d s   th p ap er .       2.   T H E   P RO P O SE P L A T F O RM     2 . 1 .   O v er v ie w   T h d esig n   m et h o d o lo g y   o f   t h p latf o r m   f o llo w s   t h e   Si m u l atio n - b ased   ap p r o ac h ,   w h er s ti m u l ar e   g en er ated ,   ap p lied   to   th D UV  an d   r esp o n s e s   ar co m p ar ed   to   th ex p ec ted   o n es.  T y p ical  v er i f icatio n   f r a m e w o r k   b ased   o n   h ig h   lev el  d esig n   lan g u ag i n cl u d es   s ti m u li  g e n er ato r R ef er en ce   m o d el   ( also   r ef er r ed   t o   as  Go ld en   Mo d el)   w h ic h   is   u s u a ll y   w r itte n   at   a   h ig h er   lev el   o f   ab s tr ac tio n a n d   co m p ar ato r .   W ab s tr ac th f u n ctio n a d escr ip tio n   o f   th p lat f o r m   i n to   th r ee   f lo w s ,   i.e . ,   co n tr o f lo w ,   d ata  f lo w   a n d   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 A u g u s 2 0 1 7     2 1 9 2     2 2 0 5   2194   v er if ica tio n   f lo w ,   a s   s h o w n   i n   Fi g u r e   1 .   T h C o n tr o f lo co n tr o ls   t h p r o ce s s   o f   v er if icatio n   t h r o u g h   th e   p latf o r m .   I f i x es  th s etti n g s i.e .   t h p ar a m eter s   o f   th e   b lo ck s   co n s tit u ti n g   t h p lat f o r m ,   d ela y   ti m es,   s a m p li n g   ti m es,  etc .   Data   f lo w   r ep r esen t s   t h tr an s f o r m atio n s   t h at  d ata  u n d er g o es ,   s tar tin g   f r o m   th e   g en er atio n   o f   lar g e - in te g er   o p er an d s ,   p ass i n g   t h r o u g h   t h in p u t   ad ap ter ,   th e   DUV,   th e   o u tp u ad ap ter   a n d ,   f i n all y ,   e n ter i n g   t h co m p ar i s o n /ch ec k i n g   b lo ck s .   T h th ir d   f lo w ,   Ver i f icatio n   f lo w ,   v er if ies   th f u n ct io n al  co r r ec tn ess   o f   t h DUV.   W ch o s to   b u ild   t h v er if icati o n   f lo w   ar o u n d   t w o   co m p le m en tar y   s i m u latio n - b ased   v er if icat io n   ap p r o ac h es:  test b e n ch   a n d   as s er tio n - b ased   v er if icatio n .   W g u id t h test b e n ch   v ia  a   v er if ica tio n   s tr u ctu r e   w it h   co n s id er atio n s   o f   a   co v er ag e   p l an .   W h e n   test b e n ch   is   la u n c h ed ,   o u tp u ts   o f   DUV   an d   r ef er en ce   m o d el  ar co m p ar ed .   R esu lts   ar th e n   tr an s f er r ed   to   Sco r eb o ar d   t o   b e   a n al y ze d .   W w r it e   ass er tio n s   i n   P r o p er ty   Sp ec i f i ca tio n   L an g u ag ( P S L )   [ 2 4 ] s tan d ar d   ass er tio n   la n g u a g e ,   i n s id t h DU an d   r ep r esen p r ec is d escr ip tio n   o f   th e   DUV s   b eh a v io r .   No te  th at   w c h o s P S L   f o r   p r o p er ty   d e s cr ip tio n   a s   it‗ s   i n   w id esp r ea d   u s in   i n d u s tr y   an d   co m p atib le  w it h   m a n y   h ar d w ar d escr ip tio n   lan g u a g es .   P SL   as s er tio n s   ar ch ec k ed   b y   t h HD L   s i m u lato r   d u r in g   th s i m u latio n .   T h ass er tio n s   v er i f icatio n   r esu lt s   ( p ass / f ail)   ar also   s en to   th s co r eb o ar d   to   b an al y ze d   a n d   n e w   s ti m u li   ar g en er ated   i n   th e   n e x te s t b en ch   ac co r d in g   to   th e   u p d ated   f u n c tio n al  co v er a g e .           Fig u r 1 .   Fu n c tio n al  De s cr ip ti o n   o f   th p lat f o r m .     2 . 2 .   T he  F un ct io na l V er if ica t io P ro ce s s   T h p u r p o s o f   th F u n ct i o n al‖  v er i f icatio n   p r o ce s s   is   to   v er if y   t h at  t h DUV  m atch es  it s   s p ec if icatio n .   T h is   p r o ce s s   s h o u ld   v er if y   t h at  th i m p le m e n ted   f u n ct io n s   b e h av co r r ec tl y .   T h v er if icat io n   tech n o lo g y   u s ed   i s   th s i m u lat io n - b ased   v er i f icatio n ,   m o r p r ec is el y   co s i m u latio n   b et w ee n   Ma tlab /Si m u l in k   an d   Mo d elSi m ,   an d   s i m u lated   ass er tio n s   wr itten   i n   P SL .   Glo b all y ,   w f o llo w ed   co v er ag e - d r iv e n   r an d o m - b ased   v er if icatio n   ap p r o ac h .     T h lev el  o f   v er if ica tio n   ca n   b o f   u n i t/ s u b - u n it  o r   co r es/b lo ck s   le v el  an d   t w o   s i m u latio n - b ased   v er i f ica tio n   tech n iq u e s   ar u s ed   j o in tl y ,   d ep en d in g   o n   t h p ar titi o n   o f   DUV  b ein g   v er i f ied .   I n   f ac t,  co m m o n   p r ac tice  in   th in te g r ated   c ir cu its   d esi g n   co m m u n i t y   is   t o   d iv i de   d esi g n s   i n to   d atap at h   a n d   co n tr o lo g ic  ( F ig u r e   2 ) .   B ec au s o f   t h eir   d if f er e n ce s ,   ap p r o p r iate  v er if icatio n   s ch e m e s   ca n   b ap p lie d   to   ea ch .   Data p ath   u n its   w h ich   in v o lv lar g e - in te g er s   p r o ce s s in g   ca n   b v e r if ied   u s in g   t h Ma tlab /Si m u l in k   te s tb en c h   w h er lar g e - in t eg er s   a re   s u p p o r ted   as  w i ll  b d etailed   in   th n e x t   s ec tio n .     Data p ath   u s u al l y   co n s i s ts   o f   u n if o r m   ar r a y s   o f   ce l ls ,   s u c h   as  b its   i n   r eg is ter   f ile,   s lice s   in   a n   ad d er   an d   s o   o n .   T h r em ai n i n g   lo g i is   r eg ar d ed   as c o n tr o l lo g ic.   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F u n ctio n a V erif ica tio n   o f La r g e - in teg ers   C ir cu its   u s in g   a   C o s imu la tio n - b a s ed   A p p r o a c h   ( N ejme d d in A limi )   2195       Fig u r 2 .   Data p ath   an d   co n tr o l   lo g ic  p ar titi o n   f o r   v er i f icatio n       An   ad v a n ta g o f   u s i n g   HD L   co s i m u latio n   w it h   Ma tlab /S i m u li n k   te s tb en c h   i s   t h e   p o s s ib ilit y   o f   cr o s s - le v el  d atap ath   v er if ica ti o n ,   as  w ill  b m o r d etailed   later .   T h is   m ea n s   th at  d ata s   o u tp u t   o f   d i f f er e n t   h ier ar ch ical  le v el  ca n   b p r o b ed   an d   co m p ar ed   in   r u n - ti m ag ain s Ma t lab   m o d els.  O n   t h o th er   h a n d ,   co n tr o lo g ic  ca n   b ac c u r atel y   s p ec i f ied   b y   p r o p er ties   an d   a s s er tio n s ,   a n d   t h u s   i s   v er i f iab le  u s i n g   P S L .   T h DUV s   co n tr o l lo g ic  is   s p ec i f ied   b y   s et  o f   p r o p r ieties  w r itte n   i n   P SL   as s er tio n s .   T h v er if icatio n   s tr u c tu r is   t h s et  o f   Ma t lab   Fu n ctio n   B lo ck s   w it h i n   t h e   p latf o r m   i n   c h a r g o f   th e   v er if ica tio n   p la n .   Fi g u r 3   r ep r esen ts   th ar c h itect u r o f   t h e   Ver i f icatio n   s tr u ctu r e‖ .   T h latter   is   d iv id ed   i n   t w o   b lo ck   s et s ,   co n n ec ted   to   f o r m   lo o p   w it h   th r est  o f   t h p latf o r m .   T h f ir s s et  is   c o m p o s ed   o f   s ti m u li   g en er atio n   b lo ck s   w h ile  t h s ec o n d   is   co m p o s ed   o f   a n al y s i s   b lo ck s   ( C o m p ar ato r ‖,   C h ec k er ‖  an d   Sco r eb o ar d ‖) .   W ith in   th f ir s t,  th Data   o u tp u o f   t h D UV  ( Z _ DUV) ,   is   v er if ied   a g ain s t h R ef er e n ce   Mo d el  o u tp u ( Z _ R ef ) ,   th r esu lt  o f   t h co m p ar is o n   is   tr an s f er r ed   to   th Sco r eb o ar d .   A cc o r d in g   to   th f ee d b ac k ,   t h f ir s t   s et   g e n er a tes  n e w   s ti m u li  co r r esp o n d in g   to   t h n e x co v er ag s tep   an d /o r   to   th e   n e x t   p r o p er ty   to   b v er i f ied .   T h DUV  is   h er m o d u lar   ar ith m et ic  o p er atio n .   T h o b j ec tiv is   t o   en s u r th at   DU V   m atc h es it s   s p ec if icatio n .   T h f u n ct io n al  v er i f icat io n   ap p r o ac h   is   w h ite - b o x   ap p r o ac h   ( i.e .   th HDL   d esi g n   is   k n o w n   to   th v er if ier ) .   B ec au s o f   s a m p li n g   ti m d i f f er e n ce ,   co n tr o s ig n als  a n d   d ata  w er as s ig n ed   to   s ep ar ate  b lo ck s   ( Fig u r 3 ) .   B o th   b lo ck s   ar d r iv en   b y   b lo ck   ca lled   T estb en ch   Scen ar io   Up d ate‖ .   T h r o le  o f   th la tter   is   to   u p d ate  co n tr o l sig n als a n d   d ata  ac co r d in g   to   v er i f icat io n   co v er ag e.         Fig u r 3 .   T h v er if icatio n   s tr u ctu r e       I n s id th Data   b lo ck ,   R an d o m   N u m b er   Gen er ato r   ( R NG)   p r o d u ce s   co n s tr ain ed   r an d o m   lar g e - in te g er   d ata  ( X, o p er an d s )   u s in g   VP I   s ee d   v alu e.   An   o v e r v ie w   o f   t h f u n ctio n i n g   o f   t h p latf o r m s   b lo ck s   is   g i v en   i n   T ab le   1 .   T h c o m p ar ato r   r ec eiv es  d ata  f r o m   D UV  an d   R ef er e n ce   Mo d el,   co n v er t s   it  to   VP I   d ata   t y p e,   m a k e s   t h co m p ar i s o n ,   a n d   f in al l y   tr an s f er s   t h r es u lt   t o   th Sco r eb o ar d .   Su b - DUV  C h ec k er   c h ec k s   t h e   f u n ctio n al  co r r ec tn ess   o f   in t er n al  o p er atio n s   o f   DUV.   I r ec eiv es  th p r o b ed   m etad a ta  f r o m   th D UV,   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 A u g u s 2 0 1 7     2 1 9 2     2 2 0 5   2196   co n v er ts   it  to   VP I   d ata  t y p e,   ca lcu late s   th in ter n al  o p er atio n   b it - w i s as  r e f er en ce   o p er atio n ,   m a k es  t h e   co m p ar is o n   a n d   f in a ll y   tr an s f er s   th e   r es u lt  to   th e   Sco r eb o ar d .   A s   ill u s tr ated   in   Fi g u r 3 ,   t h co m p ar ato r   a n d   th S u b - DU C h ec k er   u p d ate  th s co r eb o ar d   w i th   r es u lt s   as  lo n g   as t h co s i m u latio n   is   g o i n g   o n .   T h co n tr o lo g ic  v er i f icatio n ,   n o t r ep r esen ted   in   Fig u r 3 ,   is   d o n w ith   P SL   a s s er tio n s   s i m u lated   in   t h HDL   S i m u lato r .       T ab le  1 Fu n ctio n i n g   o f   p lat f o r m   b lo ck s   P h a se   B l o c k   C o r r e sp o n d i n g   p se u d o - c o d e   S t i m u l i   p r e p a r a t i o n   a n d   G e n e r a t i o n   T e st - b e n c h   S c e n a r i o   U p d a t e   n e w _ see d = C o m p u t e _ se e d ( f e e d b a c k ( i ) )     / / c o n s t r a i n t   o n   se e d   t o   h i t   s p e c i f i c   d a t a   i n t e r v a l        D o {                       C R L I _ 1     =   r a n d i n t ( v p i ( n e w _ se e d ) ) ;       ( * )     / /   C R L I   =   C o n st r a i n e d   R a n d o m L a r g e - I n t e g e r     C R L I _ 2   =   r a n d i n t ( v p i ( n e w _ se e d ) ) ;               O K   =   V e r i f y _ se e d   ( n e w _ se e d ,     C R L I _ 1 , C R L I _ 2 ) ;         }   / /   t o   v e r i f y   t h a t   R L I   i s c o n st r a i n e d   a s   d e si r e d   W h i l e   ( N O T   ( O K ) )           / /   R L I s d o   n o t   mat c h   t h e   d e si r e d   i n t e r v a l .   S i g n a l s   R e se t   < =   1 ;   W h e n   T   =   T 0 ,     R e se t   < =   0 ;                                     / /     T 0   =   n 0   *   C L K   C y c l e s   W h e n   T   =   T 1 ,       S t a r t _ f r a me s < =   1             / /     T 1   =   n 1   *   C L K   C y c l e s   W h e n   T   =   T 1 ,     S t a r t _ f r a me s < =   0 ;           / /     T 1   =   T 1   +   1   C L K   C y c l e   D a t a   X < =   V P I _ t o _ b i n a r y _ mat r i x ( C R L I _ 1 ) ;     Y < =   V P I _ t o _ b i n a r y _ mat r i x ( C R L I _ 2 ) ;   S i g n a l s   W h e n   T   =   T 2,       S t a r t   < =   1                                       / /     T 2   =   n 2   *   C L K   C y c l e s   W h e n   T   =   T 2,     S t a r t   < =   0 ;                                   / /     T 2 =   T 2   +   1   C L K   C y c l e   R e f e r e n c e   M o d e l   X _ v p i < =   b i n a r y _ mat r i x _ t o _ V P I ( X ) ;                               / /   i n s i d e   t h e   R e f e re n c e   Mo d e l   Y _ v p i < =   b i n a r y _ mat r i x _ t o _ V P I ( Y ) ;                               / /   i n s i d e   t h e   R e f e re n c e   Mo d e l   Z _ R e f < =   R e f e r e n c e _ M o d e l ( X _ v p i , Y _ v p i ) ;           / /   i n si d e   t h e   Re f e r e n c e   M o d e l   V e r i f i c a t i o n   e x e c u t i o n   a n d   a n a l y s i s   C o mp a r - a t o r   C o mp a r e _ r e s < =   ( Z _ D U V   = =   Z _ R e f ) ?   S u b - DUV  C h e c k e r   O p _ i , , O p _ k < =   b i n a r y _ m a t ri x _ t o _ V PI ( Pro b e _ i , , Pro b e _ k ) ;   / /   O p e ra n d o f   a   sel e c t e d   i n t e r n a l   o p e r a t i o n   a re  p r o b e d   f r o m   D U V     I n t _ M a t l a b _ o u t p u t < =   I n t e r n a l _ o p e r a t i o n ( O p _ i , , O p _ k ) ;   / /   T h e   e q u i v a l e n t   Ma t l a b   o p e ra t i o n   i s   c a l c u l a t e d .   I n t _ D U V_ o u t p u t < =   b i n a ry _ m a t ri x _ t o _ VPI( Pr o b e _ n ) ;   / /   T h e   res u l t   o f   t h e   i n t e r n a l   o p e r a t i o n   i a l s o   p r o b e d   C h e c k _ r e s< = ( I n t _ D U V _ o u t p u t     = = I n t _ Ma t l a b _ o u t p u t ) ?   / /   res u l t a r e   c o m p a re d   P r o p e r t y   a sse r t i o n s   ( * * )     p sl   a sse r t _ d o n e _ p u l se   :   a sse r t   a l w a y s( {d o n e } | - >             n e x t   {! d o n e } a b o r t   ! R S T _ N )   @   ( p o se d g e   C L K ); --   si g n a l   D O N i a   p u l se  o f   o n e   c l o c k     c y c l e     S c o r e - b o a r d   D a t a _   c o v e ra g e = Me a s u re _ c o v e ra g e ( C o m p a r e _ res, C h e c k _ r e s, C RLI _ ( c o v e ra g e _ st e p   ) ,   T o t a l _ Ass e rt i o n s _ c o v e ra g e )   f e e d b a c k ( i + 1 ) = C o m p u t e _ n e w _ t e st b e n c h _ s c e n a ri o ( D a t a _   c o v e r a g e ) ;   *   r a n d i n t ( )   i s a   r a n d o a n d   u n i f o r ml y   d i st r i b u t e d   V P I   n u m b e r .     **   P r o p e r t y   A ss e r t i o n s‖  i n o t   a   b l o c k   o f   t h e   p l a t f o r m;   i t   r u n s   i n   H D L   si mu l a t o r .       2 . 3 .   L a rg e - inte g er   Da t a   P ro ce s s ing   L ar g e - i n te g er s   d ata  p r o ce s s i n g   i s   a n   i m p o r tan p ar o f   t h e   p latf o r m .   P r o ce s s i n g   is   ca r r ied   o u i n   Ma tlab ,   Si m u li n k   a n d   s i m u la ted   h ar d w ar e.   W a s s u m t h at  th e   p latf o r m ,   s h o w n   in   Fi g u r 4 ,   v er if ies  th e   o p er atio n   f:   f( X , Y) ,   w h er e:  X Y   an d   Z   ar e   th r ee   lar g e - in t eg er s .   C o n tr o s i g n a ls   ar r eset  an d   s tar t.  Do n is   an   o u tp u s i g n al  t h at  i n d icate s   th e   en d   o f   t h DUV s   o p er atio n .   Si m u la tio n   co n tr o l is  h a n d led   b y   Si m u li n k .   T h co - s i m u latio n   s ta g ( s ta g 5   in   Fi g u r 4 )   co n tai n s   t h R e f er en ce   Mo d el  an d   th e   DUV.   T h R ef er e n ce   Mo d el  is   t h D U V‘ s   eq u i v alen m o d el  w r it ten   in   Ma t lab   in s id Ma tlab   Fu n ctio n   b lo c k .   T h DUV  is   r ep r esen ted   b y   t h HDL   C o s i m u latio n   b lo ck .   T h DUV‘ s   s i m u lato r   ( Mo d elSim )   is   la u n c h ed   an d   lin k ed   to   Si m u li n k   u s i n g   Ma tlab   co d b ased   o n   T C L   s cr ip t.  W h en   co m m u n icati o n   is   estab li s h ed ,   t h e   s i m u lato r   f u n ctio n s   as  th s er v er   an d   Si m u li n k   a s   clien t.  T h HDL   s i m u lato r   r esp o n d s   to   s i m u latio n   r eq u ests   it  r ec ei v es  f r o m   th S i m u li n k   C lie n t.  T h co m m u n i ca tio n   b et w ee n   t h HD L   Si m u lato r   an d   Si m u li n k   is   d o n e   t h r o u g h   th HD L   Ve r if ier   to o l.  T h m ax i m u m   len g th   o f   in te g er   d ata  t y p es  s u p p o r ted   b y   HD L   C o s i m u la tio n   B lo ck   in   S i m u l in k   i s   1 2 8 - b its .   T o   w o r k   ar o u n d   t h is   li m itat io n ,   th DUV   w as  m as k ed   in   a n   HDL   w r ap p er   th at  s tack s   th r ec eiv ed   d ata  f r a m es  i n to   lo g ic  v ec to r   th at  m atc h es  th i n p u d ata  s ize  o f   th e   DUV  a n d   v ice - v er s f o r   t h o u tp u d ata.   T w o   k i n d s   o f   ad ap ter s   w er e   u s ed   in   t h p lat f o r m   ( Fro n te n d   an d   B ac k en d   ad ap ter s ) T h f ir s o n e   ad ap t s   d ata  an d   co n tr o s ig n al s   r ec eiv ed   in   Ma tlab /Si m u lin k   f o r m at s   to   DUV  s u p p o r ted   f o r m at s .   W ith in   t h is   s tag e,   ea c h   d ata  m atr i x   is   co n v er ted   i n to   s eq u e n ce   o f   s ca lar s   u s i n g   th e   Si m u li n k ‘s   b lo ck   U n b u f f er ‖.   T h Un b u f f er   u n b u f f er s   a n   M - by - in p u in to   1 - by - o u tp u ( Fig u r 5 ( a ) ) .   T h at  is ,   in p u ts   ar u n b u f f er ed   r o w - w i s s o   th a ea ch   m atr ix   r o w   b ec o m e s   an   i n d ep en d en t   ti m e - s a m p le  in   t h e   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F u n ctio n a V erif ica tio n   o f La r g e - in teg ers   C ir cu its   u s in g   a   C o s imu la tio n - b a s ed   A p p r o a c h   ( N ejme d d in A limi )   2197   o u tp u t.  A s   e x a m p le,   1 9 2 - b it  d ata  f its   i n to   2 4 - by - 8   m atr i x ,   an d   th Un b u f f er   B lo ck   w i ll  u n b u f f er   t h 2 4 - by - 8   i n p u t   i n to   a n   8 - b it   le n g t h   v ec to r .   T h en ea c h   d ata  i s   co n v er ted   to   s tan d ar d   lo g ic  v ec to r   v ia  t h ―Da ta   T y p C o n v er s i o n ‖  b lo ck .   T h B ac k en d   ad ap ter   ad ap ts   d ata  an d   s i g n a ls   f r o m   DU to   th C o m p ar ato r   an d   C h ec k er   b lo ck s .   I n   th is   s ta g e,   th HDL   b lo ck   o u tp u d ata  is   r e - b u f f er ed   in to   d ec i m al  m a tr ix   u s i n g   a   Si m u li n k   b lo ck   ―D ela y   L in e‖ .   T h latter   p er f o r m s   t h r ev e r s task   o f   th ―Un b u f f er   B lo ck r eb u f f er i n g   s eq u en ce   o f   Mi - by - m a tr ix   i n p u t s   in to   s eq u en ce   o f   Mo - by - m atr i x   o u tp u ts   ( Fi g u r 5 ( b ) ) .           Fig u r 4 .   B lo ck   d iag r a m   o f   t h p r o p o s ed   v er if icatio n   p lat f o r m           Fig u r 5 .   T h ad a p ter s       An   atte n tio n   s h o u ld   b g i v e n   to   th r ea d in g   ti m o f   t h De la y   L i n e‖   o u tp u s o   t h at  t h d ata  m atr i x   ca n   b r ea d   e n tire l y .   I n   f ac t,   t h DU w r ap p er ,   d etailed   in   latter   p ar ag r ap h w a s   d es ig n ed   to   s en d   ea c h   o f   Z _ DUV  f r a m es   at  e v er y   clo ck s   p o s iti v ed g s tar tin g   f r o m   i n s tan t   w h en   th e   o u tp u s ig n al  d o n e‖   is   o n   a n d   ac co r d in g   to   t h Dela y   L i n e ‖  B lo ck   f u n ctio n i n g ,   t h e n tir m atr i x   r ep r esen t in g   Z _ DUV   ca n   b r ea d   b y   t h e   C o m p ar ato r   B lo ck   at  ti m T   c alcu lated   in   f o r m u la  2 :     T=T i m e ( done = 1) +N br_of _Z_f rames*T ( Z _s ample _ pe r iod)           ( 2)   U n b u f f e r N M  ... N N M D U V   I n p u t           ( H W )   D a t a   Ty p e   C o n v e r s i o n D e l a y     Li n e  ... N N M i   =   1 D U V   o u p u t             ( H W ) N Mo ( a )   T h e   F r o n t e n d   A d a p t e r ( b )   T h e   B a c k e n d   A d a p t e r D a t a   m a t r i x D a t a   f r a m e s D a t a   f r a m e s D a t a   m a t r i x U n b u f f e r   D a t a   Ty p e   C o n v e r s i o n Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 A u g u s 2 0 1 7     2 1 9 2     2 2 0 5   2198   W h er e:  T im e (done = 1)   is   t h ti m e   w h en   d o n i s   s et  to   1 ,   Nb r of  fram es   is   t h t o tal    n u m b er   o f   Z   f r a m e s   o u tp u t ted   f r o m   HD L   B lo ck ,   an d   (Z  sam pl period)   is   th s a m p li n g   t i m o f   Z .   T h Fig u r e   6   ill u s tr ates  t h c o m m u n icatio n   b et w ee n   Si m u l in k   an d   th e   DUV   v ia   t h w r ap p er .   A s   s h o w n ,   I n p u ts   ( r eset,  s tar t_ f r a m es,  s tar t,  X,   Y)   ar s ti m u l f r o m   Ma tlab /Si m u li n k ,   w h i le  O u tp u t s   ( Do n e,   Z _ DUV,   P r o b e1 …  P r o b e   n )   ar r esu lts   s e n b ac k   to   Ma tlab /Si m u li n k   f o r   co m p ar is o n   a n d   in ter n al  c h ec k in g .   T h s tar t_ f r a m es i s   an   e x tr a   in p u t to   th DUV  W r ap p er   to   co n tr o l th r ec ep tio n   o f   f r a m e s   f r o m   Data   b lo ck .   T h r o le  o f   th W r ap p er   is   t o   h an d le  c y cle - ac c u r ate  tr a n s f er   o f   d ata  b et w ee n   Si m u l i n k   a n d   t h e   DUV  w it h o u m o d i f y in g   th e   latter s   d escr ip tio n .   T h w r ap p er   ,   wr itte n   in   VHD L ,   i s   b ased   o n   a n   I n p u t   co n v er ter   an d   t w o   O u tp u t c o n v er ter s .   On d ed icate d   to   DUV‘ s   r es u lt,  t h e   o th er   to   in ter n al   s ig n als ( Fi g u r e   7 ) .           Fig u r 6 .   UM L   s eq u en ce   d ia g r a m   o f   Si m u li n k     HD L   b lo ck   co m m u n icatio n           Fig u r 7 .   T h HDL   C o s i m u lat io n   b lo ck   d ata  f lo w       As  ill u s tr ated   in   F ig u r 8 ( a ) ,   T h I n p u C o n v er ter ‖  m o d u le  r ec eiv e s   d ata  ( X, Y)   f r o m   Ma tlab /Si m u l in k ,   s tac k s   t h w - b it  le n g t h   f r a m e s   ( f i )   i n to   S tan d ar d   lo g ic  v ec to r .   T h m - b it  m atc h i n g   t h s ize   o f   th ex p ec ted   DUV  i n p u d ata  s ize  ( f 0   to   f k   f r a m es)   ar ex tr ac ted   ( u n p a d d i n g ‖  o p er atio n ) W h en   t h e   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F u n ctio n a V erif ica tio n   o f La r g e - in teg ers   C ir cu its   u s in g   a   C o s imu la tio n - b a s ed   A p p r o a c h   ( N ejme d d in A limi )   2199   O u tp u C o n v er ter ‖  m o d u le  r ec eiv es  t h r esu l t ,   b its   ar ad d ed   to   th lo g ic  v ec to r   to   b r i n g   it  to   th r eq u ir ed   s ize  ( f k+ to   f n   f r a m e s)   ( p a d d in g ‖  o p e r atio n ) .   T h en ,   th lo g i v ec to r   is   s e n   i n   w - bi f r a m es  to   th n ex s ta g e   ( Fig u r e   8 ( b ) ) .   Si m ilar l y ,   t h ―De b u g   C o n v er ter ‖  m o d u le  b r in g s   DUV s   i n ter n al  s i g n a ls   to   th n e x t s tag e.             Fig u r 8 T h DUV‘ s   W r ap p e r   u n it s .     2 . 4 .   P la t f o rm   Co ntr o l,  Set t ing s   a nd   E x ec utio   An   ess e n tial  s id o f   th p latf o r m   i th e   co n tr o an d   s etti n g s .   P latf o r m   co n tr o co n s i s ts   i n   c o n tr o llin g   th e x ec u tio n   o f   t h tes tb en c h   b y   s c h ed u li n g   t h s t i m u li   t o   th DUV /R e f er en ce   Mo d el  an d   t h o u t g o in g   s ig n al s /d ata  to   b v er i f ied .   T h ch a llen g h er is   to   s y n c h r o n ize  t h Ma tlab /S i m u li n k   b lo ck s ,   w h ich   ar e   in h er e n tl y   u n t i m ed ,   w it h   a n   R T L - lev e l d esig n   r u n n i n g   in   a n   ev en t - b ased   s i m u lato r   ( Mo d elSi m ) .   T h P latf o r m   C o n tr o l p r o ce s s   is   ab s tr ac ted   in   th ti m ed   f in ite  s tate  m a c h in ( T FS M)   r ep r esen ted   in   Fi g u r e   9.           Fig u r 9 T h f in ite  s ta te  m ac h in o f   t h P latf o r m   C o n tr o l       B ec au s Ma tlab   Fu n ctio n   B l o ck ,   an d   Ma t lab   lan g u ag e   i n   g e n er al,   is   u n ti m ed ,   t h ti m i n g   an d   th e   d eliv er y   o f   t h d ata  is   co n tr o lled   b y   t h HD L   s i m u lato r   ( w h e n   Ma tlab   Fu n ctio n   B lo ck   is   lo ca ted   af ter   th e   DUV)   an d /o r   b y   th B lo ck s   s a m p lin g   ti m s etti n g   ( w h e n   M atlab   Fu n ctio n   B lo ck   is   lo ca te d   f o r w ar d ) .   Usi n g   a   Si m u li n k   Dig ital  C lo c k ,   th s t i m u li  ( co n tr o s i g n al s   an d   d at a)   ar e   g en er ated   in   s p ec if ic  s i m u latio n   ti m e s .   T h e   tr an s itio n   d ela y   ti m e s   b et w ee n   th T FS s tates a r p r esen te d   in   T ab le  2 .   P latf o r m   s et tin g s   ar th e   s ett i n g s   o f   p ar a m eter s   r elate d   to   ea ch   b lo ck   o f   t h p lat f o r m .   T h at  i s ,   th e   Si m u li n k   b lo ck s   p ar a m e ter s   ( Un b u f f er ,   Dela y   L i n e,   etc . )   a n d   th s a m p li n g   ti m es  f o r   Ma tlab   f u n ctio n   b lo ck s   ( Ver if icatio n   s tr u ct u r b lo cs).   A   g r ap h ical  u s er   in ter f ac ( G UI )   w as d ev elo p ed   to   f ac ilit at th is   ta s k .     I n   ad d itio n   to   t h c h o ice  o f   Si m u li n k   b lo ck s   an d   a lg o r it h m s   in s id Ma tlab   Fu n ctio n   b lo ck s ,   t h f u n ctio n i n g   o f   t h p lat f o r m   r e lies   o n   th ti m in g   s etti n g s .   I n   f ac t,  f o r   ea ch   b lo ck ,   a   s a m p l ti m n ee d s   to   b s p ec if ied .   I n   Si m u l in k ,   t h s a m p le  ti m o f   a   b lo ck   is   a   p ar am eter   t h at  i n d icate s   w h e n ,   d u r in g   s i m u latio n ,   t h e   b lo ck   is   ac tiv an d   i f   ap p r o p r i ate,   u p d ates  its   in ter n al  s tate.   Fo r   HDL   co s i m u lat io n   B lo ck ,   s a m p le  ti m h as  X Y X Y m m R e c e p t i o n U n p a d d i n g Clk reset start_frame done Z w Z w w m Tr a n s m i s s i o n P a d d i n g + ... f0 + fk w w + ... + fn w + ... f0 + fk w w + ... + fn w + ... fk + fn w w + ... f0 + w ( a )   T h e   i n p u t   c o n v e r t e r ( b )   T h e   o u t p u t   c o n v e r t e r Data vectors Data frames Data vector Data frames ... f0 f1 fk m ... f0 f1 fk m ... f0 f1 fk m S t a r t   d a t a g e n e r a t i o n   p r o c e s s S t a r t   t e s t   b e n c h   p a r a m s   u p d a t e r e s e t r e s e t   =   0 r e s e t   =   1 s t a r t _ f r a m e s   =   1 s i m _ t i m e   =   T0   s i m _ t i m e   =   T1 S t a r t   d a t a   g e n e r a t i o n p r o c e s s   -   f i n i s h e d s t a r t _ f r a m e s   =   0 s i m _ t i m e   =   T1 ' s i m _ t i m e   =   T2 S t a r t   L a r g e - i n t o p e r a t i o n s t a r t   =   1 s i m _ t i m e   =   T2 ' L a r g e - i n t o p e r a t i o n s t a r t   =   0 S t a r t   t e s t   b e n c h   p a r a m s   u p d a t e   -   f i n i s h e d U p d a t e   =   1 U p d a t e   =   0 s i m _ t i m e   =   Tp w a i t   T1 w a i t   T1 ' w a i t   T0 w a i t   T2 w a i t   T2 ' w a i t   Tp w a i t   Tf C o m p a r i s o n   v e r i f i c a t i o n w a i t   Td i n i t P r o c e s s   r e s u l t s         &   d i s p l a y i d l e s i m _ t i m e   =   Tf s i m _ t i m e   =   Td Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 A u g u s 2 0 1 7     2 1 9 2     2 2 0 5   2200   to   b s et  f o r   ea ch   i n p u t/o u tp u t.  Sa m p le  ti m e s   o f   p lat f o r m   b lo ck s   w er s et  to   HD L   clo ck   p er io d   ex ce p t   th r ef er e n ce   m o d el‖  w h o m   t h ex ec u t io n   d ep en d s   o n   t h tr i g g er in g   s ig n al  r ec ei v ed   f r o m   t h Sti m u li  Ge n er ato r   B lo ck .   T h s am p le  ti m o f   Da ta  b lo ck   ca n   b ca lcu lated   u s in g   f o r m u la  5   d er iv ed   f r o m   f o r m u la  4 :     UB O_ S a mp le_ Time  UB I _ S a mp le_ Time  / D a ta   Ma tr ix_ r o w s _ N b r       ( 4 )     W h er UB is   U n b u f f er ed   B lo ck   Ou tp u t‖      UB I _ s a mp le_ time  = D UV _ clk_ p erio d   *   D a ta   Ma tr ix_ r o w s _ N b r       ( 5 )     W h er UB I   is   U n b u f f er ed   B lo ck   I n p u t‖    As  UB I   is   co n n ec ted   to   Da ta   b lo ck ,   th v al u o f   Data   b lo ck s   s a m p le  t i m e   is   t h s a m e   as  t h at  o f   UB I .   B ec au s th e   Un b u f f er   o n l y   ac ce p ts   f i x ed - s ize  i n p u t,  o u tp u t   o f   Da ta  s u b - b lo ck   ca n n o b s et  to   v ar iab le   s ize  t y p e.   T h er ef o r e,   d ata  b it - s ize  ( o p er an d s )   h as to   b s et  m an u al l y   b y   u s er   f o r   d if f er en t o p er an d s   b it - s ize.     I n   p r ac tice,   Sam p le  ti m ca n   b s et  au to m atica ll y   b y   w o r k i n g   ar o u n d   th r es tr ictio n   o f   th Un b u f f er .   T o   d o   s o ,   th s ize  o f   a ll  d ata  tr an s f er r ed   b et w ee n   b lo ck s   in   th e   p latf o r m   ar c h o s en   as  co n s ta n t h a h o ld s   all   s ta n d ar d   s izes  o f   f i n ite - f ield   co m m o n l y   u s ed   in   P u b lic - k e y   C r y p to g r ap h y   ( f o r   i n s ta n ce ,   1 0 2 4 ) .   T h er ef o r e,   th e   N u m b er   o f   d ata  m atr ix   r o w s   i s   also   co n s ta n ( f i x ed   s ize - in p u t)   an d   th Sa m p le  T im e   o f   UB I ,     b ec o m e s   o n l y   DUV s   C lo ck   d ep en d en t.  T h ch o ice  o f   u n iq u s ize  s i m p li f ies  th e   tr an s m is s io n /r ec ep tio n   o f   d at in s id ea c h   b lo ck   an d   o n l y   b its   co r r esp o n d in g   to   o p er an d s   r ea s ize  ( e. g .   1 9 2 - b it)  ar u s ed .   T h is   tas k   i s   d o n b y   th W r ap p er   as  it  b r in g s   o p er an d s   to   th r eq u i r ed   s ize  b y   t h p ad d in g   a n d   u n p a d d in g   p r o ce s s es  p r ev io u s l y   d etailed .   User   h as   to   p lace   th VHD L   d e s ig n   co d e( s )   in s id s p ec if ic  f o ld er   f o r   co - s i m u lat io n ,   ad j u s w r ap p er s   p ar a m eter s   to   th s ize  o f   th HD L   d esi g n   o p er an d s   an d   co n n ec w r ap p er s   p r o b es  ( o u tp u ts )   to   d esir ed   DUV‘ s   in ter n al   s ig n al s .   T h O u tp u t   Data   A d a p ter ,   r ep r esen ted   b y   t h Si m u l in k   b lo ck   Dela Lin e ‖,   e x ec u tes   t h r e v er s ta s k   o f   th U n b u f f er   B lo ck .   T h at  is ,   it tr an s f o r m s   s eq u en ce   o f   d ata  f r a m e s   in to   m atr ix .     W h en   v er i f icatio n   is   la u n c h ed ,   P SL   ass er tio n s   test   r es u lts   ar p r o ce s s ed   in   Ma tlab   w o r k s p ac e.   T h en ,   r esu lt s   ar ca r r ied   t o   Sco r eb o ar d   alo n g   co m p ar ato r   an d   ch ec k er   r esu lt s .   T h Sco r eb o a r d   co m p u tes  t h n e v er if ica tio n   co v er ag a n d   g en er ates  f ee d b ac k   s u m m ar izin g   th co v er ag e.   A cc o r d in g   to   th f ee d b ac k ,   n e test b en c h   s ce n ar io   a n d   p ar a m eter s   tar g eti n g   t h u n co v er ed   ass er tio n s   a n d /o r   d atap ath   lo g ic  n o y et  v er i f ied   ar s et.   T h en ,   th n e x t te s tb e n ch   w ill b r ea d y   to   r u n .       T ab le  2 .   T im P er io d s   o f   th T FS M   D e l a y   t i me   sy mb o l   S i g n i f i c a n c e   V a l u e   T 0   T i me   t o   w a i t   b e f o r e   st a r t i n g   a   n e w   t e st   T 0   = n 0   *   C L K   C y c l e s   T 1   T i me   t o   w a i t   b e f o r e   S t a r t i n g   D a t a   g e n e r a t i o n   p r o c e ss   T 1   = n 1   *   C L K   C y c l e s   T 2   T i me   t o   w a i t   b e f o r e   S t a r t i n g   D a t a   g e n e r a t i o n   p r o c e ss   T 2   = n 2   *   C L K   C y c l e s   T d   T i me   t o   w a i t   b e f o r e   D o n e   =   1   T d   = n d   *   C L K   C y c l e s   T f   T i me   t o   w a i t   b e f o r e     F e e d b a c k   i s   r e a d y   T f   = n f   *   C L K   C y c l e s   T p   T i me   t o   w a i t   b e f o r e   Te st b e n c h   P a r a m e t e r s a r e   u p d a t e d   T p   = n d   *   C L K   C y c l e s   T x‘   O n e   c l o c k   c y c l e   a f t e r   T x   T x   =   T x   +   C L K   C y c l e       2 . 5 .   Ver if ica t io n P la t f o rm   w it h F P G in - t he - lo o p   An o th er   a s p ec o f   r eu s ab ilit y   o f   t h p r o p o s ed   p latf o r m   is   t h p o s s ib ilit y   to   s w itch   f r o m   HD L   co s i m u latio n   to   r ea h ar d w ar e   test i n g   w h ile   k ee p in g   th e   s a m v er if icatio n   p latf o r m .   T h is   o p tio n   w a s   te s ted   w it h   t h ―Ha r d w ar e - i n - t h e - lo o p ‖  ( HI L )   o p tio n   p r o v id ed   b y   S i m u li n k   f o r   FP GA   b o ar d s   eq u ip p ed   w it h   Gi g ab it   E th er n et   p o r ( an   A l ter DE 2 - 1 1 5   b o ar d   w ith   C y clo n e   I E P 4 C E 1 1 5   FP GA   w a s   u s ed ) .   T h is   w a y   e n ab les   co n tr o llin g   an d   v er if y i n g   d e s ig n   ( m o d u lar   m u ltip lier ,   m o r d etails  in   s ec tio n   3 )   r u n n i n g   o n   FP G A   f r o m   th Ma tlab /S i m u li n k   p latf o r m   w it h   t h d esi g n ‘s   r ea ex ec u tio n   ti m e   ( Fi g u r 1 0 ) .   Ho w e v er ,   th is   ca m at  co s t   as  t h at  i n ter n al  v er i f icatio n   ( S u b - DU P r o b in g )   b ec o m e s   i n ac ce s s ib le   d u to   t h e   FP G A   d ev elo p m e n t s   to o r estrictio n s   o n   d es ig n s   co d in g   s t y le  a n d   w r ap p in g .   T o   co n clu d th i s   s ec tio n ,   T ab le  3   g i v e s   co m p ar is o n   b et wee n   t h p r es e n w o r k   a n d   s i m ilar   w o r k s   f r o m   l iter atu r e.   T h T ab le  s h o w s   th at   t h p r o p o s ed   p latf o r m   w h ile  s h ar in g   s o m f ea t u r es  w it h   o t h er   w o r k s   ( s u p p o r ted   HDL ,   co s i m u lat io n ,   etc. ) ,   s tan d s   o u w it h   m o r p o w er f u HV L ,   u n r estric ted   lar g e - i n te g er   s u p p o r an d   ad ap tab ilit y   to   HI L .   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F u n ctio n a V erif ica tio n   o f La r g e - in teg ers   C ir cu its   u s in g   a   C o s imu la tio n - b a s ed   A p p r o a c h   ( N ejme d d in A limi )   2201       Fig u r 10 .   Ver if icatio n   P latf o r m   w it h   FP G A - in - t h e - lo o p       T ab le  3.   C o m p ar is o n   w i th   s i m ilar   v er if icat io n   p lat f o r m s   V e r i f i c a t i o n   e n v i r o n me n t   H W   V e r i f i c a t i o n   L a n g u a g e   ( H V L )   S u p p o r t e d   H D L   I n t e r f a c i n g   w i t h   S i mu l a t o r   C o si m u l a t i o n   w i t h   V H D L   si mu l a t o r   L a r g e - i n t e g e r   su p p o r t   D U V   i n   H a r d w a r e   [ 1 3 ]   C   V H D L   F LI   Y e s   L i mi t e d   No   [ 1 4 ]   P y t h o n   V H D L / V e r i l o g   F LI / V P I   Y e s   L i mi t e d   No   [ 1 5 ]   P y t h o n   V e r i l o g   V P I   No   L i mi t e d   No   [ 2 5 ]   P y t h o n   V e r i l o g   V P I   No   L i mi t e d   No   [ 2 6 ]   Ru by   V e r i l o g   V P I   No   L i mi t e d   No   T h i s W o r k   M a t l a b / S i m u l i n k   V H D L / V e r i l o g   H D L   V e r i f i e r ®   +   W r a p p e r   Y e s   U n l i mi t e d     Y e s (H I L )     V PI   V e r i l o g   P r o c e d u r a l   I n t e r f a c e F L I   F o r e i g n   L a n g u a g e   I n t e r f a c e ,   PL I   P r o c e d u r a l   L a n g u a g e   I n t e r f a c e   HIL   :   H a r d w a r e - in - t h e - l o o p .       3.   CASE   S T UD & R E SU L T S         As  ca s e   s t u d y   o f   t h p lat f o r m ,   w e   co n s id er   th e   o p er atio n   Z   f ( X , Y )   ,   w h er e   X Y   an d   Z   ar th r ee   lar g e - i n te g er s .   C o n tr o s i g n a ls   ar e   r ese t   a n d   s ta r t ,   w h ile   Do n e   is   a n   o u tp u t   i n d icatin g   th e   e n d   o f   th e   o p er atio n T h g o al   is   to   e v alu a te  t h co s o f   t h b it - s ize,   t h n u m b er   o f   ass er tio n s   a n d   th in ter n al  s ig n al  p r o b in g   o n   t h e   p latf o r m .     3 . 1 .   L a rg e - inte g er   Arit h m et ic  B a ck g ro un d   L ar g e - i n te g er   ar ith m etic  h as  a   v ar iet y   o f   ap p licatio n s   in   cr y p to g r ap h y .   Am o n g   t h ese,   A E S,  R S A   a n d   E C C .   As  ill u s tr ated   i n   th e   Fi g u r e   1 1 ,   E C C   s c h e m es   ar b ased   o n   P o in t   o p er atio n s ,   p r i m ar il y   o n   t h p o in t   m u ltip licatio n   an d   also   o n   t h o p er atio n s   o n   w h ic h   it  p o in m u lt ip licatio n   r elie s ,   i.e .   p o in ad d itio n   an d   d o u b lin g .   I n   tu r n ,   t h o s p o in o p er atio n s   ar m ad o n   f in ite - f ield s   ar it h m etic,   a   p ar tic u lar   f ie ld   o f   lar g e - in te g er s .   T h is   i m p l ies  t h at  f in ite - f ield   ar ith m etic  ar d et er m in a n t   to   d esi g n   a n   e f f ici en ellip tic  c u r v cr y p to s y s te m .     Fi n ite - f ield   ar i th m etic  is   t h ar it h m e tic  o f   i n teg er s   m o d u lo   lar g p r i m e   p .   A r ith m etic  i n   f i n ite - f ield   is   d if f er e n f r o m   s t an d ar d   in teg er   ar ith m etic   an d   all  o p er atio n s   p er f o r m ed   in   th f in ite - f ield   r esu l t   in   an   e le m en w it h i n   th a f ie ld .   T h r ee   k in d s   o f   f ield s   t h at   ar u s ed   f o r   ef f icien i m p le m en tatio n   o f   E C C   s y s te m s   ar p r i m f ield s   ( F p ) ,   b in ar y   f ield s   ( F 2 m ) ,   an d   o p t i m al  e x te n s io n   f ie ld s   ( F p m ) .   T h o s f i eld s   w er ex ten s i v el y   s t u d ied   a n d   th is   h as   r es u lted   i n   n u m er o u s   a lg o r ith m s .   Fi n ite - f ield   ar it h m etic  is   a   p r ac tical   ex a m p le  o f   lar g e - i n teg er   ar it h m etic  u s a g an d   is   t h co r n er s to n o f   cr y p to g r ap h ic  s ch e m e s   s u c h   as E C C .   Evaluation Warning : The document was created with Spire.PDF for Python.