I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute r  E ng in ee ring   ( I J E CE )   Vo l.   9 ,   No .   5 ,  Octo b e r   2 0 1 9 ,   p p .   3 4 2 3 ~ 3 4 3 1   I SS N:  2088 - 8708 ,  DOI : 1 0 . 1 1 5 9 1 / i j ec e . v 9 i 5 . p p 3 4 2 3 - 3431           3423       J o ur na l ho m ep a g e :  h ttp : //ia e s co r e . co m/ jo u r n a ls /in d ex . p h p / I JE C E   An  o pti m i zed  m e t ho d t o w a rds  f o r m a l  v erification o f  m ix ed  s ig na ls usin g   d iff e rential  f ed  n e ura l   n etw o rk  ov er FF NN       Vidy a   D.   S . ,  M a njuna t h   Ra m a cha n dra   A s sa m   Do n   Bo sc o   Un iv e rsity ,   G u w a h a ti ,   In d ia       Art icle  I nfo     AB ST RAC T   A r ticle  his to r y:   R ec eiv ed   Oct   10 ,   2 0 1 8   R ev i s ed   Mar   2 6 ,   2 0 1 9   A cc ep ted   A p r   1 5 ,   2 0 1 9       T o d a y ,   th e   se m i c o n d u c t o r  i n d u stries   a re   ra p id ly   u sin g a n a lo g   a n d   m ix e d   sig n a ls  to   a c h iev e   c o st - e ff e c ti v e   s o lu t i o n s o n   a   S y ste m   o n   Ch ip   (S o C)  d e sig n .     T h e   S o C  d e v ice   i s  a   p a rt  o f   a n a lo g ,   d ig it a l  a n d   e ss e n ti a l  m ix e d - sig n a l   m o d e ls/circ u it s  m e rg e d   o n   a   s e m ico n d u c t o r  d e v ic e ,   w h ich   p r o v id e s  th e   p latf o rm   to   b u il d   m o d e rn   re tail/ c o n su m e r  e lec tro n ics   a p p li a n c e s  w it h   s m a rt   tec h n o l o g y .   In   o rd e r  t o   e v a lu a te  th e   m ix e d   sig n a ls,  th e   c o n v e n ti o n a l  a p p ro a c h e s  a re   n o t  e f f e c ti v e   with   re sp e c t  to   it s  p e rf o r m a n c e ,   ti m e   a n d   m a n u f a c tu rin g   c o st.  T h u s,  th e   re c e n t  re se a rc h e s  we re   m u c h   in tere ste d   in   f o r m a l  v e ri f ica ti o n   tec h n iq u e   a s  it   p ro v id e s  th e   e v id e n c e   o f  c o n sc io u s   a lg o rit h m s  in   a   sy ste m .   T h e   d e m a n d   f o r  f o rm a l  v e ri f ica ti o n   in   th e   S o C   d e sig n s  in   t h e   c o n tex t  o f   so f twa r e   a n d   h a rd w a re   p latf o r m   is  h ig h   b e c a u se   o f   it s  c o st  a n d   a c c u ra c y .   T h u s,  th e   p a p e r  in tro d u c e s  a tec h n i q u e   o f   f o r m a l   v e ri f ica ti o n   f o r   m ix e d   sig n a ls  b y   u sin g   train in g   m o d e ls  o f   th e   Dif f e re n ti a l  f e d   n e u ra l  n e tw o rk   (DFNN)  o v e r  fe e d f o r w a rd   n e u ra l  n e tw o rk   (F F NN ).   T h e   f o r m a l  v e ri f ica ti o n   is  p e rf o rm e d   t h ro u g h   e q u iv a len c e   c h e c k in g   b y   u sin g   re c e n tl y   a d o p ted   d e sig n s  a s  re fe re n c e   d e sig n s.  T h e   o u tco m e s  o f   th e   v e ri f ica ti o n   tec h n i q u e s  s u g g e sts  th a t  DFNN   b a se d   tec h n i q u e   im p ro v e s  th e   train in g   a c c u ra c y   a n d   o p t im ize s  t h e   h a rd w a re   re so u rc e s  li k e   a re a ,   p o w e r  th a n   th e   F F NN   b a se d   tec h n i q u e .   K ey w o r d s :   A r ea   Fo r m al  v er i f icatio n   Mix ed   s i g n al s   Neu r al  n et w o r k s   P o w er   Co p y rig h t  ©   2 0 1 9   In stit u te o f  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 l  rig h ts re se rv e d .   C o r r e s p o nd ing   A uth o r :   Vid y a  D.   S . ,    R esear ch   Sch o lar ,     Ass a m   Do n   B o s co   Un i v er s it y ,     Gu w a h ati,   I n d ia .   E m ail: d s v id h y a0 7 7 0 @ g m ail. co m       1.   I NT RO D UCT I O N   Var io u s   f o r m s   o f   r esear ch   ac ti v itie s   w er e  m ad e  i n   t h e  r ec en t   p ast  w h ic h   p r o v id ed   a  b r ea k t h r o u g h   f o r   th e  co m p u ter - a id ed   d esig n   ( C A D)   p r ac tices,  m ai n l y   i n   t h e  d esig n   o f   h ar d w ar e  d escr ip tio n   la n g u a g e  ( HD L )   m ea n t  f o r   an al y s i s   o f   th e   m ix ed   s ig n als   ( MS)   b eh a v io r   [ 1 ] .   So m e  o f   t h e  i m p o r tan t  d esi g n   m ec h a n i s m s   w er e   p r esen ted   to   v ar io u s   f o r m   o f   d es ig n   p r o ce d u r es  b y   u s i n g   d if f er en t  d esig n   tech n iq u es.  T h e  p r im e  in te n tio n   o f   C A D  tec h n iq u e  is   a n al y s i s   a n d   d esig n   v er if icat io n   b u t  wh ich   is   c h alle n g i n g   tas k   a n d   it  n ee d s   t h e  lo t  o f   ex p er tis e  an d   i n - d ep th   u n d er s tan d in g   o f   a n alo g   a n d   m i x ed   s ig n al s   ( A M S)  b eh av io r   [ 2 ,   3 ] .   T h e  v er if icat io n   p r o ce s s   in v o lv es   v ar io u s   k i n d s   o f   i s s u es  i n   al l  t h e  s ta g es  o f   t h e  d esi g n   p r o ce d u r e.   A ls o ,   th e  w id e  r a n g e  o f   d if f er e n ce   ca n   b e  o b s er v ed   in   th e  d i f f er e n t  clas s es  o f   AM S  d esig n s   [ 4 ] .   T h e  m aj o r   p r o b lem   d u r in g   t h e   v er if ica tio n   p r o ce s s   f o r   A MS   d esig n s   at   ad ap tio n   le v el  o f   t h e  an a lo g   cir c u its   ar e  th e  c h a r ac ter is tics   d e f in ed   d ir ec tl y   in   ter m s   o f   u n i n ter r u p ted   s ig n al  q u an t ities   [ 5 ] .   A l s o ,   th e  p r o b le m   as s o ciate d   w it h   t h e  p r o p er   f u n ctio n alitie s   o f   i n te g r ated   d esig n s   n ee d   to   m ee t t h e  s y s te m   p er f o r m a n ce   o f   t h e  s y s te m   w it h   r esp ec t to   p o w er   u tili za t io n   a n d   ar ea   [ 6 ] .   T h is   p ap er   in tr o d u ce s   a  f o r m al   v er if icatio n   m et h o d   to   v er i f y   th e   m i x ed   s i g n als   b y   tr ain i n g   a n d   lear n i n g   t h e  n et w o r k s   u s i n g   Feed f o r w ar d   n e u r al  n et w o r k   ( FF NN)   a n d   d if f er en tia l  f ed   n e u r al   n et w o r k   ( D FNN) .   T h e  e n tire   p ap er   is   o r g an ized   w ith   t h e  s ec tio n s   lik e   R e v ie w   o f   e x i s ti n g   r esear c h   ( Sectio n   1 . 2 )   to   u n d er s tan d   t h e  cu r r e n t  s tate  o f   ar t  in   t h e  v er i f ic atio n   o f   m ix ed   s i g n als ,   P r o p o s ed   s y s te m   m o d el   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   5 ,  Octo b er   2 0 1 9   :   3 4 2 3   -   3 4 3 1   3424   ( Sectio n   2 )   d is c u s s es  tech n iq u es  ad o p ted   f o r   f o r m a l  v er if ica t io n ,   r es u lts   an d   a n al y s i s   ( Sect i o n   3 )   d ea lin g   w i th   p er f o r m a n ce   a n al y s i s   o f   b o th   t h e  F FNN  a n d   DF NN  tec h n iq u es   an d   co n clu s io n   g i v es   t h e  co n clu d i n g   p o in t s   o f   th e  p ap er   in   (S ec tio n   4) .   T h e  ex is ti n g   r e s ea r ch es  w er e  s elec ted   an d   r ev ie w ed   f r o m   t h e  o f f icial  p u b lica tio n s   l ik e  I E E E ,   Sp r in g er ,   E l s ev ier   m ea n t  w it h   a n alo g ,   m i x ed   s i g n als   v er i f icatio n   ap p r o ac h es.  T h e  co n ce p t  d is cu s s io n   o n   v er if ica tio n   o f   s o f t w ar e  o n   ch ip   ( So C )   in clu d i n g   an alo g   c ir cu itr y   is   ad d r ess ed   in   K u n d er t  an d   C h an g   [ 6 ]   w h ic h   in v o lv e s   t h e  m et h o d i ca l  p r o ce s s ,   a  n ec ess it y   o f   v er if ica tio n ,   i m p le m e n ti n g   a n alo g   v er if ica tio n .   A   m o d elin g   ap p r o ac h   f o r   an al o g / m i x ed   s ig n als   is   f o u n d   i n   Gan g   [ 7 ]   w h ic h   u s es  Ver ilo g   c o d in g .   T h e  w o r k   [ 7 ]   ad o p ted   a   to p - lev el  m et h o d o lo g y   w h ic h   b r in g s   in te g r atio n   o f   s i m u latio n   a n d   m o d elin g   in   t h e  C ad en ce   en v ir o n m e n t.  T h r o u g h   t h i s   m et h o d o lo g y ,   [ 7 ]   ca n   ac h i ev e  ef f icie n t  an d   ac c u r ate  m o d el.   Si m ilar   r esear ch   ad d r ess in g   v er i f icatio n   o f   So C   w it h   a  m i x ed   s ig n al  i s   f o u n d   in   Ya n g   et  al.   [ 8 ]   b y   u s i n g   t h e  Ver ilo g   m o d el.   T h e  d esig n   o f   [ 8 ]   b u ild s   an   e q u iv ale n t  m o d el  o f   h i g h - le v el   r ad io   f r eq u en c y   ( HL R F)  b y   i n teg r at in g   V er i lo g   lan g u a g e  w it h   m i x ed   s ig n al s .   T h e  v er if icatio n   an al y s is   is   p er f o r m ed   b y   u s i n g   d ig ital  m eth o d s   lik e  r an d o m   d ata  g en er atio n ,   m a n u al  v e r if icatio n   m et h o d o lo g y ,   a s s er tio n - b ased   v er if ica tio n ,   a n d   co v er ag e - d r iv e n   v er if ica tio n .   Fro m   th e   an a l y s is ,   it   h a s   b ee n   f o u n d   t h at  [ 8 ]   y ield s   f aster   v er i f icatio n   t h an   o t h er   e x is ti n g   ap p r o ac h es.  A   r esear ch   s u r v e y   ad d r ess in g   e x is t in g   p it f alls   in   f o r m al  v er if icat io n   tec h n iq u es  o f   a n alo g   an d   m i x ed   s i g n als   is   f o u n d   i n   Vid y a  a n d   Ma n j u n at h   [ 9 ] .   T h is   k i n d   o f   v er i f icatio n   is   t h e  cr itica l sta g e  o f   t h e  d esi g n   w h ic h   ass u r es  t h e  cir c u it  d e s ig n   p r ec is e n ess   a n d   its   b e h av io r   w ith   r esp ec t  to   t h e  d esig n   o f   t h e  s y s te m .   T h e  w o r k   [ 9 ]   d is cu s s ed   v ar io u s   asp ec ts   o f   th e  s tan d ar d   tech n iq u es  a n d   m o d els  w h ic h   ex ec u te  ef f ec ti v en e s s   i n   ter m s   o f   ar ea   o f   cir c u it d esi g n .   T h e  w o r k   o f   Har i n ar a y a n a  et   al.   [ 1 0 ]   p r esen ted   an   a u to m a ted   v er if icatio n   m o d el  f o r   m i x ed - s ig n a l   So C s   d esi g n ed   f o r   m o d er n   ap p licatio n   b y   in teg r ati n g   an alo g ,   d ig ital  a n d   m i x ed   s i g n al s .   T h e  v er if icatio n   i s   p er f o r m ed   at  d if f er en t  le v el s   an d   d if f er e n t  m o d es.  A   f r a m e w o r k   b ased   o n   d if f er en tia l  lear n in g   ap p r o ac h   to   p er f o r m in g   t h e  f o r m al   v er i f ic atio n   i s   p r esen ted   in   Vid y a   [ 1 1 ]   b y   co n s id er in g   m i x ed   s i g n als.  T h e  tec h n iq u e   h as  p r esen ted   an   an al y tical  m o d elin g   ap p r o ac h   th at  co n s id er s   an   alg o r it h m   to   g en e r ate  th e  m u lt ip le  m i x ed   s ig n al s   m ea n t   f o r   a  f ea s ib le  o p er atio n   o f   t h e  m i x ed   s ig n al  c ir cu its ,   a n   alg o r it h m   f o r   tr ain i n g   an d   v er i f icatio n .   Fro m   o u tco m e s   an al y s i s ,   it  w as  f o u n d   th at  [ 1 1 ]   ac h iev ed   9 8 . 7 %  ac cu r ac y   w it h   th e  b etter   s p ee d   o f   r esp o n s e   th an   o th er   m ac h i n e  lear n in g   alg o r ith m s . T h e  w o r k   o f   C h itt i  et  al.   [ 1 2 ] ,   p r esen ted   a  u n i q u e  test   m o d el  f o r   d if f er e n t  So C s   i n   w h ich   C ad en ce   v er i f icatio n   m e th o d o lo g y   is   ad o p ted   f o r   th e  So C   e n v ir o n m e n t.  Fro m   t h e   o u tco m e  an al y s is   [ 1 2 ]   f o u n d   an   ef f ec ti v e  r ed u ctio n   i n   s i m u latio n   ti m e  o f   So C   w it h   r esp ec t  to   o th er   ex is tin g   w o r k s .   Si m ilar l y   f o r   ap p licatio n   p r o s p ec tiv e  B o u zian e  et  al.   [ 1 3 ]   p r esen ted   an   o p ti m al  v er i f icatio n   f o r   s p ea k er   m o d eli n g   b y   u s i n g   p er s o n al ized   b ac k g r o u n d   m o d el s .   Si m ilar   k i n d   o f   w o r k   is   f o u n d   in   Ku m ar i  an d   J ay a n n a  [ 1 4 ]   w h ic h   is   m ea n t  f o r   v er if icatio n   o f   li m ited   d ata  s p ea k er s .   Fro m   a  r ev ie w   o f   all  t h e  r ec en t  liter at u r e,   it  h a s   b ee n   o b s er v ed   th at  s ig n i f ica n t  w o r k s   ca r r ied   o n   f o r m al  v er i f icatio n   o f   m i x ed   s ig n al s   b ased   o n   t h e  s o f t w ar e   ap p r o ac h es  ar e  q u ite  r ar e  in   ter m s   o f   h ar d w ar e   ar ch itect u r es.  T h u s ,   r elev a n t  w o r k s   ar e  n ee d ed   to   b e  f o cu s e d   o n   th e  r esear ch   i s s u es  b y   co n s id er in g   h ar d w ar e - b ased   ap p r o ac h es.  On   an al y zi n g   r ec en t   w o r k s   a n al y s is   it   is   b ee n   f o u n d   th a t  v er y   less   w o r k   to w ar d s   th e   an alo g   an d   m ix ed   s ig n al s   f o u n d   w it h   f o r m al  v er i f icatio n   o f   m i x e d   s ig n als.   Mo s t  o f   t h e  r esear ch   w o r k s   h av e   b ee n   ev o lv ed   w it h   in d u s tr ial  ap p licatio n s   p r o s p ec tiv es.  A ls o ,   i n   h ar d w ar e  m o d elin g   p r o s p ec tiv es  s o m e  o f   th e   tech n iq u es  w er e  ad o p ted   f o r m al  v er if ica tio n   tec h n iq u e  w i th   tr ai n in g   o f   m i x ed   s i g n als,  Fu zz y   n et w o r k s ,   etc .   A l s o ,   it  is   b ee n   o b s er v ed   th at  v er y   les s   e m p h a s is   g i v en   f o r   f o r m al  v er i f icatio n   o f   m i x ed   s ig n a ls   in   r ea l - ti m e  s ce n ar io .   E x i s tin g   w o r k s   ar e  lack s   w it h   o p ti m izatio n s   ap p r o ac h es f o r   f o r m al  v er if icatio n   o f   m ix ed   s i g n als  o n   Dig i tal  I C 's  an d   w er e  lag s   w it h   lo w   co s t - e f f ec tiv e  s o l u tio n s   f o r   So C   p latf o r m .   T h u s ,   th er e  is   a  n ee d   o f   “n o ve l   o p timiz ed ,   co s t - effec tive  a p p r o a ch ”       2.   P RO P O SE D  SYS T E M   M O DE L   T h e  p r im e  i n ten tio n   o f   t h i s   w o r k   i s   to   p er f o r m   t h e  f o r m a l  v er if icatio n   o f   m i x ed   s i g n al s   b y   u s i n g   tr ain i n g / L ea r n i n g   n et w o r k s   li k e  d i f f er e n tial   f ed   n e u r al  n et wo r k   ( DFNN)   [ 1 5 ]   o r   Feed f o r war d   n eu r al  n et w o r k   ( FF NN)   [ 1 6 ] .   I n   o r d er   to   d esi g n   t h e  h ar d w ar e  ar c h itect u r e  o f   b o th   tr ain i n g   al g o r ith m s   D FNN  a n d   F FNN  a   b ac k p r o p ag atio n   ( B P )   alg o r ith m   i s   u s ed .   B o th   th e   DFN N  a n d   FF NN  ar e   h a v i n g   p er ce p tr o n   la y er   ar ch itectu r e   w it h   2 - 3 - 1   n et w o r k   t y p e  w h ic h   is   tr ai n ed   b y   b ac k   p r o p ag ati o n   to   u p d ate  th e  w ei g h ts   a n d   r ep r esen t  th e  i n p u t   an d   o u tp u ts .   T h e  m aj o r   o b j ec t iv e  i s   to   i m p le m e n t  th e  h ar d war e  ar ch itectu r e  o f   tr ai n i n g   n e t w o r k s   li k e  D FNN   an d   FF N N  f o r   f o r m a l  v er i f ic atio n   o f   m ix ed   s ig n al s   to   i m p r o v e  th e  p er f o r m a n ce   w it h   h i g h   ac cu r ac y   i n   r ea l   ti m e  ap p licatio n s .   T h e  o v er v ie w   o f   t h e  i m p le m en ted   r esear c h   m eth o d o lo g y   is   g i v e n   i n t h e  f o r m   o f   d esi g n   f lo w   as d escr ib ed   in   F ig u r e  1 .   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   o p timiz ed   meth o d   t o w a r d s   fo r ma l v erif ica tio n   o f m ixed   s ig n a ls   u s in g   d iffer en t ia l fe d   .. .   ( V id ya   D.   S . )   3425   G e n e r a t i o n   o f   M i x e d   S i g n a l   g e n e r a t i o n   +   R a n d o m   n o i s e i m p l e m e n t e d   d e s i g n :   P e r f o r m   à   L e a r n i n g   t e c h n i q u e   D i f f e r e n t i a l   F e d   N e u r a l   N e t w o r k   ( D F N N )   o r   F e e d   f o r w a r d   N e u r a l   N e t w o r k   ( F F N N ) P e r f o r m   f o r w a r d   V e r i f i c a t i o n   M a t l a b   R a n d o m   M i x e d   S i g n a l   g e n e r a t i o n   ( M a t l a b ) R e f e r e n c e   D e s i g n   ( F P G A )   P e r f o r m a n c e   M e a s u r e m e n t     F P G A     Fig u r e  1 .  R esear ch   m et h o d o lo g y   o f   th e  p r o p o s ed   d esig n       T h e  d esig n   f lo w   i n v o l v est w o   d if f er e n t set o f   d esi g n s :   1 )   i m p le m en ted   d esi g n   an d   2 )   r ef er en ce   d esi g n   to   p er f o r m   f o r m al  v er i f icatio n .   T h e  d esi g n   co n s i s ts   o f   m i x ed   s i g n al  g en er atio n   m o d u le   alo n g   w it h   r a n d o m   n o is e  ad d itio n   u s i n g   Ma t lab   w h ic h   is   f o llo w ed   b y   h ar d w a r e  ar ch itectu r e  o f   d i f f er e n tial  f ed   o r   f ee d - f o r w ar d   n eu r al  n et w o r k   m o d el  u s i n g   B ac k p r o p ag atio n   tr ain i n g   m o d el.   T h e  r ef er en ce   d esig n   i n cl u d es  r an d o m   m i x ed   s ig n al  g en er atio n   b y   u s in g   Ma tlab   an d   its   o u tco m e s   w il l  b e  s av ed   as  a  tex t  f ile  an d   th en   f o llo w ed   w i th   r ef er en ce   m o d el  w h i h   co n s i s ts   o f   I P   C o r e  m e m o r y   g e n er atio n   b y   u s i n g   s av ed   te x t   f ile  a s   a  m e m o r y   co ef f icie n t   f i le.   T h e  i m p le m e n ted   d esi g n   an d   r e f er en ce   d es ig n   ar e  m o d eled   b y   R T L   co d i n g   an d   t h e  m o d els   o u tco m es   ar e  co n s id er ed   f o r   f o r m al  v er i f icatio n   b y   u s i n g   eq u iv ale n ce   c h ec k in g .   T h e  p er f o r m an ce   an al y s is   car r ied   o u t  b y   co n s id er in g   h ar d w ar e  co n s tr ain t s   li k e  A r ea ,   p o w er   u t ilizatio n   an d   e v alu a ted   th e  ac c u r ac y   r ate   w it h   er r o r   f i n d in g s .   T h e  f o llo w i n g   d is c u s s io n   w il l  g i v e  t h e   d etailed   ex p lan atio n   o f   t h e  p r o p o s ed   ap p r o ac h   to w ar d s   f o r m al  v er i f icatio n .     2 . 1 .   M ix ed  s ig na l g ener a t io n   T h e  g en er atio n   o f   m u ltip le  m i x ed   s i g n al s   is   i n tr o d u ce d   to   test   th e  f o r m al  v er i f icatio n   w it h   r esp ec t  to   DFNN  o r   FF NN   tr ai n in g .   T h e  g e n er atio n   o f   th e   m i x ed   s i g n al  g e n er atio n   is   p er f o r m ed   b y   u s i n g   M A T L A B   w h ic h   i n clu d es   b o th   an a lo g   an d   d ig ital  f o r m   o f   t h e  s i g n a ls   an d   ar e  c h ar ac ter ized   b y   c u r r en t  a n d   v o lta g e   elec tr ical  f ac to r s .   B ased   o n   t h esec u r r en t  an d   v o lta g e  f ac to r s ,   th e  m ix ed   s i g n als   ar e  ca te g o r ized as  s tab le   o r   u n s tab le  s tate  s ig n al s .   Fu r t h er ,   o n   th e  b asis   o f   h i g h er   an d   lo w er   elec tr ical  f ac to r s ,   th e  m u l tip le  m i x ed   s ig n al s   ar e  g en er ated   an d   ar e  f ea s ib le  f o r   p er f o r m a n ce   a n al y s is .   I n   o r d er   to   g en er ate  th e   m u lt i p le  m i x ed   s i g n al s ,   t h e  ti m e  i n t er v al  o f   t=  0 :2   i s   d ef i n ed   w it h   a  s p ac in g   o f   0 . 0 0 0 5   an d   s am p li n g   f r eq u en c y   o f   f s =  5   Hz.   L ater ,   a  r o u n d   f u n ctio n   ‘ R f '   is   co n s id er ed   to   g en er ate  th e  d at a   s ig n al  w it h   t h e  h elp   s in e   f u n ctio n   a n d   its   o u tco m e  w i ll  b e  r o u n d   o f f   to   n ea r est  h e x ad ec i m al  v al u e.   T h e   tr ain i n g   n et w o r k   i s   d e f in ed   a s   2 - 3 - 1   s tr u ct u r es  to   s ep ar ate   t w o   s i g n als   ar e  f ed   as   o n e   m i x ed   s i g n al  to   th e  n et w o r k .   T h e  ( m i x ed   s i g n al - 1 )   m s 1   ca n   b e  d ef in ed   a s   f o l lo w s .   T h e  d ata  s i g n al  i s   r ep r esen ted   b y   ‘ Ya ’   i s   d ef in ed   as     )) 2 s i n ( 1 1 ( t fs a c R Y f a   ( 1 )     A d d   th e  p s e u d o - r an d o m   n u m b er s   to   th e  d ata  s ig n al  to   f o r m   t h e  m i x ed   s i g n al  M1   is   r ep r esen ted   b elo w     )) , 1 ( 1 . 0 ( 1 a a f Y Rn Y R M     ( 2 )     w h er e  R n   is   n o r m all y   d is tr ib u ted   p s eu d o r an d o m   n u m b er s   w h ic h   g e n er ates  t h e  ‘ Ya '   d ata   s ig n als,  s i m ilar l y ,   f o r   th e  s ec o n d   s ig n al  to   th e  n et w o r k   a s   d ef i n ed   as,     )) 2 s i n ( 2 2 ( t fs a c R Y f b     ( 3 )     )) , 1 ( 1 . 0 ( 2 b b f Y Rn Y R M   ( 4 )     C o n s tan t   v al u e  s et  to   c1   =   5 ,   c2   =  1 5   an d   a m p lit u d e  s e t to   a1   =  4 . 1   an d   a2   =  1 0 .   Hen ce ,   eq u atio n s   ( 2 )   an d   ( 4 )   ar e  co n s id er ed   as  a  s in g le  m i x ed   s i g n al  ‘ m s 1 ’   b y   u s i n g   M1   a n d   M2   r esp ec tiv el y   to   th e  tr ai n i n g   n et w o r k . Si m i lar l y ,   ch a n g e  t h e  am p lit u d es  an d   co n s ta n t s   w it h   d if f er en t  p s eu d o - r an d o m   to   g e n er ate  th e   m u ltip le  m ix ed   s ig n al s .   Gen e r ate  th e  M3   an d   M4   u s in g   ( 2 )   an d   ( 4 )   to   f o r m   t h e  m ix ed   s ig n al  ‘ m s 2 '   u s i n g   d if f er e n t  co n s ta n ts   c3   =   4 ,   c4   =  1 5   an d   a m p lit u d es  a3   =  4   an d   a4   =  5 . 1 .   Si m ilar l y ,   f o r   m i x ed   s i g n a l  ‘ m s 3 ’   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   5 ,  Octo b er   2 0 1 9   :   3 4 2 3   -   3 4 3 1   3426   g en er atio n ,   g e n er ate  t h e  M5   an d   M6 ,   u s in g   eq u atio n s   ( 2 )   an d   ( 4 )   w it h   d i f f er en t  co n s ta n ts   c5 =  5 ,   c6 =5   an d   a m p lit u d es  a5 =4 . 0 5   an d   a 6 = 4 .   T h e  p ea k   v o ltag e  o r   cu r r en t  elec tr ic  f ac to r s   ar e  ch a n g i n g   w i th   r esp ec t  to   a m p lit u d e  v alu e  c h an g es  i n   th e  m ix ed   s i g n a l  g e n e r atio n .   T h e  v ar iatio n   in   t h e  a m p lit u d e  v a lu es  w il l  d ec id e  th e  h ig h   elec tr icit y   o r   lo w   elec tr i cit y   f ac to r .   I f   ad d   m o r e  co m p lex   p s eu d o - r a n d o m   n u m b er   th e  d ata  s ig n al  w il l  b ec o m e  th e   u n s tab le   s tate.   T h e  g en er ated   m u ltip le  m i x ed   s i g n al s   ‘ m s 1 ' ,   ‘ m s 2 ' ,   an d   ‘ m s 3 '   ar e  f ed   to   t h e   tr ain i n g   n et w o r k   i n d iv id u all y   t o   p er f o r m   t h e  f o r m a l v er i f icati o n   f o r   p er f o r m an ce   a n al y s i s .     2 . 2 .   M o du le  f o r  t ra ini ng   T h e  tr ain in g   m o d u le  is   u s ed   to   tr ain   th e  d if f er en t  t y p e s   o f   n e u r al  n et w o r k s   lik e  DF NN  an d   FF NN  f o r   f o r m al   v er i f icatio n   u s i n g   m i x e d   s ig n al s .   T h e  d esi g n   f lo w   o f   t h e  T r a in i n g   m o d u le  i s   r ep r esen ted   i n   F i g u r e  2 .   First  t h e  n et w o r k   t y p e  i s   d ef i n ed   b y   u s i n g   DFNN  a n d   FF N N .   T h en ,   th e  n u m b er s   o f   s a m p l es  ar e  s elec ted   an d   ar e  f ed   to   th e  n et w o r k   f o r m   t h e  g en er ated   m ix ed   s i g n als.  T h en   co n s tr u ct  t h e  n e u r al  n et w o r k s .       G e n e r a t e d   M i x e d   s i g n a l s D e f i n e   t h e   T y p e   o f   N e t w o r k   f o r D F N N   o r   F F N N D e s i g n   t h e   I n p u t ,   H i d d e n   a n d   O u t p u t   l a y e r   a l o n g   w i t h   B P T   D i f f e r e n t i a l   F e e d b a c k D F N N F F N N S a v e   t h e   n e t w o r k   a s   I M D 1   &   I M D 2     Fig u r e  2 .   T h e  d esig n   f lo w   o f   t r ain in g   m o d u le       Fo r   b o th   t h e  D FNN  a n d   F F NN  n e t w o r k s ,   th e   n e t w o r k   s tr u ctu r e   is   f i x ed   2 - 3 - 1 .   T h e  n u m b er   o f   n eu r o n s   to   b e  tr ain ed   is   d ec id ed   b y   th e  n et w o r k   s tr u ct u r e.   T h e  p r o p o s ed   n et w o r k   s tr u ctu r e   in clu d es  t w o   i n p u t   la y er s ,   th r ee   h id d en   la y er s ,   an d   a  s in g le  o u tp u t  la y er   alo n g   w ith   b ac k p r o p ag atio n   tr ai n i n g   ( B P T )   Mo d u le.   Fo r   DFNN  Mo d u le   d if f er en ti al  f ee d b ac k   w ill  b e  f ed   to   all  t h e  t h r ee   la y er s   i n cl u d es  i n p u t,   h id d en   a n d   o u tp u t   la y er s   a n d   also   b ased   o n   t h e   Dif f er en tial  f lo w   t h e  co r r es p o n d in g   o u tp u t   w ill  b e  g e n er ated   to   ea ch   la y er .   T h e  o u tp u ts   o f   th e  DFN N  an d   FF NN  ar e  s av ed   as  an   i m p le m e n ted   d esig n - 1   ( I MD 1 )   an d   im p le m e n ted   d esig n - 2   ( I MD 2 )   r esp ec tiv el y .   T h e  co r r esp o n d in g   D FNN  a n d   FF NN  h ar d w ar e  ar ch itect u r es  ar e  ex p lain ed   i n   b elo w   s es s io n s .     2 . 3 .   F ee d  f o rwa rd  neura l net w o r k   ( F F NN)   T h e  h ar d w ar e   ar ch itect u r e  o f   th e   f ee d - f o r w ar d   n e u r al  n et w o r k   w it h   b ac k p r o p ag atio n   t r ain in g   is   p r esen ted   w i th   a  2 - 3 - 1   n et w o r k   s tr u ct u r e  in   F i g u r e   3 .   E ac h   o f   th e  in p u t  la y er s   r ec ei v es  t h e  in p u ts   f r o m   th e   m u ltip le  m i x ed   s i g n als   li k e  m s 1   o r   m s 2   o r   m s 3 .   E ac h   m ix e d   s ig n al   m s 1   is   h av i n g   t w o   s i g n al s   ar e  in p u ts   to   d in 1   an d   d in 2   in p u t  la y er .   I n   t h e  i n p u t  la y er ,   t w o   in p u t  n o d es  ar e  u s ed ,   ea ch   in p u t  n o d e  is   h av i n g ,   s i n g le  8 - b it   in p u t  d i n 1   an d   t h r ee   w ei g h ts   w 1 ,   w 2 ,   a n d   w 3 .   T h e  t h r ee   m u ltip lier s   ar e  u s ed   to   m u lt ip l y   t h e  d in 1   w i t h   w ei g h ts   w 1 ,   w 2   an d   w 3   to   g en er ate  th e  il1 ,   il2 ,   an d   il3 .   S i m ilar l y   u s e  i n p u t  n o d e2   to   g en er ate  th e  il4 ,   il5 ,   an d   il6 .   T h e  h id d en   la y er   r ec ei v es t h e  s ix   in p u ts   f r o m   th e   in p u t la y er s .   T h e  h id d en   la y er   m a in l y   i n clu d e s   th r ee   s ep ar ate  lin ea r   n eu r o n   m o d el s .   E ac h   lin ea r   n eu r o n   m o d u le  h as  t w o   m u ltip lier s ;  o n e  ca r r y   lo o k   a h ea d   ad d e r   an d   li n ea r   f u n ctio n   u s i n g   L U T   ( L o o k - up - T ab le) .   T h e  1 6 - b it  in p u ts   il1   a n d   il2   ar e  m u lti p lied   w it h   w ei g h t s   w h 1   an d   w h 2   to   g et  th e  p r o d u cts  p 1   an d   p 2   w h ic h   ar e  ad d ed   u s in g   ca r r y   lo o k   ah ea d   ad d er . T h e  ca r r y   lo o k s   ah ea d   ad d er   is   f ast  p ar allel  p r ef ix   ad d er   w h ic h   i m p r o v es  t h e  s p ee d   o f   t h e  h ar d w ar e  b y   r ed u cin g   th e  ti m e   w h ic h   is   d e f i n ed   b y   t h e  ca r r y   b its .   T h e  C L A   o u tp u t s   a r e  in p u t s   to   L UT ,   w h ich   is   a  lin ea r   f u n ctio n ,   r ep r esen ted   in   h ar d w ar e.   T h e  L UT   r ec eiv es  t h e  i n p u t  f r o m   t h e  ad d er ;  b ased   o n   in p u t s   it  i s   ca p ab le  o f   lear n in g   an d   u p d ati n g   th e  f i n al  h id d en   v al u es.  T h e  t h r ee   li n ea r   n e u r o n s   ar e  g e n er ated   t h e  o u tp u t s   h l1 ,   h l2 ,   an d   h l3   w h ic h   ar e  i n p u t  to   t h e  o u tp u t  l a y er .   T h e  o u tp u t  la y er   i s   h av i n g   th r ee   m u ltip lier   a n d   s i g m o i d   m o d el.   T h e  th r ee   in p u t s   ar e  m u ltip lied   w it h   w ei g h ts   w o 1 ,   w o 2 ,   a n d   w o 3   an d   o u tco m e s   ar e  ad d ed   u s in g   ad d er   m o d u le ,   th e  r esu lts   ar e  u s ed   in   th e  s i g m o id   m o d el  to   g e n er ate  th e   f in al  r es u lt s .   T h e  s ig m o id   f u n ctio n   p r o v id es  t h e   b etter   w a y   o f   lear n in g   t h e  w e i g h t s   i n   n e u r al  n e t w o r k s   b y   u s i n g   its   d er iv ati v es   an d   b r in g   n o n lin ea r it y   i n to   t h e   n et w o r k s .   T h e  b ac k p r o p ag atio n   m o d el  is   u s ed   to   p r o v id es th e  tr ain in g   to   th e  al l th e  t h r ee   la y er s   b y   ca lc u lati n g   an d   u p d atin g   th e  n e w   w ei g h ts   in to   it.   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   o p timiz ed   meth o d   t o w a r d s   fo r ma l v erif ica tio n   o f m ixed   s ig n a ls   u s in g   d iffer en t ia l fe d   .. .   ( V id ya   D.   S . )   3427   I n p u t   L a y e r c l k r s t D i n   1 D i n   2 8 8 H i d d e n   L a y e r i l 1 i l 6 i l 5 i l 4 i l 3 i l 2 h l 2 h l 1 h l 3 O u t p u t   L a y e r O u t w 3 w 2 w 1 w h 1 w h 2 w h 3 w o 1 w o 2 w o 3 8 8 8 B a c k   P r o p a g a t i o n   M o d u l e     c l k r s t O u t p u t   L a y e r   i n p u t s H i d d e n   L a y e r   i n p u t s I n p u t   L a y e r   i n p u t s 8 8 8 8 8 8 8     Fig u r e  3 .   Feed f o r w ar d   n e u r al  n et w o r k   ( FF NN)   u s in g   B P T       2 . 4 .   Dif f er ent ia l  f ed  neura l net wo rk   ( DF NN)   T h e  h ar d w ar e  ar ch itect u r e  o f   Dif f er en t ial  f ed   n eu r al  n et wo r k   w i th   D if f er en tial  f ee d b ac k   m o d u le   alo n g   w i th   b ac k p r o p ag atio n   i s   r ep r esen ted   w it h   2 - 3 - 1   n et w o r k   s tr u ct u r e  i n   F i g u r e  4 .   T h e  ar ch itectu r e  is   s i m ilar   to   f ee d   f o r w ar d   n e u r al  n et w o r k   ex ce p t  f o r   d if f er e n tiall y   f ee d b ac k   an d   f e w   c h an g es  i n   th e  d esi g n s .   T h e  Dif f er e n tial  f ee d b ac k   i s   a p p licab le  to   all  th e  th r ee   la y er s . T h e  d in 1   an d   d in 2   ar e  th e  m i x ed   s i g n al s   ap p lied   as  an   i n p u t  to   t h e  in p u t  la y er   an d   g e n er ates  t h e  s i x   d if f er en t  o u tp u ts   il1 ,   il2 ,   il3 ,   il4 ,   il5 ,   an d   il6   alo n g   w i t h   d if f er e n tial   f ee d b ac k .   T h e  s i x   o u tp u t s   ar e  in p u ts   to   t h e  h id d en   la y er .   T h e  h id d en   la y er   i n clu d e s   3 -   d if f er e n t  lin ea r   n eu r o n   m o d el s ,   w h ic h   g en er ate s   t h e  t h r ee   o u tp u t s   h l 1 ,   h l2 ,   an d   h l3   alo n g   w it h   d i f f er en tia l  f ee d b ac k .   T h e  o u tp u t  la y er   h as  3   in p u ts   ar e  m u ltip lied   b y   t h r ee   w ei g h t s   w o 1 ,   w o 2 ,   w o 3 ,   th e  t h r ee   m u ltip lied   o u tco m e s   ar e  o l1 ,   o l2   an d   o l3   ar e   f ee d b ac k   to   th e  d if f er en tial  f ee d b ac k   m o d el  an d   th e  o u tp u t   o f   th e  d if f er en tia l   f ee d b ac k   m o d el  is   i n p u t  to   o u tp u t  la y er   w h ich   i s     f o llo w e d   b y   s i g m o id   f u n ct io n   to   g e n er ate  th e  f i n al  8 - b it   o u tp u t  ‘ o u t ' .       c l k r s t D i n   1 D i n   2 8 8 i l 1 i l 6 i l 5 i l 4 i l 3 i l 2 h l 2 h l 1 h l 3 O u t w 3 w 2 w 1 w h 1 w h 2 w h 3 w o 1 w o 2 w o 3 8 8 8 B a c k   P r o p a g a t i o n   M o d u l e     c l k r s t O u t p u t   L a y e r   i n p u t s H i d d e n   L a y e r   i n p u t s I n p u t   L a y e r   i n p u t s 8 8 8 8 8 8 8 D i f f e r e n t i a l   F e e d b a c k   M o d u l e I n p u t   n o d e - 1 I n p u t   n o d e - 2 L i n e a r   N e u r o n - 1 L i n e a r   N e u r o n - 2 L i n e a r   n e u r o n - 3 M U L - 1 M U L - 2 M U L - 3 S i g m o i d   M o d u l e I n p u t   L a y e r H i d d e n   L a y e r O u t p u t   L a y e r     Fig u r e  4   Dif f er en tia l f ed   n e u r a l n et w o r k   ( DFN N)       T h e  th eo r etica l  co n ce p t  o f   d if f er e n tial  f ee d b ac k   i n   D F NN  is   co n s id er ed   f r o m   [ 1 7 ] ,   b y   u s in g   d if f er e n tial  f ee d b ac k ,   tr ain i n g   w il l  b e  b r o u g h t  d o w n   f o r   th e  n u m b er   o f   iter atio n   o r   s a m p le s .   A cc o r d in g   to   th e   th eo r etica l a s p ec ts   f r o m   [ 1 7 ] ,   th e  f ir s t o r d er   d if f er en tial  f ee d b ac k   w i th   r ed u ce d   la y er s   o u tp u t  w ill b e,     ) ( ) ( 1 1 d b m w i i   ( 5 )     w h er e  w i  is   t h e  w ei g h t s   an d   m i  is   m ix ed   s i g n al  i n p u t s .   T h e  b 1  w ill  b e  an   a u to r eg r es s iv e  te r m   an d   s et  to   1   an d   d 1   is   1 st   o r d er   d if f er en tial.  Fo r   d if f er e n tial  o r d er s   o f   f ee d b ac k ,   a  s et  o f   DFNN  w ill  f o r m   a  m u ltip le  o f   p ar allel   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   5 ,  Octo b er   2 0 1 9   :   3 4 2 3   -   3 4 3 1   3428   s tr u ct u r es.  T h e  p r o p o s ed   DFNN  u s es  t h e  t h r ee   d i f f er e n tial s   o f   2 nd   o r d er   d if f er e n tial  f ee d b ac k ,   f o r   e x a m p le   i n   th e  o u tp u t la y er ,   ( o l 2 - ol 1 ) ,   ( o l 3 - ol 2 )   an d   ( o l 3 - ol 1 ) .   T h e  d if f er e n tial f ee d b ac k   o f   o u tp u t la y er   is   ex p r ess ed   as,     ) ( ) ( ) ( 1 _ 1 3 3 2 3 2 1 2 1 ol ol wo ol ol wo ol ol wo o df   ( 6 )     w h er e  d f _ o l  r ep r ese n ts   th e   2 nd   o r d er   d if f er en tial  f ee d b ac k   o f   o u tp u t   la y er   a n d   w o l ,   w o 2   a n d   w o 3   ar e   u p d ated   w ei g h ts .   T h e  d f _ o l  is   f ee d b ac k   to   o u tp u t  la y er   i s   a n   in p u t;  i n   t h e  o u tp u t  la y er   t h e  s ig m o id   m o d el  g e n er ate  t h e   f i n al  tr ain in g   o u tp u t  b ased   o n   th e  d f _ o l.  T h e  s a m e  co n ce p t  i s   ap p li ca b le  to   th e  o th er   t w o   l a y er s   i n clu d e s   in p u t   an d   h id d en   la y er s . B y   u s in g   t h e  Dif f er e n tial  f ee d b ac k   in   t h e  DFNN,   t h e  tr ai n i n g   ti m e  w ill  b e  r ed u ce d ,   w h ic h   b o o s ts   th e  p er f o r m a n ce   i n   f o r m al  v er if ica tio n .   T h e  h ar d w ar e  co m p lex it y   w i ll  b e  r ed u ce d   w it h   o p ti m izatio n   o f   ar ea   an d   p o w er   t h a n   Feed f o r w ar d   n e u r al  n e t w o r k   ( FF N N ) .   T h e  b ac k - p r o p ag atio n   m o d el  is   u s ed   in   f ee d   d if f er e n tial  f ed   n eu r al   n et w o r k s   to   d eter m i n e  t h e  g r ad ien t  t h at  r eq u ir es   esti m at in g   t h e  weig h ts   to   b e  u s ed   i n   th e  g i v e n   n et w o r k .   B y   u s i n g   th is   m o d el,   ad j u s ti n g   t h e  weig h ts   to   r ed u ce   th e  er r o r   r a te.   T h e  h ar d w ar e  i m p le m en ta tio n   o f   th e  b ac k - p r o p ag atio n   m o d el  in v o l v es  t wo   m aj o r   s tag e s   in c lu d es  p r o p ag atio n   a n d   w ei g h t   u p d atio n .   T h e  p r o p ag atio n   s tag e  in v o l v es  g e n er ati n g   th e  o u tp u t  d ata  in   t h e  n et w o r k   u s i n g   p r o p ag a tio n   f o r w ar d .   B ased   o n   th e  T ar g et   tr ain in g   n et w o r k ,   th e  p r o p ag atio n   o f   th e  ac ti v atio n s   b ac k   th r o u g h   t h e  n e u r al   n et w o r k   to   ca lc u late  t h e   d if f e r en ce   u s i n g   tar g e ted   o u tp u t  a n d   ac t u al  o u tp u t   f r o m   all   t h e  la y er s .   T h e  w e ig h t   u p d ate  s ta g e  i n v o l v es  th e  w e ig h t ' s   d i f f er en ce ,   a n d   la y er s   ac tiv atio n   is   m u lt ip lied   to   g e n er ate  t h e  u p d ated   w ei g h t.  T h e  lear n i n g   r ate  i m p ac ts   t h e  q u a lit y   a n d   s p ee d   o f   t h e   tr ain i n g   n et w o r k .   T h e  l ea r n in g   r ate   ‘ L r ’   is   d ef in ed   w it h   o n e.   I f   L r   is   m o r e,   n eu r o n   tr ain i n g   w il l  b e  f ast,  an d   if   it  is   les s ,   n eu r o n   tr a in i n g   w il l  b e  m o r e   ac cu r ate.   C o n s id er   all  t h e  la y er s   in p u ts   i n cl u d e  i n p u t,  h id d en ,   an d   o u tp u t  la y er s   ad d   la y e r - w is e  in d i v id u al l y ,   an d   th e  ad d ed   o u tp u ts   ar e  s et  o p 1 ,   o p 2 ,   an d   o p 3   r esp ec tiv ely .   On ce   t h e  p r o p ag atio n   s tar ts ,   r eset  all  th e  la y er s   w ei g h ts   a n d   in itialize  to   ze r o   an d   Up d ate  th e  m e m o r y   w it h   ac tu al  d ata  w it h   t h r ee   ad d r ess   lo ca tio n   f o r   th r ee   la y er s .   T h e  m e m o r y   w ill  b e  u p d ated   b ased   o n   th e  co u n ter .   T h e  d if f er en ce   Di '   w ill  b e  ca lcu lated   u s in g   t h e   ac tu al  d ata  w h ic h   i s   u p d ated   f r o m   m e m o r y   i s   s u b tr ac ted   b y   o u tp u t la y er   o u tp u t ‘ O p . '   I f   th e  Dif f er en ce   ‘ D i '   w il l  b e  less   th a n   m e m o r y   ac tu al   d ata  an d   co u n ter   i s   t w o ,   a  c o u n ter   w ill  b e  r e s et  to   ze r o   o th er w is e  it  w i ll  b e   in cr e m e n t  till   r ea c h es   t w o   an d   a  v al id   s i g n a l  w il l b e  u p d ated .   T h e  Dif f er en t la y er s   I n p u ts / o u tp u t s   ‘ D o ’   w i ll b e   u p d ated   b ased   o n   t h e  la y er - wis e.   Fo r   o u tp u t  la y er   w eig h t   u p d atio n ,   o p 1 ,   o p 2   an d   o p 3   w i ll  b e  co n s id er ed   as   ‘D o . '   Fo r   i n p u t   an d   h id d en   la y er   w ei g h t  u p d atio n ,   m ix ed   s ig n als  w ill  b e  t h e  ‘ Do . '   T h e  w ei g h t   u p d atio n   w ill  b e   d ef in ed   as   b elo w :     Up d ated   W eig h t =   )) 1 ( ( Op Op Do Di Lr I w   ( 7 )     Fro m   t h e  eq u atio n   ( 7 )   w h er e  th e  I w   i s   i n itial   w ei g h t s ,   T h e  O p   w ill  b e  d e f in ed   b ased   o n   t h e  la y er s   o u tp u t  Fo r   O u tp u t  la y er ,   O p   will  b e  u p d ated   s a m e  a n d   f o r   in p u t  an d   h id d en   la y er s ,   th e  o p 1 ,   o p 2 ,   an d   o p 3   w il l   b e  co n s id er ed   as ‘ O p .'     2 . 5 .   M o du le  f o r  f o rm a l v er if ica t io n   T h e  f o r m al  v er i f icatio n   is   v er i f icatio n   tec h n iq u e  w h ic h   a g r ee s   o r   d is ag r ee s   o n   t h e  q u alit y   o f   r elate d   alg o r ith m s   o r   m o d els  w it h   r es p ec t  to   s u i tab le  f o r m al  m et h o d s   o r   m o d els  o r   ex ac t  s p ec i f ic atio n s   in   h ar d w ar e   an d   s o f t w ar e  v ie w p o in t.  I n   p r o p o s ed   d esig n   u s es   s u itab le  m o d el s   to   test s   th e  f o r m al  v e r if icatio n s   o f   m i x ed   s ig n al s .   T h e  f o r m al  m o d eli n g   in v o l v es   th e  f o r m a l  eq u i v ale n ce   ch ec k in g ;  it   is   p r o ce s s ed   a n d   u s ed   d u r in g   t h e   d esig n   an d   d ev elo p m e n t  o f   d i g ital  I C 's,  to   p r o v e  f o r m a ll y   t h at  th e  t w o   m o d el s   o f   th e  d esi g n s   r ev ea l  t h e  s a m e   b eh av io r .   T h e  f o r m al  v er if ica t io n   o f   m i x ed   s ig n al s   is   ca r r ied   o u t  u s i n g   tr ai n i n g   n et w o r k s   D FNN  a n d   FF NN  to   f i n d   s its   ac c u r ac y ,   an d   it s   t y p i ca l  d esig n   f lo w   i s   r ep r esen ted   in   F i g u r e  5 .   T h e  co m p lete  f o r m al  v er i f icatio n   i s   d o n e  b ased   R T L - RT L   m o d eli n g   v er i f icat io n   w h ic h   is   d o n e   th r o u g h   eq u iv ale n ce   c h ec k i n g .   T h e  eq u i v ale n ce   ch ec k i n g   co n tai n s   t w o   m ai n   m o d el s   n a m el y   i m p le m en ted   d esig n   an d   r ef er en ce   d esig n .   Hen ce ,   n ee d   to   v er if y   b o th   th e  m o d els  o f   th e  d esi g n s   ex h ib it s   th e  s a m e  f ea t u r es.  Fo r   an al y s is   p u r p o s e,   T h e  DFNN  n et w o r k   s a v ed   as   I m p le m e n ted   d esig n - 1 ( I MD 1 )   an d   FF NN  Net w o r k   s a v ed   as   I m p le m e n ted   d esig n - 2   ( I MD 2 )   as  a  tr ain ed   d ata .   T h e  im p le m e n ted   d esig n s   I M D1   an d   I MD 2   ar e  d esig n ed   with   a  h ar d w ar e  ar ch itect u r e  o f   DFNN  an d   F FNN   r esp ec tiv el y .   Fi g u r e   5   s h o w s   t h e  r ef er e n ce   m i x ed   s i g n al   g e n er atio n   w h ich   is   s i m ilar   to   i m p le m en ted   d es ig n s ,   b u t  h er e  r an d o m ize  m o r e  w i th   p s eu d o   n u m b er s   to   f o r m   th e  m ix ed   s i g n als  f o r   f o r m al   v er if icat io n   w it h   d if f er e n t  in p u ts   f u n ct io n alit y .   T h e  DFNN  r ed u ce   th e  tr ain in g   t i m e  i n t er n all y   w h ile  p r o ce s s i n g   t h e  f o r m al   v er if ica tio n   o f   m i x ed   s i g n als.   T h e  o u tp u t   o f   r e f er en ce   r a n d o m l y   g e n er ated   m i x ed   s ig n a ls   ar e  c h ec k i n g   t h e   eq u iv ale n ce   w it h   tr ain ed   i m p l e m en ted   d esig n   o u tco m es to   ch ec k   t h e  ac cu r ac y .       Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   o p timiz ed   meth o d   t o w a r d s   fo r ma l v erif ica tio n   o f m ixed   s ig n a ls   u s in g   d iffer en t ia l fe d   .. .   ( V id ya   D.   S . )   3429   G e n e r a t i o n   o f   R e f e r e n c e   M i x e d   s i g n a l   w i t h   n o i s e S t o r e   t h e   r e f e r e n c e   o u t p u t   m i x e d   s i g n a l s   i n   B l o c k   R A M   I P   C o r e S a v e   a s   R D 1   f o r   D F F N   a n d   R D 2   f o r   F F N N P e r f o r m   t h e   f o r m a l   V e r i f i c a t i o n   u s i n g   E C E x t r a c t   t h e   s a v e d   N e t w o r k   I M D 1   &   I M D 2 E v a l a v a t e   t h e   p e r f o r m a n c e   a n a l y s i s R e f e r e n c e   D e s i g n     Fig u r e  5 .   T y p ical  d esig n   f lo w   o f   f o r m al  v er i f icatio n       T h e  r ef er en ce   d esig n   i n clu d e s   th e  r ef er en ce   m i x ed   s i g n al s   g en er atio n   is   d o n e  b y   u s in g   M atlab   w it h   n o is e  w h ic h   is   s i m ilar   to   i m p l e m en ted   d esi g n   m ix ed   s i g n al   g en er atio n .   T h e  o u tp u t  o f   r e f e r en ce   m ix ed   s i g n a ls   is   s to r ed   in   th e  tex t  f ile.   W h i ch   is   h a v i n g   ar o u n d   4 0 0 0   s a m p les  an d   ea ch   s a m p le  is   8 - b it  an d   s to r es  th ese   s a m p les   as   a  co ef f icie n t  f i le  ( . co e)   in   I P   C o r e  b ased   B lo ck   R A M  Mo d el  w h ic h   i s   h av i n g   th e  r e f er en ce   o u tp u t   s ig n al s .   Sa v e  t h e   r ef er en ce   d e s ig n   m o d el  h as   R D1   f o r   DFN N  an d   R D2   f o r   F FNN.   T h i s   i m p le m e n ted   d e s ig n   I MD 1   an d   r ef er en ce   d esig n   R D1   ar e  test ed   f o r   f o r m a l  v er if icatio n   b y   u s i n g   eq u i v alen ce   c h ec k i n g .   I n   eq u i v ale n ce   ch ec k i n g ,   b o th   th e  I MD 1   a n d   R D1   ar e  m atc h ed   w it h   s a m e  f ea t u r es,  t h e n   co n s id er   th e   f o r m al   v er if ica tio n   is   " s u cc ess f u l"   if   t h e  f ea t u r es  ar e  n o t  m atc h ed   it   is   " u n s u cc e s s f u l,"   u s e   a  co u n t er   m et h o d   to   ch ec k   th e  er r o r s   in   th e  m o d els.T h e   ac cu r ac y   o f   t h e  f o r m al  v er if icat io n   m o d els  w il l  f i n d ,   if   b o th   t h e  m o d el ' s   f ea t u r e s   ar e  s a m e,   th e n   co u n ter   is   r ese t  to   ze r o .   I f   n o t,  co u n ts   s tar t  co u n ti n g ,   w h e n   b o th   th e  I MD 1   an d   R D1   s a m p led   d ata  ar e  n o t  m atc h i n g   till   t h e   last   s a m p les.  B ased   o n   t h e  c o u n t,  th e   ac cu r ac y   w i ll  b e  ca lcu lated   f o r   f o r m al   v er if ica tio n .   I n   o r d er   to   p er f o r m   th e  p er f o r m a n ce   an al y s i s ,   f o r m al  v er if ica tio n   o f   m i x ed   s i g n al s   u s in g   DFNN   is   co m p ar ed   w ith   t h e  FF NN   tr ain in g   m et h o d .   T h e  p r o p o s ed   f o r m al  v er i f icatio n   o f   m ix ed   s ig n al s   u s i n g   d if f er e n tial  f ed   n e u r al  n et wo r k   p r o v id es  b etter   p er f o r m an ce   in   ter m s   o f   ac cu r ac y   an d   less   h ar d w ar e   co m p le x it y   o v er   th e  Feed f o r w ar d   n e u r al  n et w o r k .   T h e  p e r f o r m an ce   a n al y s is   o f   b o th   th e  d esig n s   w il l  b e  ex p lain ed   i n   th e  n ex t sectio n .       3.   RE SU L T   AND  DI SCUS SI O N   T h e  p r o p o s ed   Fo r m al  v er if ic atio n   o f   m u ltip le  m i x ed   s i g n als  u s i n g   tr ain i n g   alg o r it h m s   in cl u d es   Feed f o r w ar d   Ne u r al  Ne t w o r k   ( FF NN) ,   a n d   Di f f er en tia ll y - Fed   Neu r al  Net w o r k   ( D FNN )   o f   2 - 3 - 1   n e t w o r k     R es u lts   ar e  an a l y ze d   i n   th e  b elo w   s ec t io n .   T h e  p r o p o s ed   w o r k   i s m o d eled o v er   Xili n x   I SE  1 4 . 7   en v ir o n m e n t   u s i n g   Har d w ar e  lan g u ag e  V er ilo g - H DL   a n d   w a v e f o r m   s i m u lated   u s i n g   Mo d elsi m   6 . 5   s im u lato r   an d   i m p le m en ted   o n   A r ti x - 7   FP G A . T h e  s y n t h esized   r es u lts   o f   p r o p o s ed   d esig n s   F FNN  an d   DFN N  w h ic h   ar e  tab u lated   in   T ab le  1 .   E ac h   d e s ig n   i n clu d e s   b o th   i m p le m e n t ed   an d   r ef er en ce   d esi g n   f o r   f o r m al  v er i f icatio n   o f   m i x ed   s i g n als.T h e  r eso u r ce   u tili za t io n   i n cl u d es  3 3 4   s lice s   L UT ' s   o f   DFNN   o v er   3 5 7   o f   FF NN   w it h   a n   i m p r o v e m en t o f   n ea r l y   7   %.  T h e  o th er   r eso u r ce   u t ilizatio n   in   b o th   d esig n s   is   al m o s t t h e  s a m e.         T ab le  1 .   Dev ice  u tili za tio n   o f   t h e  p r o p o s ed   DFNN  alo n g   w it h   FF N N  f o r   f o r m a l v er i f icatio n   L o g i c   U t i l i z a t i o n   F F N N   D F N N   N u mb e r   o f   S l i c e   R e g i st e r s   1 9 5   2 0 3   N u mb e r   o f   S l i c e   L U T s   3 5 7   3 3 4   N u mb e r   o f   f u l l y   u se d   L U T - F F   p a i r s   1 2 2   1 2 4   N u mb e r   o f   b o n d e d   I O B s   48   48   N u mb e r   o f   B l o c k   R A M / F I F O   2   2   N u mb e r   o f   D S P 4 8 E 1 s   39   39       T h e  p o w er   u tili za tio n   o f   DF NN  an d   F FNN  f o r   f o r m al  v er if icatio n   o f   m i x ed   s i g n als  i s   an al y ze d   u s i n g   X - P o w er   a n al y ze r   to o l  f r o m   Xili n x   I SE.   T h e  T o ta l  p o w er s   co n s u m ed   b y   t h e  DFNN  a n d   FF NN   n et w o r k s   ar e  0 . 1 1 2 W   an d   0 . 1 1 7 W   r esp ec tiv el y   w it h   an   i m p r o v e m en t  o f   5 %.  T h e  d y n a m ic  p o w er   u ti lizatio n   o f   b o th   DFNN  a n d   FF NN  n et w o r k   i s   0 . 0 3 0 W   an d   0 . 0 3 5 W   r esp e ctiv el y   w h ich   ar e  tab u la te d   i n  T ab le  2 .   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   5 ,  Octo b er   2 0 1 9   :   3 4 2 3   -   3 4 3 1   3430   T ab le  2 .   P o w er   co n s u m p tio n o f   th e  p r o p o s ed   DFNN  alo n g   with   F FNN  f o r   f o r m al  v er i f icati o n   T o t a l   P o w e r   su mm a r y   F F N N   D F N N   T o t a l   P o w e r   ( W )   0 . 1 1 7   0 . 1 1 2   D y n a mi c   P o w e r   ( W )   0 . 0 3 5   0 . 0 3       T h e  m a x i m u m   o p er atin g   f r e q u en c y   is   o b tain ed   f r o m   A r t ix - 7   FP GA   f o r   th e  DFNN,   an d   FF NN   n et w o r k s   ar e  5 9 . 2 5 2   MH z  an d   3 7 . 6 0 5   MH z  r esp ec tiv ely   with   a n   i m p r o v e m e n t  o f   3 6 . 5 4   %  w h ic h   i n d icate s   th at  DF NN  w o r k s   a t  a  h i g h er   o p er atin g   r ate  th a n   t h e  FF N N  Mo d u le.   T h e  p r o p o s ed   w o r k   tar g et s   to   ai m   f o r   f o r m al  v er i f icatio n   o f   m u ltip l e  m i x ed   s i g n als  u s in g   tr ai n ed   n et w o r k s   li k e  DF NN  a n d   FF NN.   T h e  h i g h er   r ate   o f   ac cu r ac y   f r o m   t h e  tr ai n ed   o r   lear n in g   n et w o r k   i s   a  p r im e  p er f o r m an ce   p ar a m eter   f o r   f o r m al  v er if ica tio n . T h e  an al y s is   o f   f o r m al  v er i f icatio n   is   d o n e  b y   e q u iv ale n ce   c h ec k i n g   f o r   b o th   DFNN  a n d   FF NN   d esig n s .   E ac h   d esi g n   is   h av i n g   i m p le m e n ted   ( R T L )   an d   r ef er en ce   ( R T L )   Mo d u les  an d   b y   u s in g   t h eir   d esig n   o u tp u ts ,   c h ec k   it   is   eq u i v alen t ,   if   y es,  t h e n   t h e  v er if icatio n   i s   1 0 0 %  s u cc e s s f u l.  I f   n o t,  I f   i t  is   d i f f er en t  u s in g   eq u iv ale n ce   ch ec k i n g   w i th   a  co u n ter   m e th o d   to   f in d   o u t  th e  er r o r s   t o   g et  th e  ex ac t  ac cu r ac y   o f   t h e  tr ain e d   n et w o r k .   T o   f i n d   a n   ac c u r ac y   o f   tr ai n in g   m e th o d s   lik e   F FN N  an d   DFNN   f o r   f o r m a l  v er if icatio n ,   t h e  a n al y s i s   is   c ar r ied   o u t  o v er   m u ltip le   te s t  e n v ir o n m e n t s   b y   c h a n g in g   th e  n et w o r k   t y p e  o r   a  n u m b er   o f   s a m p les   w h ich   f ee d   to   th e  in p u t  la y er s   as  m u ltip le  m i x ed   s i g n al s .   T h e  i m p le m en ted   d esi g n s   co n tai n   co m p lete  h ar d w ar e   ar ch itect u r e  o f   DFNN  o r   FF N N  w h ic h   is   f ed   b y   s ep ar ate   m ix ed   s i g n al s   as  an   i n p u t  to   th e  to p   im p le m en ted   d esig n   ar ch i tectu r e,   f o llo w e d   b y   th r ee   h id d en   la y er s   a n d   s i n g le  o u tp u t   la y er   g i v e s   t h e  f in a l  r es u lt s .   T h e  r ef er en ce   d esig n   co n tain s   ac tu al  tr ai n ed   d ata  w h ic h   i s   o b tain ed   f r o m   th e  m i x ed   s i g n al  g e n er atio n   b y   Ma tlab   th en   s to r e  it  in   B lo ck   R A M  I P   co r es  w h ich   g iv e s   co m p lete  r ef er e n ce   m o d el. I n   DFNN  T r ain in g   m o d u le,   d if f er e n tial  f ee d b ac k   w h ic h   is   g e n er ated   f r o m   th e  o u tp u t  la y er   an d   f ed   b ac k   to   th e  o u tp u t  la y er   as   o n e  o f   th e  i n p u t s   w h ich   i m p r o v es t h e  tr ain i n g   ti m e  a n d   ac cu r ac y   o f   th e  tr ai n i n g   n et w o r k .   T h e  f o r m al  v er i f icatio n   o u tc o m e s   w i th   an   ac cu r ac y   o f   m u ltip le  m i x ed   s i g n als   ar e  r ep r esen ted   i n   F ig u r e  6 .   T h e  p r o p o s ed   DFNN  o v er   FF NN  tr ai n i n g   tech n i q u e  f o u n d   t h e  b etter   a v er ag e   ac cu r ac y   o f   t h r ee   m i x ed   s ig n al s .   I n   t h at  m ix ed   s ig n al - 3   g i v es  h i g h e s t  ac cu r ac y   r ate  o f   9 8 . 9 7   %  u s in g   DF N N  o v er   9 5 . 9 5   %  o f   FF NN  w it h   i m p r o v e m e n t s ,   wh en   co m p ar ed   to   o th er   t w o   m ix ed   s i g n als.  T h e  f o llo w i n g   T ab le. 3   in d icate s   t h e   o u tco e m s   o f   tr ai n ed   n et w o r k .   I t is o b s er v ed   th at,   t h e  a v er ag e   ac cu r ac y   o f   th r ee   m i x ed   s i g n a ls   u s i n g   D FNN  f o r   f o r m al  v er i f icatio n   i s   9 7 . 5 5   %.  Si m ilar l y   f o r   FF NN,   t h e  9 3 . 9 6 %  is   th e  a v er ag e   ac cu r ac y   o f   t h r ee   m ix ed   s ig n al s   w h ile  p er f o r m i n g   f o r   f o r m al  v er if ica tio n ,   w h ic h   clea r l y   in d icate s   t h at  DFNN  tr ain i n g   n et w o r k   w h ic h   g iv e s   b etter   o u tco m e s   an d   s at is f ac to r y   o v er   FF NN  tr ai n i n g   n et w o r k   w it h   a n   i m p r o v e m e n t   o f   n ea r l y   3 . 7 %  o f   ac cu r ac y   a n d   w h ic h   i s   ap p licab le  to   d o   f o r m al  v e r i f icatio n   in   s y s te m   o n   c h ip   lev el,   a n d   also   f o r   co m p le x   d ig ital  m o d elli n g   v er i f icatio n .           Fig u r e  6 .   Fo r m a l v er i f icatio n   o u tco m es  w i th   a n   ac cu r ac y   o f   m u ltip le  m ix ed   s i g n als       4.   CO NCLU SI O N     Th is   p ap er   h as  p r esen ted   a  co s t - e f f ec tiv e,   o p ti m ized   s o l u tio n   to   f o r m al  v er if ica tio n   o f   m u ltip le   m i x ed   s i g n als   u s i n g   DFN N  o v er   FF NN   o n   th e   h ar d w ar e  p lat f o r m .   I n   o r d er   to   r ed u ce   t h e  c o m p le x it y   o f   m i x ed   s ig n al s   in   SO C   d esig n   lev el,   f o r m al  v er i f icatio n   is   b est - s u i ted   s o lu tio n s   to   i m p r o v e  t h e  ac cu r ac y   o v er   er r o r   r ate  T h e  p r o p o s ed   d esig n s   g i v es  th e  s o lu tio n s   to   th e  c h allen g es  is   v er if icat io n   ac r o s s   SO C   f o r   m u ltip le  m ix ed   s ig n al s .   T h e  p r o p o s ed   w o r k   i s   d esig n ed   o v er   a  d if f er en tiall y   f ed   n eu r al  n et w o r k   ( DF NN)   w h ic h   p r o v id es  th e  o p tim a l  s o lu tio n s   f o r   p er f o r m i n g   f o r m al  v er if icatio n   o f   d if f er e n t  t y p e s   o f   m ix ed   s i g n als.  T h e  p r o p o s ed   Fo r m al  v er i f icatio n   m o d el   o f   th e  b o th   DF NN  a n d   F FNN   T r ain in g   m o d u le s   in cl u d es   Mu l tip le  Mix ed   s i g n a l   8 8 . 0 0 % 9 0 . 0 0 % 9 2 . 0 0 % 9 4 . 0 0 % 9 6 . 0 0 % 9 8 . 0 0 % 1 0 0 . 0 0 % M i x e d si g n a l - 1 M i x e d si g n a l - 2 M i x e d si g n a l - 3 A v e r a g e A c c u r a c y Acc ura cy FF NN DFNN Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   o p timiz ed   meth o d   t o w a r d s   fo r ma l v erif ica tio n   o f m ixed   s ig n a ls   u s in g   d iffer en t ia l fe d   .. .   ( V id ya   D.   S . )   3431   g en er atio n s ,   I m p le m e n ted   d esi g n   u s i n g   DFN N  o r   FF N N,   b o th   th e    R ef er e n ce   Desi g n s   a n d   f o r m al  v er if ica tio n   u s i n g   eq u i v ale n ce   c h ec k in g .   T h e  R T L - R T L   v er i f icatio n   is   d o n e  f o r   b o th   th e   n et w o r k s .   T h e  c h ip   le v el   co n s tr ain ts   i m p r o v e m e n t  d o n e   b y   u s in g   DFN N  w h ic h   in cl u d es  ar ea   o p tim ized   b y   n ea r l y   7 %  in   ter m s   o f   Sli c e  L UT ' s ,   T o tal  p o w er   co n s u m p t io n   o n - ch ip   lev el   is   n ea r l y   5   %  an d   o p er atin g   f r eq u en c y   o f   n ea r l y   3 6   %  o v er   FF NN.   T h e  p er f o r m an ce   o f   D FNN  in   ter m s   o f   ac cu r ac y   i m p r o v e m e n t is 3 . 7 % o v er   FF NN.       RE F E R E NC E S     [1 ]   R.   E.   Bry a n t,   e t  a l . ,   “ L im it a ti o n s  a n d   c h a ll e n g e s  o f   c o m p u te r - a id e d   d e sig n   tec h n o lo g y   f o r  CM OS  V L S I ,”   Pro c e e d in g s  o f  t h e   IEE E ,   v o l/ iss u e :  89 ( 3 ),   p p .   3 4 1 - 3 6 5 ,  2 0 0 1 .   [2 ]   M .   S .   Er d e n ,   e t  a l . ,   “ A   re v ie w   o f  f u n c ti o n   m o d e li n g :  A p p r o a c h e s  a n d   a p p li c a ti o n s ,”   Ai   E d a m ,   v o l/ i ss u e :   22 ( 2 ),   p p .   147 - 1 6 9 ,  2 0 0 8 .   [3 ]   M .   H.  Zak i,   e t  a l . ,   “ F o rm a l  v e ri f i c a ti o n   o f   a n a lo g   a n d   m ix e d - sig n a l  d e sig n s:  A   su rv e y ,”   M icr o e le c tro n ics   jo u r n a l ,   v o l/ issu e :  39 ( 12 ),   p p .   1 3 9 5 - 1 4 0 4 ,  2 0 0 8 .   [4 ]   B.   W ielin g a   a n d   G .   S c h re ib e r ,   “ Co n f ig u ra ti o n - d e sig n   p r o b lem   so lv in g ,”   IEE E  Ex p e rt ,   v o l/ issu e :  12 ( 2 ),   p p .   49 - 56 ,  1 9 9 7 .   [5 ]   S. G u p ta,  e t  a l . ,   “ T o w a rd s f o r m a l   v e ri f ica ti o n   o f   a n a lo g   d e sig n s ,”   Pro c e e d in g s  o f  th e   2 0 0 4   I EE E/ AC M   In ter n a ti o n a l   c o n fer e n c e   o n   C o mp u ter - a i d e d   d e sig n .   I EE E  C o mp u ter   S o c iety ,   2 0 0 4 .   [6 ]   K.  Ku n d e rt   a n d   H .   Ch a n g ,   “ Ve rify in g   a ll   o f  a n   S OC - a n a lo g   c ircu it ry   in c lu d e d ,”   IE EE   S o li d - S t a te  Circ u it s  M a g a zin e ,  v o l/ issu e :  1 ( 4 ),   2 0 0 9 .   [7 ]   P.  G a n g ,   “ B e h a v io ra l  m o d e li n g   a n d   sim u latio n   o f   a n a lo g /m ix e d - si g n a l  s y ste m s  u sin g   v e ril o g - ams ,”   In fo rm a t io n ,   Co mp u t in g   a n d   T e lec o mm u n ic a ti o n ,   2 0 0 9 .   Y C - IC T '0 9 .   IEE E  Y o u t h   Co n fer e n c e   o n .   IE EE ,   2 0 0 9.   [8 ]   X .   Ya n g ,   e t   a l . ,   “ M ix e d - sig n a l  sy ste m - on - a - c h ip   (s o c )  v e rif ica ti o n   b a se d   o n   sy ste m v e ril o g   m o d e l ,”   S y ste m  T h e o ry   ( S S S T ),   2 0 1 3   4 5 th   S o u t h e a ste rn   S y mp o siu m  o n .   IEE E ,   2 0 1 3 .   [9 ]   V id h y a   D.   S .   a n d   M .   Ra m a c h a n d ra ,  “ Re se a r c h   T re n d s  in   F o rm a l  Ve rif ic a ti o n   P r o c e ss   f o r   A n a lo g   a n d   M ix e d   S ig n a l   De sig n , ”   In ter n a ti o n a l  J o u rn a l  o f   Co mp u ter   Ap p li c a t io n s ,   v ol /i ss u e :   1 0 9 ( 11 ) ,   Ja n   2 0 1 5 .   [1 0 ]   G .   S .   Ha rin a ra y a n ,   e t  a l . ,   “ A u to m a ted   F u ll   Ch i p   S P ICE  sim u latio n s  w it h   se lf - c h e c k in g   a ss e rti o n s  f o r  las t  m il e   v e ri f ica ti o n   &   f irst  p a ss   S il ico n   o f   m ix e d   sig n a l  S o Cs ,”   S y ste m - on - C h ip   C o n fer e n c e   ( S OCC),  2 0 1 6   2 9 th   IE EE   In ter n a t io n a l .   IEE E,   2 0 1 6 .   [1 1 ]   V id h y a   D.  S .   a n d   M .   Ra m a c h a n d ra ,   “ A  No v e l  D e sig n   in   F o rm a l  V e rif ica ti o n   Co rre sp o n d i n g   to   M ix e d   S ig n a ls  b y   Diff e r e n ti a l  L e a rn in g ,”   Co mp u ter   S c ien c e   On - li n e   Co n fer e n c e .   S p ri n g e r,   Ch a m ,   2 0 1 7 .   [1 2 ]   S.  Ch it ti ,   e t  a l . ,   “ A   Un iq u e   T e st   Be n c h   f o r  V a rio u s  S y ste m - on - a - Ch i p ,”   I n ter n a ti o n a l  J o u r n a l  o f  El e c trica l  a n d   Co mp u ter   E n g in e e rin g   ( IJ ECE ) ,   v o l/ issu e :  7 ( 6 ),   p p .   3 3 1 8 - 3 3 2 2 ,  2 0 1 7 .   [1 3 ]   A .   Bo u z ian e ,   e t  a l . ,  “ T o w a rd s  a n   Op ti m a l  S p e a k e r  M o d e li n g   i n   S p e a k e r  V e rif ica ti o n   S y ste m s  u sin g   P e rso n a li z e d   Ba c k g ro u n d   M o d e ls , ”   In ter n a ti o n a l  J o u r n a l  o f  El e c trica l  a n d   Co mp u ter   En g i n e e rin g   ( IJ ECE ),   v ol /i ss u e :  7 ( 6 ) ,  p p .   3 6 5 5 - 3 6 6 3 ,  De c   2 0 1 7 .   [1 4 ]   T .   R.   J .   Ku m a rian d   a n d   H.   S .   J a y a n n a ,   “ L i m it e d   Da ta  S p e a k e r  V e rif ica ti o n :  F u si o n   o f   F e a tu re s , ”   In ter n a ti o n a l  J o u rn a l  o f  El e c trica l  a n d   C o mp u t e r E n g i n e e rin g   ( IJ ECE ),   v ol /i ss u e :   7 ( 6 ) ,  p p .   3 3 4 4 - 3 3 5 7 ,  De c   2 0 1 7 .   [1 5 ]   M.  W o jcie c h o w sk i,   “ S o lv in g   d iff e re n ti a l  e q u a ti o n s  b y   m e a n s  o f   fe e d - f o r w a rd   a rti f icia l  n e u ra l  n e tw o rk s ,”   In ter n a t io n a l  C o n fer e n c e   o n   Arti f icia l  In telli g e n c e   a n d   S o ft   C o mp u ti n g .   S p rin g e r,  Ber li n ,   He id e lb e rg ,   2 0 1 2 .   [1 6 ]   J.  Ilo n e n ,   e t  a l . ,   “ Dif fe re n ti a l  e v o lu ti o n   trai n in g   a lg o rit h m   f o r  f e e d - f o rwa rd   n e u ra l  n e tw o rk s ,”   N e u ra l  Pro c e ss in g   L e tt e rs ,   v o l/ issu e :   17 ( 1 ) ,   p p .   93 - 1 0 5 ,  2 0 0 3 .   [1 7 ]   M a n ju n a th   R . ,  e t  a l . ,   “ Diff e r e n ti a l  lea rn in g   a lg o rit h m   f o r  A rti f i c ial  Ne u ra l  Ne t w o rk s , ”   In ter n a ti o n a l  J o u r n a l  o f   Co mp u ter   A p p li c a ti o n s ,  v o l /i ss u e :   1 ( 1 ) ,   p p .   65 - 7 0 ,   F e b   2 0 1 0 .       B I O G RAP H I E S   O F   AUTH O RS          V id h y a . D.S .   is  a   P h d   c a n d id a te   in   E lec tro n ics   a n d   c o m m u n ica t io n   e n g g   a t  A ss a m   Do n   Bo sc o   u n iv e rsity ,   G u w a h a ti   S h e   r e c e iv e d   h e r  M   tec h   d e g re e   in   V L S I  d e s ig n   a n d   Em b e d d e d   s y ste m   f ro m   V T U  u n iv e rsity .   S h e   h a s  m o re   t h a n   1 4   y e a rs  o f  tea c h in g   e x p e rien c e   He r  re se a rc h   a r e   w o rk in g   d if fe re n t  a p p li c a ti o n   w it h   Em b e d d e d   M icr o   c o n tro l lers ,   sig n a l  p r o c e ss in g   a n d   V L S I.     M a n ju n a th   Ra m a c h a n d ra   g o t  h is  P h D  f ro m   Ba n g a lo re   u n iv e rsit y .   He   h a s  a   b len d   o f   a c a d e m ic   a n d   in d u stry   e x p e rien c e   o v e r  t w o   d e c a d e s.   He   h a s   a u th o re d   1 7 0   R e se a rc h   p a p e rs  in   i n tern a ti o n a l   c o n f e re n c e s  a n d   jo u r n a ls  a n d   a   b o o k .     His  a re a s  o f  in tere st  in c lu d e   h a rd w a re ,   sig n a l  p ro c e ss in g ,   a rti f icia l  in telli g e n c e   e tc.       Evaluation Warning : The document was created with Spire.PDF for Python.