abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
verCore.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [verCore.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Verilog parser.]
8 
9  Synopsis [Parses several flavors of structural Verilog.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - August 19, 2006.]
16 
17  Revision [$Id: verCore.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "ver.h"
22 #include "map/mio/mio.h"
23 #include "base/main/main.h"
24 
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 // types of verilog signals
33 typedef enum {
41 
42 // types of verilog gates
43 typedef enum {
53 
54 static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Des_t * pGateLib );
55 static void Ver_ParseStop( Ver_Man_t * p );
56 static void Ver_ParseFreeData( Ver_Man_t * p );
57 static void Ver_ParseInternal( Ver_Man_t * p );
58 static int Ver_ParseModule( Ver_Man_t * p );
59 static int Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType );
60 static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
61 static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
62 static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
64 static int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk );
65 static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
66 static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
67 static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
68 static int Ver_ParseAttachBoxes( Ver_Man_t * pMan );
69 
70 static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
71 static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
72 static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
73 static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
74 
75 static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan );
76 
77 static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); }
78 static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
79 
80 int glo_fMapped = 0; // this is bad!
81 
82 typedef struct Ver_Bundle_t_ Ver_Bundle_t;
84 {
85  char * pNameFormal; // the name of the formal net
86  Vec_Ptr_t * vNetsActual; // the vector of actual nets (MSB to LSB)
87 };
88 
89 ////////////////////////////////////////////////////////////////////////
90 /// FUNCTION DEFINITIONS ///
91 ////////////////////////////////////////////////////////////////////////
92 
93 /**Function*************************************************************
94 
95  Synopsis [Start parser.]
96 
97  Description []
98 
99  SideEffects []
100 
101  SeeAlso []
102 
103 ***********************************************************************/
104 Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Des_t * pGateLib )
105 {
106  Ver_Man_t * p;
107  p = ABC_ALLOC( Ver_Man_t, 1 );
108  memset( p, 0, sizeof(Ver_Man_t) );
109  p->pFileName = pFileName;
110  p->pReader = Ver_StreamAlloc( pFileName );
111  if ( p->pReader == NULL )
112  {
113  ABC_FREE( p );
114  return NULL;
115  }
116  p->Output = stdout;
117  p->vNames = Vec_PtrAlloc( 100 );
118  p->vStackFn = Vec_PtrAlloc( 100 );
119  p->vStackOp = Vec_IntAlloc( 100 );
120  p->vPerm = Vec_IntAlloc( 100 );
121  // create the design library and assign the technology library
122  p->pDesign = Abc_DesCreate( pFileName );
123  p->pDesign->pLibrary = pGateLib;
124  // derive library from SCL
125 // if ( Abc_FrameReadLibScl() )
126 // Abc_SclInstallGenlib( Abc_FrameReadLibScl(), 0, 0, 0 );
127  p->pDesign->pGenlib = Abc_FrameReadLibGen();
128  return p;
129 }
130 
131 /**Function*************************************************************
132 
133  Synopsis [Stop parser.]
134 
135  Description []
136 
137  SideEffects []
138 
139  SeeAlso []
140 
141 ***********************************************************************/
143 {
144  if ( p->pProgress )
145  Extra_ProgressBarStop( p->pProgress );
146  Ver_StreamFree( p->pReader );
147  Vec_PtrFree( p->vNames );
148  Vec_PtrFree( p->vStackFn );
149  Vec_IntFree( p->vStackOp );
150  Vec_IntFree( p->vPerm );
151  ABC_FREE( p );
152 }
153 
154 /**Function*************************************************************
155 
156  Synopsis [File parser.]
157 
158  Description []
159 
160  SideEffects []
161 
162  SeeAlso []
163 
164 ***********************************************************************/
165 Abc_Des_t * Ver_ParseFile( char * pFileName, Abc_Des_t * pGateLib, int fCheck, int fUseMemMan )
166 {
167  Ver_Man_t * p;
168  Abc_Des_t * pDesign;
169  // start the parser
170  p = Ver_ParseStart( pFileName, pGateLib );
171  p->fMapped = glo_fMapped;
172  p->fCheck = fCheck;
173  p->fUseMemMan = fUseMemMan;
174  if ( glo_fMapped )
175  {
176  Hop_ManStop((Hop_Man_t *)p->pDesign->pManFunc);
177  p->pDesign->pManFunc = NULL;
178  }
179  // parse the file
180  Ver_ParseInternal( p );
181  // save the result
182  pDesign = p->pDesign;
183  p->pDesign = NULL;
184  // stop the parser
185  Ver_ParseStop( p );
186  return pDesign;
187 }
188 
189 /**Function*************************************************************
190 
191  Synopsis [File parser.]
192 
193  Description []
194 
195  SideEffects []
196 
197  SeeAlso []
198 
199 ***********************************************************************/
201 {
202  Abc_Ntk_t * pNtk;
203  char * pToken;
204  int i;
205 
206  // preparse the modeles
207  pMan->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(pMan->pReader) );
208  while ( 1 )
209  {
210  // get the next token
211  pToken = Ver_ParseGetName( pMan );
212  if ( pToken == NULL )
213  break;
214  if ( strcmp( pToken, "module" ) )
215  {
216  sprintf( pMan->sError, "Cannot read \"module\" directive." );
218  return;
219  }
220  // parse the module
221  if ( !Ver_ParseModule(pMan) )
222  return;
223  }
224  Extra_ProgressBarStop( pMan->pProgress );
225  pMan->pProgress = NULL;
226 
227  // process defined and undefined boxes
228  if ( !Ver_ParseAttachBoxes( pMan ) )
229  return;
230 
231  // connect the boxes and check
232  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
233  {
234  // fix the dangling nets
235  Abc_NtkFinalizeRead( pNtk );
236  // check the network for correctness
237  if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
238  {
239  pMan->fTopLevel = 1;
240  sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
242  return;
243  }
244  }
245 }
246 
247 /**Function*************************************************************
248 
249  Synopsis [File parser.]
250 
251  Description []
252 
253  SideEffects []
254 
255  SeeAlso []
256 
257 ***********************************************************************/
259 {
260  if ( p->pDesign )
261  {
262  Abc_DesFree( p->pDesign, NULL );
263  p->pDesign = NULL;
264  }
265 }
266 
267 /**Function*************************************************************
268 
269  Synopsis [Prints the error message including the file name and line number.]
270 
271  Description []
272 
273  SideEffects []
274 
275  SeeAlso []
276 
277 ***********************************************************************/
279 {
280  p->fError = 1;
281  if ( p->fTopLevel ) // the line number is not given
282  fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
283  else // print the error message with the line number
284  fprintf( p->Output, "%s (line %d): %s\n",
285  p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
286  // free the data
287  Ver_ParseFreeData( p );
288 }
289 
290 /**Function*************************************************************
291 
292  Synopsis [Finds the network by name or create a new blackbox network.]
293 
294  Description []
295 
296  SideEffects []
297 
298  SeeAlso []
299 
300 ***********************************************************************/
302 {
303  Abc_Ntk_t * pNtkNew;
304  // check if the network exists
305  if ( (pNtkNew = Abc_DesFindModelByName( pMan->pDesign, pName )) )
306  return pNtkNew;
307 //printf( "Creating network %s.\n", pName );
308  // create new network
309  pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
310  pNtkNew->pName = Extra_UtilStrsav( pName );
311  pNtkNew->pSpec = NULL;
312  // add module to the design
313  Abc_DesAddModel( pMan->pDesign, pNtkNew );
314  return pNtkNew;
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis [Finds the network by name or create a new blackbox network.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName )
329 {
330  Abc_Obj_t * pObj;
331  if ( (pObj = Abc_NtkFindNet(pNtk, pName)) )
332  return pObj;
333  if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
334  return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
335  if ( !strcmp( pName, "1\'b1" ) )
336  return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
337  return NULL;
338 }
339 
340 /**Function*************************************************************
341 
342  Synopsis [Converts the network from the blackbox type into a different one.]
343 
344  Description []
345 
346  SideEffects []
347 
348  SeeAlso []
349 
350 ***********************************************************************/
351 int Ver_ParseConvertNetwork( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, int fMapped )
352 {
353  if ( fMapped )
354  {
355  // convert from the blackbox into the network with local functions representated by AIGs
356  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
357  {
358  // change network type
359  assert( pNtk->pManFunc == NULL );
360  pNtk->ntkFunc = ABC_FUNC_MAP;
361  pNtk->pManFunc = pMan->pDesign->pGenlib;
362  }
363  else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
364  {
365  sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
367  return 0;
368  }
369  }
370  else
371  {
372  // convert from the blackbox into the network with local functions representated by AIGs
373  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
374  {
375  // change network type
376  assert( pNtk->pManFunc == NULL );
377  pNtk->ntkFunc = ABC_FUNC_AIG;
378  pNtk->pManFunc = pMan->pDesign->pManFunc;
379  }
380  else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
381  {
382  sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
384  return 0;
385  }
386  }
387  return 1;
388 }
389 
390 /**Function*************************************************************
391 
392  Synopsis [Parses one Verilog module.]
393 
394  Description []
395 
396  SideEffects []
397 
398  SeeAlso []
399 
400 ***********************************************************************/
402 {
403  Mio_Gate_t * pGate;
404  Ver_Stream_t * p = pMan->pReader;
405  Abc_Ntk_t * pNtk, * pNtkTemp;
406  char * pWord, Symbol;
407  int RetValue;
408 
409  // get the network name
410  pWord = Ver_ParseGetName( pMan );
411 
412  // get the network with this name
413  pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord );
414 
415  // make sure we stopped at the opening paranthesis
416  if ( Ver_StreamPopChar(p) != '(' )
417  {
418  sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
420  return 0;
421  }
422 
423  // skip to the end of parantheses
424  do {
425  if ( Ver_ParseGetName( pMan ) == NULL )
426  return 0;
427  Symbol = Ver_StreamPopChar(p);
428  } while ( Symbol == ',' );
429  assert( Symbol == ')' );
430  if ( !Ver_ParseSkipComments( pMan ) )
431  return 0;
432  Symbol = Ver_StreamPopChar(p);
433  if ( Symbol != ';' )
434  {
435  sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
437  return 0;
438  }
439 
440  // parse the inputs/outputs/registers/wires/inouts
441  while ( 1 )
442  {
443  Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
444  pWord = Ver_ParseGetName( pMan );
445  if ( pWord == NULL )
446  return 0;
447  if ( !strcmp( pWord, "input" ) )
448  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT );
449  else if ( !strcmp( pWord, "output" ) )
450  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT );
451  else if ( !strcmp( pWord, "reg" ) )
452  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG );
453  else if ( !strcmp( pWord, "wire" ) )
454  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
455  else if ( !strcmp( pWord, "inout" ) )
456  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT );
457  else
458  break;
459  if ( RetValue == 0 )
460  return 0;
461  }
462 
463  // parse the remaining statements
464  while ( 1 )
465  {
466  Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
467 
468  if ( !strcmp( pWord, "and" ) )
469  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND );
470  else if ( !strcmp( pWord, "or" ) )
471  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR );
472  else if ( !strcmp( pWord, "xor" ) )
473  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR );
474  else if ( !strcmp( pWord, "buf" ) )
475  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF );
476  else if ( !strcmp( pWord, "nand" ) )
477  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND );
478  else if ( !strcmp( pWord, "nor" ) )
479  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR );
480  else if ( !strcmp( pWord, "xnor" ) )
481  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR );
482  else if ( !strcmp( pWord, "not" ) )
483  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
484 
485  else if ( !strcmp( pWord, "dff" ) )
486  RetValue = Ver_ParseFlopStandard( pMan, pNtk );
487 
488  else if ( !strcmp( pWord, "assign" ) )
489  RetValue = Ver_ParseAssign( pMan, pNtk );
490  else if ( !strcmp( pWord, "always" ) )
491  RetValue = Ver_ParseAlways( pMan, pNtk );
492  else if ( !strcmp( pWord, "initial" ) )
493  RetValue = Ver_ParseInitial( pMan, pNtk );
494  else if ( !strcmp( pWord, "endmodule" ) )
495  break;
496  else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName((Mio_Library_t *)pMan->pDesign->pGenlib, pWord, NULL)) ) // current design
497  RetValue = Ver_ParseGate( pMan, pNtk, pGate );
498 // else if ( pMan->pDesign->pLibrary && st__lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
499 // RetValue = Ver_ParseGate( pMan, pNtkTemp );
500  else if ( !strcmp( pWord, "wire" ) )
501  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
502  else // assume this is the box used in the current design
503  {
504  pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord );
505  RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp );
506  }
507  if ( RetValue == 0 )
508  return 0;
509  // skip the comments
510  if ( !Ver_ParseSkipComments( pMan ) )
511  return 0;
512  // get new word
513  pWord = Ver_ParseGetName( pMan );
514  if ( pWord == NULL )
515  return 0;
516  }
517 
518  // convert from the blackbox into the network with local functions representated by AIGs
519  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
520  {
521  if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 )
522  {
523  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
524  return 0;
525  }
526  else
527  {
528  Abc_Obj_t * pObj, * pBox, * pTerm;
529  int i;
530  pBox = Abc_NtkCreateBlackbox(pNtk);
531  Abc_NtkForEachPi( pNtk, pObj, i )
532  {
533  pTerm = Abc_NtkCreateBi(pNtk);
534  Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) );
535  Abc_ObjAddFanin( pBox, pTerm );
536  }
537  Abc_NtkForEachPo( pNtk, pObj, i )
538  {
539  pTerm = Abc_NtkCreateBo(pNtk);
540  Abc_ObjAddFanin( pTerm, pBox );
541  Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm );
542  }
543  }
544  }
545 
546  // remove the table if needed
548  return 1;
549 }
550 
551 
552 /**Function*************************************************************
553 
554  Synopsis [Lookups the suffix of the signal of the form [m:n].]
555 
556  Description []
557 
558  SideEffects []
559 
560  SeeAlso []
561 
562 ***********************************************************************/
563 int Ver_ParseLookupSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
564 {
565  unsigned Value;
566  *pnMsb = *pnLsb = -1;
567  if ( pMan->tName2Suffix == NULL )
568  return 1;
569  if ( ! st__lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
570  return 1;
571  *pnMsb = (Value >> 8) & 0xff;
572  *pnLsb = Value & 0xff;
573  return 1;
574 }
575 
576 /**Function*************************************************************
577 
578  Synopsis [Lookups the suffix of the signal of the form [m:n].]
579 
580  Description []
581 
582  SideEffects []
583 
584  SeeAlso []
585 
586 ***********************************************************************/
587 int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb )
588 {
589  unsigned Value;
590  if ( pMan->tName2Suffix == NULL )
591  pMan->tName2Suffix = st__init_table( strcmp, st__strhash );
592  if ( st__is_member( pMan->tName2Suffix, pWord ) )
593  return 1;
594  assert( nMsb >= 0 && nMsb < 128 );
595  assert( nLsb >= 0 && nLsb < 128 );
596  Value = (nMsb << 8) | nLsb;
597  st__insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)(ABC_PTRUINT_T)Value );
598  return 1;
599 }
600 
601 /**Function*************************************************************
602 
603  Synopsis [Lookups the suffic of the signal of the form [m:n].]
604 
605  Description []
606 
607  SideEffects []
608 
609  SeeAlso []
610 
611 ***********************************************************************/
613 {
614  st__generator * gen;
615  char * pKey, * pValue;
616  if ( pMan->tName2Suffix == NULL )
617  return;
618  st__foreach_item( pMan->tName2Suffix, gen, (const char **)&pKey, (char **)&pValue )
619  ABC_FREE( pKey );
620  st__free_table( pMan->tName2Suffix );
621  pMan->tName2Suffix = NULL;
622 }
623 
624 /**Function*************************************************************
625 
626  Synopsis [Determine signal prefix of the form [Beg:End].]
627 
628  Description []
629 
630  SideEffects []
631 
632  SeeAlso []
633 
634 ***********************************************************************/
635 int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb )
636 {
637  char * pWord = *ppWord, * pTemp;
638  int nMsb, nLsb;
639  assert( pWord[0] == '[' );
640  // get the beginning
641  nMsb = atoi( pWord + 1 );
642  // find the splitter
643  while ( *pWord && *pWord != ':' && *pWord != ']' )
644  pWord++;
645  if ( *pWord == 0 )
646  {
647  sprintf( pMan->sError, "Cannot find closing bracket in this line." );
649  return 0;
650  }
651  if ( *pWord == ']' )
652  nLsb = nMsb;
653  else
654  {
655  assert( *pWord == ':' );
656  nLsb = atoi( pWord + 1 );
657  // find the closing paranthesis
658  while ( *pWord && *pWord != ']' )
659  pWord++;
660  if ( *pWord == 0 )
661  {
662  sprintf( pMan->sError, "Cannot find closing bracket in this line." );
664  return 0;
665  }
666  assert( *pWord == ']' );
667  pWord++;
668 
669  // fix the case when <name> follows after [] without space
670  if ( *pWord == '\\' )
671  {
672  pWord++;
673  pTemp = pWord;
674  while ( *pTemp && *pTemp != ' ' )
675  pTemp++;
676  if ( *pTemp == ' ' )
677  *pTemp = 0;
678  }
679  }
680  assert( nMsb >= 0 && nLsb >= 0 );
681  // return
682  *ppWord = pWord;
683  *pnMsb = nMsb;
684  *pnLsb = nLsb;
685  return 1;
686 }
687 
688 /**Function*************************************************************
689 
690  Synopsis [Determine signal suffix of the form [m:n].]
691 
692  Description []
693 
694  SideEffects []
695 
696  SeeAlso []
697 
698 ***********************************************************************/
699 int Ver_ParseSignalSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
700 {
701  char * pCur;
702  int Length;
703  Length = strlen(pWord);
704  assert( pWord[Length-1] == ']' );
705  // walk backward
706  for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
707  if ( *pCur == ':' || *pCur == '[' )
708  break;
709  if ( pCur == pWord )
710  {
711  sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
713  return 0;
714  }
715  if ( *pCur == '[' )
716  {
717  *pnMsb = *pnLsb = atoi(pCur+1);
718  *pCur = 0;
719  return 1;
720  }
721  assert( *pCur == ':' );
722  // get the end of the interval
723  *pnLsb = atoi(pCur+1);
724  // find the beginning
725  for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
726  if ( *pCur == '[' )
727  break;
728  if ( pCur == pWord )
729  {
730  sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
732  return 0;
733  }
734  assert( *pCur == '[' );
735  // get the beginning of the interval
736  *pnMsb = atoi(pCur+1);
737  // cut the word
738  *pCur = 0;
739  return 1;
740 }
741 
742 /**Function*************************************************************
743 
744  Synopsis [Returns the values of constant bits.]
745 
746  Description [The resulting bits are in MSB to LSB order.]
747 
748  SideEffects []
749 
750  SeeAlso []
751 
752 ***********************************************************************/
753 int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord )
754 {
755  int nBits, i;
756  assert( pWord[0] >= '1' && pWord[1] <= '9' );
757  nBits = atoi(pWord);
758  // find the next symbol \'
759  while ( *pWord && *pWord != '\'' )
760  pWord++;
761  if ( *pWord == 0 )
762  {
763  sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
765  return 0;
766  }
767  assert( *pWord == '\'' );
768  pWord++;
769  if ( *pWord != 'b' )
770  {
771  sprintf( pMan->sError, "Currently can only handle binary constants." );
773  return 0;
774  }
775  pWord++;
776  // scan the bits
777  Vec_PtrClear( pMan->vNames );
778  for ( i = 0; i < nBits; i++ )
779  {
780  if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' )
781  {
782  sprintf( pMan->sError, "Having problem parsing the binary constant." );
784  return 0;
785  }
786  if ( pWord[i] == 'x' )
787  Vec_PtrPush( pMan->vNames, (void *)0 );
788  else
789  Vec_PtrPush( pMan->vNames, (void *)(ABC_PTRUINT_T)(pWord[i]-'0') );
790  }
791  return 1;
792 }
793 
794 /**Function*************************************************************
795 
796  Synopsis [Parses one directive.]
797 
798  Description [The signals are added in the order from LSB to MSB.]
799 
800  SideEffects []
801 
802  SeeAlso []
803 
804 ***********************************************************************/
805 int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType )
806 {
807  Ver_Stream_t * p = pMan->pReader;
808  char Buffer[1000], Symbol, * pWord;
809  int nMsb, nLsb, Bit, Limit, i;
810  nMsb = nLsb = -1;
811  while ( 1 )
812  {
813  // get the next word
814  pWord = Ver_ParseGetName( pMan );
815  if ( pWord == NULL )
816  return 0;
817 
818  if ( !strcmp(pWord, "wire") )
819  continue;
820 
821  // check if the range is specified
822  if ( pWord[0] == '[' && !pMan->fNameLast )
823  {
824  assert( nMsb == -1 && nLsb == -1 );
825  Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
826  // check the case when there is space between bracket and the next word
827  if ( *pWord == 0 )
828  {
829  // get the signal name
830  pWord = Ver_ParseGetName( pMan );
831  if ( pWord == NULL )
832  return 0;
833  }
834  }
835 
836  // create signals
837  if ( nMsb == -1 && nLsb == -1 )
838  {
839  if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
840  Ver_ParseCreatePi( pNtk, pWord );
841  if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
842  Ver_ParseCreatePo( pNtk, pWord );
843  if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
844  Abc_NtkFindOrCreateNet( pNtk, pWord );
845  }
846  else
847  {
848  assert( nMsb >= 0 && nLsb >= 0 );
849  // add to the hash table
850  Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
851  // add signals from Lsb to Msb
852  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
853  for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
854  {
855 // sprintf( Buffer, "%s[%d]", pWord, Bit );
856  if ( Limit > 1 )
857  sprintf( Buffer, "%s[%d]", pWord, Bit );
858  else
859  sprintf( Buffer, "%s", pWord );
860  if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
861  Ver_ParseCreatePi( pNtk, Buffer );
862  if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
863  Ver_ParseCreatePo( pNtk, Buffer );
864  if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
865  Abc_NtkFindOrCreateNet( pNtk, Buffer );
866  }
867  }
868 
869  Symbol = Ver_StreamPopChar(p);
870  if ( Symbol == ',' )
871  continue;
872  if ( Symbol == ';' )
873  return 1;
874  break;
875  }
876  sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
878  return 0;
879 }
880 
881 /**Function*************************************************************
882 
883  Synopsis [Parses one directive.]
884 
885  Description []
886 
887  SideEffects []
888 
889  SeeAlso []
890 
891 ***********************************************************************/
892 int Ver_ParseAlways( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
893 {
894  Ver_Stream_t * p = pMan->pReader;
895  Abc_Obj_t * pNet, * pNet2;
896  int fStopAfterOne;
897  char * pWord, * pWord2;
898  char Symbol;
899  // parse the directive
900  pWord = Ver_ParseGetName( pMan );
901  if ( pWord == NULL )
902  return 0;
903  if ( pWord[0] == '@' )
904  {
905  Ver_StreamSkipToChars( p, ")" );
907  // parse the directive
908  pWord = Ver_ParseGetName( pMan );
909  if ( pWord == NULL )
910  return 0;
911  }
912  // decide how many statements to parse
913  fStopAfterOne = 0;
914  if ( strcmp( pWord, "begin" ) )
915  fStopAfterOne = 1;
916  // iterate over the initial states
917  while ( 1 )
918  {
919  if ( !fStopAfterOne )
920  {
921  // get the name of the output signal
922  pWord = Ver_ParseGetName( pMan );
923  if ( pWord == NULL )
924  return 0;
925  // look for the end of directive
926  if ( !strcmp( pWord, "end" ) )
927  break;
928  }
929  // get the fanout net
930  pNet = Ver_ParseFindNet( pNtk, pWord );
931  if ( pNet == NULL )
932  {
933  sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
935  return 0;
936  }
937  // get the equality sign
938  Symbol = Ver_StreamPopChar(p);
939  if ( Symbol != '<' && Symbol != '=' )
940  {
941  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
943  return 0;
944  }
945  if ( Symbol == '<' )
947  // skip the comments
948  if ( !Ver_ParseSkipComments( pMan ) )
949  return 0;
950  // get the second name
951  pWord2 = Ver_ParseGetName( pMan );
952  if ( pWord2 == NULL )
953  return 0;
954  // check if the name is complemented
955  if ( pWord2[0] == '~' )
956  {
957  pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 );
958  pNet2 = Ver_ParseCreateInv( pNtk, pNet2 );
959  }
960  else
961  pNet2 = Ver_ParseFindNet( pNtk, pWord2 );
962  if ( pNet2 == NULL )
963  {
964  sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
966  return 0;
967  }
968  // create the latch
969  Ver_ParseCreateLatch( pNtk, pNet2, pNet );
970  // remove the last symbol
971  Symbol = Ver_StreamPopChar(p);
972  assert( Symbol == ';' );
973  // quit if only one directive
974  if ( fStopAfterOne )
975  break;
976  }
977  return 1;
978 }
979 
980 /**Function*************************************************************
981 
982  Synopsis [Parses one directive.]
983 
984  Description []
985 
986  SideEffects []
987 
988  SeeAlso []
989 
990 ***********************************************************************/
991 int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
992 {
993  Ver_Stream_t * p = pMan->pReader;
994  Abc_Obj_t * pNode, * pNet;
995  int fStopAfterOne;
996  char * pWord, * pEquation;
997  char Symbol;
998  // parse the directive
999  pWord = Ver_ParseGetName( pMan );
1000  if ( pWord == NULL )
1001  return 0;
1002  // decide how many statements to parse
1003  fStopAfterOne = 0;
1004  if ( strcmp( pWord, "begin" ) )
1005  fStopAfterOne = 1;
1006  // iterate over the initial states
1007  while ( 1 )
1008  {
1009  if ( !fStopAfterOne )
1010  {
1011  // get the name of the output signal
1012  pWord = Ver_ParseGetName( pMan );
1013  if ( pWord == NULL )
1014  return 0;
1015  // look for the end of directive
1016  if ( !strcmp( pWord, "end" ) )
1017  break;
1018  }
1019  // get the fanout net
1020  pNet = Ver_ParseFindNet( pNtk, pWord );
1021  if ( pNet == NULL )
1022  {
1023  sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
1025  return 0;
1026  }
1027  // get the equality sign
1028  Symbol = Ver_StreamPopChar(p);
1029  if ( Symbol != '<' && Symbol != '=' )
1030  {
1031  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
1033  return 0;
1034  }
1035  if ( Symbol == '<' )
1036  Ver_StreamPopChar(p);
1037  // skip the comments
1038  if ( !Ver_ParseSkipComments( pMan ) )
1039  return 0;
1040  // get the second name
1041  pEquation = Ver_StreamGetWord( p, ";" );
1042  if ( pEquation == NULL )
1043  return 0;
1044  // find the corresponding latch
1045  if ( Abc_ObjFaninNum(pNet) == 0 )
1046  {
1047  sprintf( pMan->sError, "Cannot find the latch to assign the initial value." );
1049  return 0;
1050  }
1051  pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet));
1052  assert( Abc_ObjIsLatch(pNode) );
1053  // set the initial state
1054  if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") )
1055  Abc_LatchSetInit0( pNode );
1056  else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
1057  Abc_LatchSetInit1( pNode );
1058 // else if ( !strcmp(pEquation, "2") )
1059 // Abc_LatchSetInitDc( pNode );
1060  else
1061  {
1062  sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) );
1064  return 0;
1065  }
1066  // remove the last symbol
1067  Symbol = Ver_StreamPopChar(p);
1068  assert( Symbol == ';' );
1069  // quit if only one directive
1070  if ( fStopAfterOne )
1071  break;
1072  }
1073  return 1;
1074 }
1075 
1076 /**Function*************************************************************
1077 
1078  Synopsis [Parses one directive.]
1079 
1080  Description []
1081 
1082  SideEffects []
1083 
1084  SeeAlso []
1085 
1086 ***********************************************************************/
1087 int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
1088 {
1089  char Buffer[1000], Buffer2[1000];
1090  Ver_Stream_t * p = pMan->pReader;
1091  Abc_Obj_t * pNode, * pNet;
1092  char * pWord, * pName, * pEquation;
1093  Hop_Obj_t * pFunc;
1094  char Symbol;
1095  int i, Bit, Limit, Length, fReduction;
1096  int nMsb, nLsb;
1097 
1098 // if ( Ver_StreamGetLineNumber(p) == 2756 )
1099 // {
1100 // int x = 0;
1101 // }
1102 
1103  // convert from the blackbox into the network with local functions representated by AIGs
1104  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1105  return 0;
1106 
1107  while ( 1 )
1108  {
1109  // get the name of the output signal
1110  pWord = Ver_ParseGetName( pMan );
1111  if ( pWord == NULL )
1112  return 0;
1113  if ( strcmp(pWord, "#1") == 0 )
1114  continue;
1115  // check for vector-inputs
1116  if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
1117  return 0;
1118  // handle special case of constant assignment
1119  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
1120  if ( nMsb >= 0 && nLsb >= 0 && Limit > 1 )
1121  {
1122  // save the fanout name
1123  if ( !strcmp(pWord, "1\'h0") )
1124  strcpy( Buffer, "1\'b0" );
1125  else if ( !strcmp(pWord, "1\'h1") )
1126  strcpy( Buffer, "1\'b1" );
1127  else
1128  strcpy( Buffer, pWord );
1129  // get the equality sign
1130  if ( Ver_StreamPopChar(p) != '=' )
1131  {
1132  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
1134  return 0;
1135  }
1136  // get the constant
1137  pWord = Ver_ParseGetName( pMan );
1138  if ( pWord == NULL )
1139  return 0;
1140  // check if it is indeed a constant
1141  if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
1142  {
1143  sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
1145  return 0;
1146  }
1147 
1148  // get individual bits of the constant
1149  if ( !Ver_ParseConstant( pMan, pWord ) )
1150  return 0;
1151  // check that the constant has the same size
1152  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
1153  if ( Limit != Vec_PtrSize(pMan->vNames) )
1154  {
1155  sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).",
1156  Vec_PtrSize(pMan->vNames), Buffer, Limit );
1158  return 0;
1159  }
1160  // iterate through the bits
1161  for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
1162  {
1163  // get the fanin net
1164  if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
1165  pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
1166  else
1167  pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
1168  assert( pNet != NULL );
1169 
1170  // create the buffer
1171  pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
1172 
1173  // get the fanout net
1174  sprintf( Buffer2, "%s[%d]", Buffer, Bit );
1175  pNet = Ver_ParseFindNet( pNtk, Buffer2 );
1176  if ( pNet == NULL )
1177  {
1178  sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
1180  return 0;
1181  }
1182  Abc_ObjAddFanin( pNet, pNode );
1183  }
1184  // go to the end of the line
1185  Ver_ParseSkipComments( pMan );
1186  }
1187  else
1188  {
1189  // consider the case of reduction operations
1190  fReduction = 0;
1191  if ( pWord[0] == '{' && !pMan->fNameLast )
1192  fReduction = 1;
1193  if ( fReduction )
1194  {
1195  pWord++;
1196  pWord[strlen(pWord)-1] = 0;
1197  assert( pWord[0] != '\\' );
1198  }
1199  // get the fanout net
1200  pNet = Ver_ParseFindNet( pNtk, pWord );
1201  if ( pNet == NULL )
1202  {
1203  sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
1205  return 0;
1206  }
1207  // get the equality sign
1208  if ( Ver_StreamPopChar(p) != '=' )
1209  {
1210  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
1212  return 0;
1213  }
1214  // skip the comments
1215  if ( !Ver_ParseSkipComments( pMan ) )
1216  return 0;
1217  // get the second name
1218  if ( fReduction )
1219  pEquation = Ver_StreamGetWord( p, ";" );
1220  else
1221  pEquation = Ver_StreamGetWord( p, ",;" );
1222  if ( pEquation == NULL )
1223  {
1224  sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
1226  return 0;
1227  }
1228 
1229  // consider the case of mapped network
1230  Vec_PtrClear( pMan->vNames );
1231  if ( pMan->fMapped )
1232  {
1233  if ( !strcmp( pEquation, "1\'b0" ) )
1235  else if ( !strcmp( pEquation, "1\'b1" ) )
1237  else
1238  {
1239  // "assign foo = \bar ;"
1240  if ( *pEquation == '\\' )
1241  {
1242  pEquation++;
1243  pEquation[strlen(pEquation) - 1] = 0;
1244  }
1245  if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
1246  {
1247  sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
1249  return 0;
1250  }
1251  Vec_PtrPush( pMan->vNames, (void *)(ABC_PTRUINT_T)strlen(pEquation) );
1252  Vec_PtrPush( pMan->vNames, pEquation );
1253  // get the buffer
1255  if ( pFunc == NULL )
1256  {
1257  sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
1259  return 0;
1260  }
1261  }
1262  }
1263  else
1264  {
1265  if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") )
1266  pFunc = Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
1267  else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
1268  pFunc = Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc);
1269  else if ( fReduction )
1270  pFunc = (Hop_Obj_t *)Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );
1271  else
1272  pFunc = (Hop_Obj_t *)Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
1273  if ( pFunc == NULL )
1274  {
1276  return 0;
1277  }
1278  }
1279 
1280  // create the node with the given inputs
1281  pNode = Abc_NtkCreateNode( pNtk );
1282  pNode->pData = pFunc;
1283  Abc_ObjAddFanin( pNet, pNode );
1284  // connect to fanin nets
1285  for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
1286  {
1287  // get the name of this signal
1288  Length = (int)(ABC_PTRUINT_T)Vec_PtrEntry( pMan->vNames, 2*i );
1289  pName = (char *)Vec_PtrEntry( pMan->vNames, 2*i + 1 );
1290  pName[Length] = 0;
1291  // try name
1292 // pNet = Ver_ParseFindNet( pNtk, pName );
1293  if ( !strcmp(pName, "1\'h0") )
1294  pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
1295  else if ( !strcmp(pName, "1\'h1") )
1296  pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
1297  else
1298  pNet = Ver_ParseFindNet( pNtk, pName );
1299  // find the corresponding net
1300  if ( pNet == NULL )
1301  {
1302  sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
1304  return 0;
1305  }
1306  Abc_ObjAddFanin( pNode, pNet );
1307  }
1308  }
1309 
1310  Symbol = Ver_StreamPopChar(p);
1311  if ( Symbol == ',' )
1312  continue;
1313  if ( Symbol == ';' )
1314  return 1;
1315  }
1316  return 1;
1317 }
1318 
1319 /**Function*************************************************************
1320 
1321  Synopsis [Parses one directive.]
1322 
1323  Description []
1324 
1325  SideEffects []
1326 
1327  SeeAlso []
1328 
1329 ***********************************************************************/
1331 {
1332  Ver_Stream_t * p = pMan->pReader;
1333  Abc_Obj_t * pNet, * pNode;
1334  char * pWord, Symbol;
1335 
1336  // convert from the blackbox into the network with local functions representated by AIGs
1337  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1338  return 0;
1339 
1340  // this is gate name - throw it away
1341  if ( Ver_StreamPopChar(p) != '(' )
1342  {
1343  sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
1345  return 0;
1346  }
1347  Ver_ParseSkipComments( pMan );
1348 
1349  // create the node
1350  pNode = Abc_NtkCreateNode( pNtk );
1351 
1352  // parse pairs of formal/actural inputs
1353  while ( 1 )
1354  {
1355  // parse the output name
1356  pWord = Ver_ParseGetName( pMan );
1357  if ( pWord == NULL )
1358  return 0;
1359  // get the net corresponding to this output
1360  pNet = Ver_ParseFindNet( pNtk, pWord );
1361  if ( pNet == NULL )
1362  {
1363  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1365  return 0;
1366  }
1367  // if this is the first net, add it as an output
1368  if ( Abc_ObjFanoutNum(pNode) == 0 )
1369  Abc_ObjAddFanin( pNet, pNode );
1370  else
1371  Abc_ObjAddFanin( pNode, pNet );
1372  // check if it is the end of gate
1373  Ver_ParseSkipComments( pMan );
1374  Symbol = Ver_StreamPopChar(p);
1375  if ( Symbol == ')' )
1376  break;
1377  // skip comma
1378  if ( Symbol != ',' )
1379  {
1380  sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1382  return 0;
1383  }
1384  Ver_ParseSkipComments( pMan );
1385  }
1386  if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
1387  {
1388  sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1390  return 0;
1391  }
1392 
1393  // check if it is the end of gate
1394  Ver_ParseSkipComments( pMan );
1395  if ( Ver_StreamPopChar(p) != ';' )
1396  {
1397  sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1399  return 0;
1400  }
1401  // add logic function
1402  if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
1403  pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1404  else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
1405  pNode->pData = Hop_CreateOr( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1406  else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
1407  pNode->pData = Hop_CreateExor( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1408  else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
1409  pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1410  if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
1411  pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
1412  return 1;
1413 }
1414 
1415 /**Function*************************************************************
1416 
1417  Synopsis [Parses one directive.]
1418 
1419  Description []
1420 
1421  SideEffects []
1422 
1423  SeeAlso []
1424 
1425 ***********************************************************************/
1427 {
1428  Ver_Stream_t * p = pMan->pReader;
1429  Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
1430  char * pWord, Symbol;
1431 
1432  // convert from the blackbox into the network with local functions representated by AIGs
1433  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1434  return 0;
1435 
1436  // this is gate name - throw it away
1437  if ( Ver_StreamPopChar(p) != '(' )
1438  {
1439  sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
1441  return 0;
1442  }
1443  Ver_ParseSkipComments( pMan );
1444 
1445  // parse the output name
1446  pWord = Ver_ParseGetName( pMan );
1447  if ( pWord == NULL )
1448  return 0;
1449  // get the net corresponding to this output
1450  pNetLo = Ver_ParseFindNet( pNtk, pWord );
1451  if ( pNetLo == NULL )
1452  {
1453  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1455  return 0;
1456  }
1457 
1458  // check if it is the end of gate
1459  Ver_ParseSkipComments( pMan );
1460  Symbol = Ver_StreamPopChar(p);
1461  if ( Symbol == ')' )
1462  {
1463  sprintf( pMan->sError, "Cannot parse the flop." );
1465  return 0;
1466  }
1467  // skip comma
1468  if ( Symbol != ',' )
1469  {
1470  sprintf( pMan->sError, "Cannot parse the flop." );
1472  return 0;
1473  }
1474  Ver_ParseSkipComments( pMan );
1475 
1476  // parse the output name
1477  pWord = Ver_ParseGetName( pMan );
1478  if ( pWord == NULL )
1479  return 0;
1480  // get the net corresponding to this output
1481  pNetLi = Ver_ParseFindNet( pNtk, pWord );
1482  if ( pNetLi == NULL )
1483  {
1484  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1486  return 0;
1487  }
1488 
1489  // check if it is the end of gate
1490  Ver_ParseSkipComments( pMan );
1491  Symbol = Ver_StreamPopChar(p);
1492  if ( Symbol != ')' )
1493  {
1494  sprintf( pMan->sError, "Cannot parse the flop." );
1496  return 0;
1497  }
1498 
1499  // check if it is the end of gate
1500  Ver_ParseSkipComments( pMan );
1501  if ( Ver_StreamPopChar(p) != ';' )
1502  {
1503  sprintf( pMan->sError, "Cannot parse the flop." );
1505  return 0;
1506  }
1507 
1508  // create the latch
1509  pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
1510  Abc_LatchSetInit0( pLatch );
1511  return 1;
1512 }
1513 
1514 /**Function*************************************************************
1515 
1516  Synopsis [Returns the index of the given pin the gate.]
1517 
1518  Description []
1519 
1520  SideEffects []
1521 
1522  SeeAlso []
1523 
1524 ***********************************************************************/
1525 int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
1526 {
1527  Mio_Pin_t * pGatePin;
1528  int i;
1529  for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
1530  if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
1531  return i;
1532  if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
1533  return i;
1534  if ( Mio_GateReadTwin(pGate) && strcmp(pName, Mio_GateReadOutName(Mio_GateReadTwin(pGate))) == 0 )
1535  return i+1;
1536  return -1;
1537 }
1538 
1539 /**Function*************************************************************
1540 
1541  Synopsis [Parses one directive.]
1542 
1543  Description []
1544 
1545  SideEffects []
1546 
1547  SeeAlso []
1548 
1549 ***********************************************************************/
1550 int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
1551 {
1552  Ver_Stream_t * p = pMan->pReader;
1553  Abc_Obj_t * pNetActual, * pNode, * pNode2 = NULL;
1554  char * pWord, Symbol;
1555  int Input, i, nFanins = Mio_GateReadPinNum(pGate);
1556 
1557  // convert from the blackbox into the network with local functions representated by gates
1558  if ( 1 != pMan->fMapped )
1559  {
1560  sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
1562  return 0;
1563  }
1564 
1565  // update the network type if needed
1566  if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
1567  return 0;
1568 
1569  // parse the directive and set the pointers to the PIs/POs of the gate
1570  pWord = Ver_ParseGetName( pMan );
1571  if ( pWord == NULL )
1572  return 0;
1573  // this is gate name - throw it away
1574  if ( Ver_StreamPopChar(p) != '(' )
1575  {
1576  sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) );
1578  return 0;
1579  }
1580  Ver_ParseSkipComments( pMan );
1581 
1582  // start the node
1583  pNode = Abc_NtkCreateNode( pNtk );
1584  pNode->pData = pGate;
1585  if ( Mio_GateReadTwin(pGate) )
1586  {
1587  pNode2 = Abc_NtkCreateNode( pNtk );
1588  pNode2->pData = Mio_GateReadTwin(pGate);
1589  }
1590  // parse pairs of formal/actural inputs
1591  Vec_IntClear( pMan->vPerm );
1592  while ( 1 )
1593  {
1594  // process one pair of formal/actual parameters
1595  if ( Ver_StreamPopChar(p) != '.' )
1596  {
1597  sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
1599  return 0;
1600  }
1601 
1602  // parse the formal name
1603  pWord = Ver_ParseGetName( pMan );
1604  if ( pWord == NULL )
1605  return 0;
1606 
1607  // find the corresponding pin of the gate
1608  Input = Ver_FindGateInput( pGate, pWord );
1609  if ( Input == -1 )
1610  {
1611  sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
1613  return 0;
1614  }
1615 
1616  // open the paranthesis
1617  if ( Ver_StreamPopChar(p) != '(' )
1618  {
1619  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) );
1621  return 0;
1622  }
1623 
1624  // parse the actual name
1625  pWord = Ver_ParseGetName( pMan );
1626  if ( pWord == NULL )
1627  return 0;
1628  // check if the name is complemented
1629  assert( pWord[0] != '~' );
1630 /*
1631  fCompl = (pWord[0] == '~');
1632  if ( fCompl )
1633  {
1634  fComplUsed = 1;
1635  pWord++;
1636  if ( pNtk->pData == NULL )
1637  pNtk->pData = Extra_MmFlexStart();
1638  }
1639 */
1640  // get the actual net
1641  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1642  if ( pNetActual == NULL )
1643  {
1644  sprintf( pMan->sError, "Actual net %s is missing.", pWord );
1646  return 0;
1647  }
1648 
1649  // close the paranthesis
1650  if ( Ver_StreamPopChar(p) != ')' )
1651  {
1652  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
1654  return 0;
1655  }
1656 
1657  // add the fanin
1658  if ( Input < nFanins )
1659  {
1660  Vec_IntPush( pMan->vPerm, Input );
1661  Abc_ObjAddFanin( pNode, pNetActual ); // fanin
1662  if ( pNode2 )
1663  Abc_ObjAddFanin( pNode2, pNetActual ); // fanin
1664  }
1665  else if ( Input == nFanins )
1666  Abc_ObjAddFanin( pNetActual, pNode ); // fanout
1667  else if ( Input == nFanins + 1 )
1668  Abc_ObjAddFanin( pNetActual, pNode2 ); // fanout
1669  else
1670  assert( 0 );
1671 
1672  // check if it is the end of gate
1673  Ver_ParseSkipComments( pMan );
1674  Symbol = Ver_StreamPopChar(p);
1675  if ( Symbol == ')' )
1676  break;
1677 
1678  // skip comma
1679  if ( Symbol != ',' )
1680  {
1681  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
1683  return 0;
1684  }
1685  Ver_ParseSkipComments( pMan );
1686  }
1687 
1688  // check that the gate as the same number of input
1689  if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
1690  {
1691  sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
1693  return 0;
1694  }
1695 
1696  // check if it is the end of gate
1697  Ver_ParseSkipComments( pMan );
1698  if ( Ver_StreamPopChar(p) != ';' )
1699  {
1700  sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
1702  return 0;
1703  }
1704 
1705  // check if we need to permute the inputs
1706  Vec_IntForEachEntry( pMan->vPerm, Input, i )
1707  if ( Input != i )
1708  break;
1709  if ( i < Vec_IntSize(pMan->vPerm) )
1710  {
1711  // add the fanin numnbers to the end of the permuation array
1712  for ( i = 0; i < nFanins; i++ )
1713  Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
1714  // write the fanin numbers into their corresponding places (according to the gate)
1715  for ( i = 0; i < nFanins; i++ )
1716  Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
1717  }
1718  return 1;
1719 }
1720 
1721 /**Function*************************************************************
1722 
1723  Synopsis [Parses one directive.]
1724 
1725  Description []
1726 
1727  SideEffects []
1728 
1729  SeeAlso []
1730 
1731 ***********************************************************************/
1732 int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
1733 {
1734  char Buffer[1000];
1735  Ver_Stream_t * p = pMan->pReader;
1736  Ver_Bundle_t * pBundle;
1737  Vec_Ptr_t * vBundles;
1738  Abc_Obj_t * pNetActual;
1739  Abc_Obj_t * pNode;
1740  char * pWord, Symbol;
1741  int fCompl, fFormalIsGiven;
1742  int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
1743 
1744  // gate the name of the box
1745  pWord = Ver_ParseGetName( pMan );
1746  if ( pWord == NULL )
1747  return 0;
1748 
1749  // create a box with this name
1750  pNode = Abc_NtkCreateBlackbox( pNtk );
1751  pNode->pData = pNtkBox;
1752  Abc_ObjAssignName( pNode, pWord, NULL );
1753 
1754  // continue parsing the box
1755  if ( Ver_StreamPopChar(p) != '(' )
1756  {
1757  sprintf( pMan->sError, "Cannot parse box %s (expected opening paranthesis).", Abc_ObjName(pNode) );
1759  return 0;
1760  }
1761  Ver_ParseSkipComments( pMan );
1762 
1763  // parse pairs of formal/actual inputs
1764  vBundles = Vec_PtrAlloc( 16 );
1765  pNode->pCopy = (Abc_Obj_t *)vBundles;
1766  while ( 1 )
1767  {
1768  // allocate the bundle (formal name + array of actual nets)
1769  pBundle = ABC_ALLOC( Ver_Bundle_t, 1 );
1770  pBundle->pNameFormal = NULL;
1771  pBundle->vNetsActual = Vec_PtrAlloc( 4 );
1772  Vec_PtrPush( vBundles, pBundle );
1773 
1774  // process one pair of formal/actual parameters
1775  fFormalIsGiven = 0;
1776  if ( Ver_StreamScanChar(p) == '.' )
1777  {
1778  fFormalIsGiven = 1;
1779  if ( Ver_StreamPopChar(p) != '.' )
1780  {
1781  sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) );
1783  return 0;
1784  }
1785 
1786  // parse the formal name
1787  pWord = Ver_ParseGetName( pMan );
1788  if ( pWord == NULL )
1789  return 0;
1790 
1791  // save the name
1792  pBundle->pNameFormal = Extra_UtilStrsav( pWord );
1793 
1794  // open the paranthesis
1795  if ( Ver_StreamPopChar(p) != '(' )
1796  {
1797  sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
1799  return 0;
1800  }
1801  Ver_ParseSkipComments( pMan );
1802  }
1803 
1804  // check if this is the beginning of {} expression
1805  Symbol = Ver_StreamScanChar(p);
1806 
1807  // consider the case of vector-inputs
1808  if ( Symbol == '{' )
1809  {
1810  // skip this char
1811  Ver_StreamPopChar(p);
1812 
1813  // read actual names
1814  i = 0;
1815  fQuit = 0;
1816  while ( 1 )
1817  {
1818  // parse the formal name
1819  Ver_ParseSkipComments( pMan );
1820  pWord = Ver_ParseGetName( pMan );
1821  if ( pWord == NULL )
1822  return 0;
1823 
1824  // check if the last char is a closing brace
1825  if ( pWord[strlen(pWord)-1] == '}' )
1826  {
1827  pWord[strlen(pWord)-1] = 0;
1828  fQuit = 1;
1829  }
1830  if ( pWord[0] == 0 )
1831  break;
1832 
1833  // check for constant
1834  if ( pWord[0] >= '1' && pWord[0] <= '9' )
1835  {
1836  if ( !Ver_ParseConstant( pMan, pWord ) )
1837  return 0;
1838  // add constant MSB to LSB
1839  for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
1840  {
1841  // get the actual net
1842  sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
1843  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1844  if ( pNetActual == NULL )
1845  {
1846  sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
1848  return 0;
1849  }
1850  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1851  }
1852  }
1853  else
1854  {
1855  // get the suffix of the form [m:n]
1856  if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
1857  Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1858  else
1859  Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1860 
1861  // generate signals
1862  if ( nMsb == -1 && nLsb == -1 )
1863  {
1864  // get the actual net
1865  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1866  if ( pNetActual == NULL )
1867  {
1868  if ( !strncmp(pWord, "Open_", 5) ||
1869  !strncmp(pWord, "dct_unconnected", 15) )
1870  pNetActual = Abc_NtkCreateNet( pNtk );
1871  else
1872  {
1873  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1875  return 0;
1876  }
1877  }
1878  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1879  i++;
1880  }
1881  else
1882  {
1883  // go from MSB to LSB
1884  assert( nMsb >= 0 && nLsb >= 0 );
1885  Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1886  for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
1887  {
1888  // get the actual net
1889  sprintf( Buffer, "%s[%d]", pWord, Bit );
1890  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1891  if ( pNetActual == NULL )
1892  {
1893  if ( !strncmp(pWord, "Open_", 5) ||
1894  !strncmp(pWord, "dct_unconnected", 15) )
1895  pNetActual = Abc_NtkCreateNet( pNtk );
1896  else
1897  {
1898  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1900  return 0;
1901  }
1902  }
1903  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1904  }
1905  }
1906  }
1907 
1908  if ( fQuit )
1909  break;
1910 
1911  // skip comma
1912  Ver_ParseSkipComments( pMan );
1913  Symbol = Ver_StreamPopChar(p);
1914  if ( Symbol == '}' )
1915  break;
1916  if ( Symbol != ',' )
1917  {
1918  sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
1920  return 0;
1921  }
1922  }
1923  }
1924  else
1925  {
1926  // get the next word
1927  pWord = Ver_ParseGetName( pMan );
1928  if ( pWord == NULL )
1929  return 0;
1930  // consider the case of empty name
1931  fCompl = 0;
1932  if ( pWord[0] == 0 )
1933  {
1934  pNetActual = Abc_NtkCreateNet( pNtk );
1935  Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
1936  }
1937  else
1938  {
1939  // get the actual net
1940  flag=0;
1941  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1942  if ( pNetActual == NULL )
1943  {
1944  Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1945  if ( nMsb == -1 && nLsb == -1 )
1946  {
1947  Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1948  if ( nMsb == -1 && nLsb == -1 )
1949  {
1950  if ( !strncmp(pWord, "Open_", 5) ||
1951  !strncmp(pWord, "dct_unconnected", 15) )
1952  {
1953  pNetActual = Abc_NtkCreateNet( pNtk );
1954  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1955  }
1956  else
1957  {
1958  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1960  return 0;
1961  }
1962  }
1963  else
1964  {
1965  flag=1;
1966  }
1967  }
1968  else
1969  {
1970  flag=1;
1971  }
1972  if (flag)
1973  {
1974  Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1975  for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
1976  {
1977  // get the actual net
1978  sprintf( Buffer, "%s[%d]", pWord, Bit );
1979  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1980  if ( pNetActual == NULL )
1981  {
1982  if ( !strncmp(pWord, "Open_", 5) ||
1983  !strncmp(pWord, "dct_unconnected", 15))
1984  pNetActual = Abc_NtkCreateNet( pNtk );
1985  else
1986  {
1987  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1989  return 0;
1990  }
1991  }
1992  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1993  }
1994  }
1995  }
1996  else
1997  {
1998  Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
1999  }
2000  }
2001  }
2002 
2003  if ( fFormalIsGiven )
2004  {
2005  // close the paranthesis
2006  Ver_ParseSkipComments( pMan );
2007  if ( Ver_StreamPopChar(p) != ')' )
2008  {
2009  sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
2011  return 0;
2012  }
2013  Ver_ParseSkipComments( pMan );
2014  }
2015 
2016  // check if it is the end of gate
2017  Symbol = Ver_StreamPopChar(p);
2018  if ( Symbol == ')' )
2019  break;
2020  // skip comma
2021  if ( Symbol != ',' )
2022  {
2023  sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) );
2025  return 0;
2026  }
2027  Ver_ParseSkipComments( pMan );
2028  }
2029 
2030  // check if it is the end of gate
2031  Ver_ParseSkipComments( pMan );
2032  if ( Ver_StreamPopChar(p) != ';' )
2033  {
2034  sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) );
2036  return 0;
2037  }
2038 
2039  return 1;
2040 }
2041 
2042 /**Function*************************************************************
2043 
2044  Synopsis [Connects one box to the network]
2045 
2046  Description []
2047 
2048  SideEffects []
2049 
2050  SeeAlso []
2051 
2052 ***********************************************************************/
2054 {
2055  ABC_FREE( pBundle->pNameFormal );
2056  Vec_PtrFree( pBundle->vNetsActual );
2057  ABC_FREE( pBundle );
2058 }
2059 
2060 /**Function*************************************************************
2061 
2062  Synopsis [Connects one box to the network]
2063 
2064  Description []
2065 
2066  SideEffects []
2067 
2068  SeeAlso []
2069 
2070 ***********************************************************************/
2072 {
2073  Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
2074  Abc_Ntk_t * pNtk = pBox->pNtk;
2075  Abc_Ntk_t * pNtkBox = (Abc_Ntk_t *)pBox->pData;
2076  Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
2077  Ver_Bundle_t * pBundle;
2078  char * pNameFormal;
2079  int i, k, j, iBundle, Length;
2080 
2081  assert( !Ver_ObjIsConnected(pBox) );
2082  assert( Ver_NtkIsDefined(pNtkBox) );
2083  assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
2084 
2085 /*
2086  // clean the PI/PO nets
2087  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2088  Abc_ObjFanout0(pTerm)->pCopy = NULL;
2089  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2090  Abc_ObjFanin0(pTerm)->pCopy = NULL;
2091 */
2092 
2093  // check the number of actual nets is the same as the number of formal nets
2094  if ( Vec_PtrSize(vBundles) > Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2095  {
2096  sprintf( pMan->sError, "The number of actual IOs (%d) is bigger than the number of formal IOs (%d) when instantiating network %s in box %s.",
2097  Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2098  // free the bundling
2099  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2100  Ver_ParseFreeBundle( pBundle );
2101  Vec_PtrFree( vBundles );
2102  pBox->pCopy = NULL;
2104  return 0;
2105  }
2106 
2107  // check if some of them do not have formal names
2108  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2109  if ( pBundle->pNameFormal == NULL )
2110  break;
2111  if ( k < Vec_PtrSize(vBundles) )
2112  {
2113  printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
2114  // add all actual nets in the bundles
2115  iBundle = 0;
2116  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2117  iBundle += Vec_PtrSize(pBundle->vNetsActual);
2118 
2119  // check the number of actual nets is the same as the number of formal nets
2120  if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2121  {
2122  sprintf( pMan->sError, "The number of actual IOs (%d) is different from the number of formal IOs (%d) when instantiating network %s in box %s.",
2123  Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2124  // free the bundling
2125  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2126  Ver_ParseFreeBundle( pBundle );
2127  Vec_PtrFree( vBundles );
2128  pBox->pCopy = NULL;
2130  return 0;
2131  }
2132  // connect bundles in the natural order
2133  iBundle = 0;
2134  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2135  {
2136  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2137  // the bundle is found - add the connections - using order LSB to MSB
2138  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2139  {
2140  pTermNew = Abc_NtkCreateBi( pNtk );
2141  Abc_ObjAddFanin( pBox, pTermNew );
2142  Abc_ObjAddFanin( pTermNew, pNetAct );
2143  i++;
2144  }
2145  i--;
2146  }
2147  // create fanins of the box
2148  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2149  {
2150  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2151  // the bundle is found - add the connections - using order LSB to MSB
2152  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2153  {
2154  pTermNew = Abc_NtkCreateBo( pNtk );
2155  Abc_ObjAddFanin( pTermNew, pBox );
2156  Abc_ObjAddFanin( pNetAct, pTermNew );
2157  i++;
2158  }
2159  i--;
2160  }
2161 
2162  // free the bundling
2163  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2164  Ver_ParseFreeBundle( pBundle );
2165  Vec_PtrFree( vBundles );
2166  pBox->pCopy = NULL;
2167  return 1;
2168  }
2169 
2170  // bundles arrive in any order - but inside each bundle the order is MSB to LSB
2171  // make sure every formal PI has a corresponding net
2172  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2173  {
2174  // get the name of this formal net
2175  pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
2176  // try to find the bundle with this formal net
2177  pBundle = NULL;
2178  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2179  if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2180  break;
2181  assert( pBundle != NULL );
2182  // if the bundle is not found, try without parantheses
2183  if ( k == Vec_PtrSize(vBundles) )
2184  {
2185  pBundle = NULL;
2186  Length = strlen(pNameFormal);
2187  if ( pNameFormal[Length-1] == ']' )
2188  {
2189  // find the opening brace
2190  for ( Length--; Length >= 0; Length-- )
2191  if ( pNameFormal[Length] == '[' )
2192  break;
2193  // compare names before brace
2194  if ( Length > 0 )
2195  {
2196  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2197  if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2198  break;
2199  if ( j == Vec_PtrSize(vBundles) )
2200  pBundle = NULL;
2201  }
2202  }
2203  if ( pBundle == NULL )
2204  {
2205  sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.",
2206  pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2208  return 0;
2209  }
2210  }
2211  // the bundle is found - add the connections - using order LSB to MSB
2212  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2213  {
2214  pTermNew = Abc_NtkCreateBi( pNtk );
2215  Abc_ObjAddFanin( pBox, pTermNew );
2216  Abc_ObjAddFanin( pTermNew, pNetAct );
2217  i++;
2218  }
2219  i--;
2220  }
2221 
2222  // connect those formal POs that do have nets
2223  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2224  {
2225  // get the name of this PI
2226  pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
2227  // try to find this formal net in the bundle
2228  pBundle = NULL;
2229  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2230  if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2231  break;
2232  assert( pBundle != NULL );
2233  // if the name is not found, try without parantheses
2234  if ( k == Vec_PtrSize(vBundles) )
2235  {
2236  pBundle = NULL;
2237  Length = strlen(pNameFormal);
2238  if ( pNameFormal[Length-1] == ']' )
2239  {
2240  // find the opening brace
2241  for ( Length--; Length >= 0; Length-- )
2242  if ( pNameFormal[Length] == '[' )
2243  break;
2244  // compare names before brace
2245  if ( Length > 0 )
2246  {
2247  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2248  if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2249  break;
2250  if ( j == Vec_PtrSize(vBundles) )
2251  pBundle = NULL;
2252  }
2253  }
2254  if ( pBundle == NULL )
2255  {
2256  char Buffer[1000];
2257 // printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
2258 // pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2259  pTermNew = Abc_NtkCreateBo( pNtk );
2260  sprintf( Buffer, "_temp_net%d", Abc_ObjId(pTermNew) );
2261  pNetAct = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2262  Abc_ObjAddFanin( pTermNew, pBox );
2263  Abc_ObjAddFanin( pNetAct, pTermNew );
2264  continue;
2265  }
2266  }
2267  // the bundle is found - add the connections
2268  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2269  {
2270  if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
2271  {
2272  sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.",
2273  pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
2274  // free the bundling
2275  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2276  Ver_ParseFreeBundle( pBundle );
2277  Vec_PtrFree( vBundles );
2278  pBox->pCopy = NULL;
2280  return 0;
2281  }
2282  pTermNew = Abc_NtkCreateBo( pNtk );
2283  Abc_ObjAddFanin( pTermNew, pBox );
2284  Abc_ObjAddFanin( pNetAct, pTermNew );
2285  i++;
2286  }
2287  i--;
2288  }
2289 
2290  // free the bundling
2291  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2292  Ver_ParseFreeBundle( pBundle );
2293  Vec_PtrFree( vBundles );
2294  pBox->pCopy = NULL;
2295  return 1;
2296 }
2297 
2298 
2299 /**Function*************************************************************
2300 
2301  Synopsis [Connects the defined boxes.]
2302 
2303  Description [Returns 2 if there are any undef boxes.]
2304 
2305  SideEffects []
2306 
2307  SeeAlso []
2308 
2309 ***********************************************************************/
2311 {
2312  Abc_Ntk_t * pNtk;
2313  Abc_Obj_t * pBox;
2314  int i, k, RetValue = 1;
2315  // go through all the modules
2316  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2317  {
2318  // go through all the boxes of this module
2319  Abc_NtkForEachBox( pNtk, pBox, k )
2320  {
2321  if ( Abc_ObjIsLatch(pBox) )
2322  continue;
2323  // skip internal boxes of the blackboxes
2324  if ( pBox->pData == NULL )
2325  continue;
2326  // if the network is undefined, it will be connected later
2327  if ( !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2328  {
2329  RetValue = 2;
2330  continue;
2331  }
2332  // connect the box
2333  if ( !Ver_ParseConnectBox( pMan, pBox ) )
2334  return 0;
2335  // if the network is a true blackbox, skip
2336  if ( Abc_NtkHasBlackbox((Abc_Ntk_t *)pBox->pData) )
2337  continue;
2338  // convert the box to the whitebox
2339  Abc_ObjBlackboxToWhitebox( pBox );
2340  }
2341  }
2342  return RetValue;
2343 }
2344 
2345 /**Function*************************************************************
2346 
2347  Synopsis [Collects the undef boxes and maps them into their instances.]
2348 
2349  Description []
2350 
2351  SideEffects []
2352 
2353  SeeAlso []
2354 
2355 ***********************************************************************/
2357 {
2358  Vec_Ptr_t * vUndefs;
2359  Abc_Ntk_t * pNtk, * pNtkBox;
2360  Abc_Obj_t * pBox;
2361  int i, k;
2362  // clear the module structures
2363  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2364  pNtk->pData = NULL;
2365  // go through all the blackboxes
2366  vUndefs = Vec_PtrAlloc( 16 );
2367  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2368  {
2369  Abc_NtkForEachBlackbox( pNtk, pBox, k )
2370  {
2371  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2372  if ( pNtkBox == NULL )
2373  continue;
2374  if ( Ver_NtkIsDefined(pNtkBox) )
2375  continue;
2376  if ( pNtkBox->pData == NULL )
2377  {
2378  // save the box
2379  Vec_PtrPush( vUndefs, pNtkBox );
2380  pNtkBox->pData = Vec_PtrAlloc( 16 );
2381  }
2382  // save the instance
2383  Vec_PtrPush( (Vec_Ptr_t *)pNtkBox->pData, pBox );
2384  }
2385  }
2386  return vUndefs;
2387 }
2388 
2389 /**Function*************************************************************
2390 
2391  Synopsis [Reports how many times each type of undefined box occurs.]
2392 
2393  Description []
2394 
2395  SideEffects []
2396 
2397  SeeAlso []
2398 
2399 ***********************************************************************/
2401 {
2402  Abc_Ntk_t * pNtk;
2403  Abc_Obj_t * pBox;
2404  int i, k, nBoxes;
2405  // clean
2406  nBoxes = 0;
2407  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2408  {
2409  pNtk->fHiePath = 0;
2410  if ( !Ver_NtkIsDefined(pNtk) )
2411  nBoxes++;
2412  }
2413  // count
2414  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2415  Abc_NtkForEachBlackbox( pNtk, pBox, k )
2416  if ( pBox->pData && !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2417  ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
2418  // print the stats
2419  printf( "Warning: The design contains %d undefined object types interpreted as blackboxes:\n", nBoxes );
2420  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2421  if ( !Ver_NtkIsDefined(pNtk) )
2422  printf( "%s (%d) ", Abc_NtkName(pNtk), pNtk->fHiePath );
2423  printf( "\n" );
2424  // clean
2425  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2426  pNtk->fHiePath = 0;
2427 }
2428 
2429 /**Function*************************************************************
2430 
2431  Synopsis [Returns 1 if there are non-driven nets.]
2432 
2433  Description []
2434 
2435  SideEffects []
2436 
2437  SeeAlso []
2438 
2439 ***********************************************************************/
2441 {
2442  Abc_Ntk_t * pNtk;
2443  Ver_Bundle_t * pBundle;
2444  Abc_Obj_t * pBox, * pNet;
2445  int i, k, j, m;
2446  // go through undef box types
2447  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2448  // go through instances of this type
2449  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2450  // go through the bundles of this instance
2451  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2452  // go through the actual nets of this bundle
2453  if ( pBundle )
2454  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2455  {
2456  if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
2457  if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
2458  return 1;
2459  }
2460  return 0;
2461 }
2462 
2463 /**Function*************************************************************
2464 
2465  Synopsis [Checks if formal nets with the given name are driven in any of the instances of undef boxes.]
2466 
2467  Description []
2468 
2469  SideEffects []
2470 
2471  SeeAlso []
2472 
2473 ***********************************************************************/
2474 int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
2475 {
2476  Ver_Bundle_t * pBundle = NULL;
2477  Abc_Obj_t * pBox, * pNet;
2478  int k, j, m;
2479  // go through instances of this type
2480  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2481  {
2482  // find a bundle with the given name in this instance
2483  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2484  if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
2485  break;
2486  // skip non-driven bundles
2487  if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2488  continue;
2489  // check if all nets are driven in this bundle
2490  assert(pBundle); // Verify that pBundle was assigned to.
2491  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2492  if ( Abc_ObjFaninNum(pNet) > 0 )
2493  return 1;
2494  }
2495  return 0;
2496 }
2497 
2498 /**Function*************************************************************
2499 
2500  Synopsis [Returns the non-driven bundle that is given distance from the end.]
2501 
2502  Description []
2503 
2504  SideEffects []
2505 
2506  SeeAlso []
2507 
2508 ***********************************************************************/
2510 {
2511  Ver_Bundle_t * pBundle;
2512  Abc_Obj_t * pBox, * pNet;
2513  int k, m;
2514  // go through instances of this type
2515  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2516  {
2517  if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2518  continue;
2519  // get the bundle given distance away
2520  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
2521  if ( pBundle == NULL )
2522  continue;
2523  // go through the actual nets of this bundle
2524  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2525  if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
2526  return pBundle;
2527  }
2528  return NULL;
2529 }
2530 
2531 /**Function*************************************************************
2532 
2533  Synopsis [Drives the bundle in the given undef box.]
2534 
2535  Description []
2536 
2537  SideEffects []
2538 
2539  SeeAlso []
2540 
2541 ***********************************************************************/
2542 int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 )
2543 {
2544  char Buffer[200];
2545  char * pName;
2546  Ver_Bundle_t * pBundle = NULL;
2547  Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
2548  int k, j, m;
2549 
2550  // drive this net in the undef box
2551  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle0->vNetsActual, pNetAct, m )
2552  {
2553  // create the formal net
2554  if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
2555  sprintf( Buffer, "%s", pBundle0->pNameFormal );
2556  else
2557  sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
2558  assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2559  pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2560  // connect it to the box
2561  pTerm = Abc_NtkCreateBo( pNtk );
2562  assert( Abc_NtkBoxNum(pNtk) <= 1 );
2563  pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2564  Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
2565  Abc_ObjAddFanin( pNetFormal, pTerm );
2566  Abc_ObjAddFanin( pTerm, pBox );
2567  }
2568 
2569  // go through instances of this type
2570  pName = Extra_UtilStrsav(pBundle0->pNameFormal);
2571  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2572  {
2573  // find a bundle with the given name in this instance
2574  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2575  if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
2576  break;
2577  // skip non-driven bundles
2578  if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2579  continue;
2580  // check if any nets are driven in this bundle
2581  assert(pBundle); // Verify pBundle was assigned to.
2582  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2583  if ( Abc_ObjFaninNum(pNetAct) > 0 )
2584  {
2585  sprintf( pMan->sError, "Missing specification of the I/Os of undefined box \"%s\".", Abc_NtkName(pNtk) );
2587  return 0;
2588  }
2589  // drive the nets by the undef box
2590  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2591  {
2592  pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
2593  Abc_ObjAddFanin( pTermNew, pBox );
2594  Abc_ObjAddFanin( pNetAct, pTermNew );
2595  }
2596  // remove the bundle
2597  Ver_ParseFreeBundle( pBundle ); pBundle = NULL;
2598  Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2599  }
2600  ABC_FREE( pName );
2601  return 1;
2602 }
2603 
2604 
2605 /**Function*************************************************************
2606 
2607  Synopsis [Drives the bundle in the given undef box.]
2608 
2609  Description []
2610 
2611  SideEffects []
2612 
2613  SeeAlso []
2614 
2615 ***********************************************************************/
2616 int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
2617 {
2618  char Buffer[200];
2619  Ver_Bundle_t * pBundle;
2620  Abc_Ntk_t * pNtk;
2621  Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
2622  int i, k, j, m, CountCur, CountTotal = -1;
2623  // iterate through the undef boxes
2624  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2625  {
2626  // count the number of unconnected bundles for instances of this type of box
2627  CountTotal = -1;
2628  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2629  {
2630  CountCur = 0;
2631  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2632  CountCur += (pBundle != NULL);
2633  if ( CountTotal == -1 )
2634  CountTotal = CountCur;
2635  else if ( CountTotal != CountCur )
2636  {
2637  sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.",
2638  CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
2640  return 0;
2641  }
2642  }
2643 
2644  // create formals
2645  pBox = (Abc_Obj_t *)Vec_PtrEntry( (Vec_Ptr_t *)pNtk->pData, 0 );
2646  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2647  {
2648  if ( pBundle == NULL )
2649  continue;
2650  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2651  {
2652  // find create the formal net
2653  if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
2654  sprintf( Buffer, "%s", pBundle->pNameFormal );
2655  else
2656  sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
2657  assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2658  pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2659  // connect
2660  pTerm = Abc_NtkCreateBi( pNtk );
2661  assert( Abc_NtkBoxNum(pNtk) <= 1 );
2662  pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2663  Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
2664  Abc_ObjAddFanin( pTerm, pNetFormal );
2665  Abc_ObjAddFanin( pBox2, pTerm );
2666  }
2667  }
2668 
2669  // go through all the boxes
2670  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2671  {
2672  // go through all the bundles
2673  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2674  {
2675  if ( pBundle == NULL )
2676  continue;
2677  // drive the nets by the undef box
2678  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2679  {
2680  pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
2681  Abc_ObjAddFanin( pBox, pTermNew );
2682  Abc_ObjAddFanin( pTermNew, pNetAct );
2683  }
2684  // remove the bundle
2685  Ver_ParseFreeBundle( pBundle );
2686  Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2687  }
2688 
2689  // free the bundles
2690  Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
2691  pBox->pCopy = NULL;
2692  }
2693  }
2694  return 1;
2695 }
2696 
2697 
2698 /**Function*************************************************************
2699 
2700  Synopsis [Returns the max size of any undef box.]
2701 
2702  Description []
2703 
2704  SideEffects []
2705 
2706  SeeAlso []
2707 
2708 ***********************************************************************/
2710 {
2711  Abc_Ntk_t * pNtk;
2712  Abc_Obj_t * pBox;
2713  int i, k, nMaxSize = 0;
2714  // go through undef box types
2715  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2716  // go through instances of this type
2717  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2718  // check the number of bundles of this instance
2719  if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2720  nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
2721  return nMaxSize;
2722 }
2723 
2724 /**Function*************************************************************
2725 
2726  Synopsis [Prints the comprehensive report into a log file.]
2727 
2728  Description []
2729 
2730  SideEffects []
2731 
2732  SeeAlso []
2733 
2734 ***********************************************************************/
2736 {
2737  Abc_Ntk_t * pNtk, * pNtkBox;
2738  Abc_Obj_t * pBox;
2739  FILE * pFile;
2740  char * pNameGeneric;
2741  char Buffer[1000];
2742  int i, k, Count1 = 0;
2743 
2744  // open the log file
2745  pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
2746  sprintf( Buffer, "%s.log", pNameGeneric );
2747  ABC_FREE( pNameGeneric );
2748  pFile = fopen( Buffer, "w" );
2749 
2750  // count the total number of instances and how many times they occur
2751  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2752  pNtk->fHieVisited = 0;
2753  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2754  Abc_NtkForEachBox( pNtk, pBox, k )
2755  {
2756  if ( Abc_ObjIsLatch(pBox) )
2757  continue;
2758  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2759  if ( pNtkBox == NULL )
2760  continue;
2761  pNtkBox->fHieVisited++;
2762  }
2763  // print each box and its stats
2764  fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
2765  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2766  {
2767  fprintf( pFile, "%-50s : ", Abc_NtkName(pNtk) );
2768  if ( !Ver_NtkIsDefined(pNtk) )
2769  fprintf( pFile, "undefbox" );
2770  else if ( Abc_NtkHasBlackbox(pNtk) )
2771  fprintf( pFile, "blackbox" );
2772  else
2773  fprintf( pFile, "logicbox" );
2774  fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
2775 // fprintf( pFile, "\n " );
2776  fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
2777  fprintf( pFile, " po = %4d", Abc_NtkPoNum(pNtk) );
2778  fprintf( pFile, " nd = %8d", Abc_NtkNodeNum(pNtk) );
2779  fprintf( pFile, " lat = %6d", Abc_NtkLatchNum(pNtk) );
2780  fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
2781  fprintf( pFile, "\n" );
2782  Count1 += (Abc_NtkPoNum(pNtk) == 1);
2783  }
2784  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2785  pNtk->fHieVisited = 0;
2786  fprintf( pFile, "The number of modules with one output = %d (%.2f %%).\n", Count1, 100.0 * Count1/Vec_PtrSize(pMan->pDesign->vModules) );
2787 
2788  // report instances with dangling outputs
2789  if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2790  {
2791  Vec_Ptr_t * vBundles;
2792  Ver_Bundle_t * pBundle;
2793  int j, nActNets, Counter = 0;
2794  // count the number of instances with dangling outputs
2795  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2796  {
2797  Abc_NtkForEachBox( pNtk, pBox, k )
2798  {
2799  if ( Abc_ObjIsLatch(pBox) )
2800  continue;
2801  vBundles = (Vec_Ptr_t *)pBox->pCopy;
2802  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2803  if ( pNtkBox == NULL )
2804  continue;
2805  if ( !Ver_NtkIsDefined(pNtkBox) )
2806  continue;
2807  // count the number of actual nets
2808  nActNets = 0;
2809  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2810  nActNets += Vec_PtrSize(pBundle->vNetsActual);
2811  // the box is defined and will be connected
2812  if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2813  Counter++;
2814  }
2815  }
2816  if ( Counter == 0 )
2817  fprintf( pFile, "The outputs of all box instances are connected.\n" );
2818  else
2819  {
2820  fprintf( pFile, "\n" );
2821  fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
2822  // enumerate through the boxes
2823  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2824  {
2825  Abc_NtkForEachBox( pNtk, pBox, k )
2826  {
2827  if ( Abc_ObjIsLatch(pBox) )
2828  continue;
2829  vBundles = (Vec_Ptr_t *)pBox->pCopy;
2830  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2831  if ( pNtkBox == NULL )
2832  continue;
2833  if ( !Ver_NtkIsDefined(pNtkBox) )
2834  continue;
2835  // count the number of actual nets
2836  nActNets = 0;
2837  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2838  nActNets += Vec_PtrSize(pBundle->vNetsActual);
2839  // the box is defined and will be connected
2840  if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2841  fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
2842  Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
2843  }
2844  }
2845  }
2846  }
2847  fclose( pFile );
2848  printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
2849 }
2850 
2851 
2852 /**Function*************************************************************
2853 
2854  Synopsis [Attaches the boxes to the network.]
2855 
2856  Description [This procedure is called after the design is parsed.
2857  At that point, all the defined models have their PIs present.
2858  They are connected first. Next undef boxes are processed (if present).
2859  Iteratively, one bundle is selected to be driven by the undef boxes in such
2860  a way that there is no conflict (if it is driven by an instance of the box,
2861  no other net will be driven twice by the same formal net of some other instance
2862  of the same box). In the end, all the remaining nets that cannot be driven
2863  by the undef boxes are connected to the undef boxes as inputs.]
2864 
2865  SideEffects []
2866 
2867  SeeAlso []
2868 
2869 ***********************************************************************/
2871 {
2872  int fPrintLog = 1;
2873  Abc_Ntk_t * pNtk = NULL;
2874  Ver_Bundle_t * pBundle;
2875  Vec_Ptr_t * vUndefs;
2876  int i, RetValue, Counter, nMaxBoxSize;
2877 
2878  // print the log file
2879  if ( fPrintLog && pMan->pDesign->vModules && Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2880  Ver_ParsePrintLog( pMan );
2881 
2882  // connect defined boxes
2883  RetValue = Ver_ParseConnectDefBoxes( pMan );
2884  if ( RetValue < 2 )
2885  return RetValue;
2886 
2887  // report the boxes
2888  Ver_ParseReportUndefBoxes( pMan );
2889 
2890  // collect undef box types and their actual instances
2891  vUndefs = Ver_ParseCollectUndefBoxes( pMan );
2892  assert( Vec_PtrSize( vUndefs ) > 0 );
2893 
2894  // go through all undef box types
2895  Counter = 0;
2896  nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
2897  while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
2898  {
2899  // go through undef box types
2900  pBundle = NULL;
2901  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2902  if ( (pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter )) )
2903  break;
2904  if ( pBundle == NULL )
2905  {
2906  Counter++;
2907  continue;
2908  }
2909  // drive this bundle by this box
2910  if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
2911  return 0;
2912  }
2913 
2914  // make all the remaining bundles the drivers of undefs
2915  if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
2916  return 0;
2917 
2918  // cleanup
2919  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2920  {
2921  Vec_PtrFree( (Vec_Ptr_t *)pNtk->pData );
2922  pNtk->pData = NULL;
2923  }
2924  Vec_PtrFree( vUndefs );
2925  return 1;
2926 }
2927 
2928 
2929 /**Function*************************************************************
2930 
2931  Synopsis [Creates PI terminal and net.]
2932 
2933  Description []
2934 
2935  SideEffects []
2936 
2937  SeeAlso []
2938 
2939 ***********************************************************************/
2940 Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
2941 {
2942  Abc_Obj_t * pNet, * pTerm;
2943  // get the PI net
2944 // pNet = Ver_ParseFindNet( pNtk, pName );
2945 // if ( pNet )
2946 // printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
2947  pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2948  // add the PI node
2949  pTerm = Abc_NtkCreatePi( pNtk );
2950  Abc_ObjAddFanin( pNet, pTerm );
2951  return pTerm;
2952 }
2953 
2954 /**Function*************************************************************
2955 
2956  Synopsis [Creates PO terminal and net.]
2957 
2958  Description []
2959 
2960  SideEffects []
2961 
2962  SeeAlso []
2963 
2964 ***********************************************************************/
2965 Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
2966 {
2967  Abc_Obj_t * pNet, * pTerm;
2968  // get the PO net
2969 // pNet = Ver_ParseFindNet( pNtk, pName );
2970 // if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
2971 // printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
2972  pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2973  // add the PO node
2974  pTerm = Abc_NtkCreatePo( pNtk );
2975  Abc_ObjAddFanin( pTerm, pNet );
2976  return pTerm;
2977 }
2978 
2979 /**Function*************************************************************
2980 
2981  Synopsis [Create a latch with the given input/output.]
2982 
2983  Description [By default, the latch value is a don't-care.]
2984 
2985  SideEffects []
2986 
2987  SeeAlso []
2988 
2989 ***********************************************************************/
2991 {
2992  Abc_Obj_t * pLatch, * pTerm;
2993  // add the BO terminal
2994  pTerm = Abc_NtkCreateBi( pNtk );
2995  Abc_ObjAddFanin( pTerm, pNetLI );
2996  // add the latch box
2997  pLatch = Abc_NtkCreateLatch( pNtk );
2998  Abc_ObjAddFanin( pLatch, pTerm );
2999  // add the BI terminal
3000  pTerm = Abc_NtkCreateBo( pNtk );
3001  Abc_ObjAddFanin( pTerm, pLatch );
3002  // get the LO net
3003  Abc_ObjAddFanin( pNetLO, pTerm );
3004  // set latch name
3005  Abc_ObjAssignName( pLatch, Abc_ObjName(pNetLO), "L" );
3006  Abc_LatchSetInitDc( pLatch );
3007  return pLatch;
3008 }
3009 
3010 /**Function*************************************************************
3011 
3012  Synopsis [Creates inverter and returns its net.]
3013 
3014  Description []
3015 
3016  SideEffects []
3017 
3018  SeeAlso []
3019 
3020 ***********************************************************************/
3022 {
3023  Abc_Obj_t * pObj;
3024  pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
3025  pNet = Abc_NtkCreateNet( pNtk );
3026  Abc_ObjAddFanin( pNet, pObj );
3027  return pNet;
3028 }
3029 
3030 
3031 ////////////////////////////////////////////////////////////////////////
3032 /// END OF FILE ///
3033 ////////////////////////////////////////////////////////////////////////
3034 
3035 
3037 
Mio_Gate_t * Mio_LibraryReadBuf(Mio_Library_t *pLib)
Definition: mioApi.c:47
char * memset()
Ver_Bundle_t * Ver_ParseGetNondrivenBundle(Abc_Ntk_t *pNtk, int Counter)
Definition: verCore.c:2509
static unsigned Abc_ObjId(Abc_Obj_t *pObj)
Definition: abc.h:329
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition: mioApi.c:99
static Abc_Obj_t * Ver_ParseCreateInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pNet)
Definition: verCore.c:3021
void st__free_table(st__table *table)
Definition: st.c:81
int Ver_ParseSignalPrefix(Ver_Man_t *pMan, char **ppWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:635
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static int Ver_ParseAssign(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:1087
int Ver_StreamGetLineNumber(Ver_Stream_t *p)
Definition: verStream.c:224
void * Ver_FormulaParser(char *pFormula, void *pMan, Vec_Ptr_t *vNames, Vec_Ptr_t *vStackFn, Vec_Int_t *vStackOp, char *pErrorMessage)
FUNCTION DEFINITIONS ///.
Definition: verFormula.c:76
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
int Ver_FindGateInput(Mio_Gate_t *pGate, char *pName)
Definition: verCore.c:1525
int Ver_ParseDriveInputs(Ver_Man_t *pMan, Vec_Ptr_t *vUndefs)
Definition: verCore.c:2616
static int Ver_ObjIsConnected(Abc_Obj_t *pObj)
Definition: verCore.c:78
static Hop_Obj_t * Hop_ManConst1(Hop_Man_t *p)
Definition: hop.h:132
static int Ver_ParseInitial(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:991
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Ver_ParseSignalSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:699
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Mio_Pin_t * Mio_GateReadPins(Mio_Gate_t *pGate)
Definition: mioApi.c:147
static int Abc_ObjIsLatch(Abc_Obj_t *pObj)
Definition: abc.h:356
ABC_DLL Abc_Des_t * Abc_DesCreate(char *pName)
DECLARATIONS ///.
Definition: abcLib.c:45
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
int glo_fMapped
Definition: verCore.c:80
static void Ver_ParseInternal(Ver_Man_t *p)
Definition: verCore.c:200
ABC_DLL int Abc_DesAddModel(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition: abcLib.c:226
Vec_Ptr_t * Ver_ParseCollectUndefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2356
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
static int Ver_ParseBox(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkBox)
Definition: verCore.c:1732
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
char * Mio_GateReadOutName(Mio_Gate_t *pGate)
Definition: mioApi.c:144
Abc_Des_t * Ver_ParseFile(char *pFileName, Abc_Des_t *pGateLib, int fCheck, int fUseMemMan)
MACRO DEFINITIONS ///.
Definition: verCore.c:165
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
char * Mio_PinReadName(Mio_Pin_t *pPin)
Definition: mioApi.c:170
Hop_Obj_t * Hop_CreateExor(Hop_Man_t *p, int nVars)
Definition: hopOper.c:362
Vec_Int_t vFanins
Definition: abc.h:143
static int Ver_ParseSignal(Ver_Man_t *p, Abc_Ntk_t *pNtk, Ver_SignalType_t SigType)
Definition: verCore.c:805
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static void Ver_ParseFreeData(Ver_Man_t *p)
Definition: verCore.c:258
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
static void Ver_ParseStop(Ver_Man_t *p)
Definition: verCore.c:142
int Ver_ParseDriveFormal(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_Bundle_t *pBundle0)
Definition: verCore.c:2542
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
GateType
Definition: csat_apis.h:49
#define st__is_member(table, key)
Definition: st.h:70
ABC_DLL void Abc_NtkFinalizeRead(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:360
Mio_Pin_t * Mio_PinReadNext(Mio_Pin_t *pPin)
Definition: mioApi.c:179
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Abc_LatchSetInitDc(Abc_Obj_t *pLatch)
Definition: abc.h:420
static Abc_Obj_t * Ver_ParseCreatePi(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:2940
static Hop_Obj_t * Hop_Not(Hop_Obj_t *p)
Definition: hop.h:127
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Definition: hop.h:65
static int Ver_ParseFlopStandard(Ver_Man_t *pMan, Abc_Ntk_t *pNtk)
Definition: verCore.c:1426
char * Extra_UtilStrsav(const char *s)
void Hop_ManStop(Hop_Man_t *p)
Definition: hopMan.c:84
char * Ver_StreamGetWord(Ver_Stream_t *p, char *pCharsToStop)
Definition: verStream.c:397
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
int strcmp()
void * pData
Definition: abc.h:203
Mio_Gate_t * Mio_LibraryReadConst1(Mio_Library_t *pLib)
Definition: mioApi.c:50
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
int Ver_ParseFormalNetsAreDriven(Abc_Ntk_t *pNtk, char *pNameFormal)
Definition: verCore.c:2474
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
int Mio_GateReadPinNum(Mio_Gate_t *pGate)
Definition: mioApi.c:151
static Abc_Obj_t * Ver_ParseCreateLatch(Abc_Ntk_t *pNtk, Abc_Obj_t *pNetLI, Abc_Obj_t *pNetLO)
Definition: verCore.c:2990
char Ver_StreamScanChar(Ver_Stream_t *p)
Definition: verStream.c:258
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
int st__strhash(const char *string, int modulus)
Definition: st.c:449
void * pManFunc
Definition: abc.h:191
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
static int Ver_ParseAttachBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2870
int Ver_ParseLookupSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:563
ABC_DLL void Abc_DesFree(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition: abcLib.c:94
static int Ver_ParseConnectBox(Ver_Man_t *pMan, Abc_Obj_t *pBox)
Definition: verCore.c:2071
Abc_Obj_t * pCopy
Definition: abc.h:148
void Ver_StreamSkipToChars(Ver_Stream_t *p, char *pCharsToStop)
Definition: verStream.c:349
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Hop_Obj_t * Hop_CreateAnd(Hop_Man_t *p, int nVars)
Definition: hopOper.c:320
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
static int Abc_NtkHasBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:258
typedefABC_NAMESPACE_HEADER_START struct Ver_Man_t_ Ver_Man_t
INCLUDES ///.
Definition: ver.h:45
int Ver_ParseConstant(Ver_Man_t *pMan, char *pWord)
Definition: verCore.c:753
static int Ver_ParseGateStandard(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_GateType_t GateType)
Definition: verCore.c:1330
ABC_DLL int Abc_NtkCheckRead(Abc_Ntk_t *pNtk)
Definition: abcCheck.c:77
void * pGenlib
Definition: abc.h:226
static void Ver_ParseRemoveSuffixTable(Ver_Man_t *pMan)
Definition: verCore.c:612
char * Extra_FileNameGeneric(char *FileName)
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define Abc_NtkForEachBlackbox(pNtk, pObj, i)
Definition: abc.h:509
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:507
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeBuf(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:692
if(last==0)
Definition: sparse_int.h:34
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
char * pNameFormal
Definition: verCore.c:85
int Ver_ParseCheckNondrivenNets(Vec_Ptr_t *vUndefs)
Definition: verCore.c:2440
void Ver_ParsePrintLog(Ver_Man_t *pMan)
Definition: verCore.c:2735
static Abc_Obj_t * Ver_ParseCreatePo(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:2965
static Abc_Obj_t * Abc_NtkCreateLatch(Abc_Ntk_t *pNtk)
Definition: abc.h:309
STRUCTURE DEFINITIONS ///.
Definition: mioInt.h:61
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
char * sprintf()
static int Counter
static Abc_Obj_t * Abc_NtkCreateBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:311
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
static int Ver_ParseAlways(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:892
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
void Extra_ProgressBarStop(ProgressBar *p)
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
int Ver_ParseInsertsSuffix(Ver_Man_t *pMan, char *pWord, int nMsb, int nLsb)
Definition: verCore.c:587
static void Abc_ObjBlackboxToWhitebox(Abc_Obj_t *pObj)
Definition: abc.h:361
#define Abc_NtkForEachBox(pNtk, pObj, i)
Definition: abc.h:495
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
char * strcpy()
static Abc_Obj_t * Abc_NtkBox(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:319
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Abc_LatchSetInit1(Abc_Obj_t *pLatch)
Definition: abc.h:419
char * pSpec
Definition: abc.h:159
Mio_Gate_t * Mio_GateReadTwin(Mio_Gate_t *pGate)
Definition: mioApi.c:150
Hop_Obj_t * Hop_CreateOr(Hop_Man_t *p, int nVars)
Definition: hopOper.c:341
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
ABC_DLL Abc_Ntk_t * Abc_DesFindModelByName(Abc_Des_t *p, char *pName)
Definition: abcLib.c:249
Abc_Ntk_t * pNtk
Definition: abc.h:130
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Ver_ParseGate(Ver_Man_t *p, Abc_Ntk_t *pNtk, Mio_Gate_t *pGate)
Definition: verCore.c:1550
static char * Abc_NtkName(Abc_Ntk_t *pNtk)
Definition: abc.h:270
Ver_GateType_t
Definition: verCore.c:43
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_NtkFunc_t ntkFunc
Definition: abc.h:157
void Ver_ParseReportUndefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2400
int Ver_StreamGetCurPosition(Ver_Stream_t *p)
Definition: verStream.c:208
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
void Ver_StreamFree(Ver_Stream_t *p)
Definition: verStream.c:157
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
int strncmp()
Ver_Stream_t * Ver_StreamAlloc(char *pFileName)
FUNCTION DEFINITIONS ///.
Definition: verStream.c:74
void Ver_ParseFreeBundle(Ver_Bundle_t *pBundle)
Definition: verCore.c:2053
Vec_Ptr_t * vModules
Definition: abc.h:223
#define st__foreach_item(table, gen, key, value)
Definition: st.h:107
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
#define assert(ex)
Definition: util_old.h:213
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
int strlen()
static int Abc_ObjIsBox(Abc_Obj_t *pObj)
Definition: abc.h:357
static int Ver_ParseModule(Ver_Man_t *p)
Definition: verCore.c:401
void * Ver_FormulaReduction(char *pFormula, void *pMan, Vec_Ptr_t *vNames, char *pErrorMessage)
Definition: verFormula.c:435
static Hop_Obj_t * Hop_ManConst0(Hop_Man_t *p)
Definition: hop.h:131
static int Abc_ObjFaninId(Abc_Obj_t *pObj, int i)
Definition: abc.h:366
void * pData
Definition: abc.h:145
static Ver_Man_t * Ver_ParseStart(char *pFileName, Abc_Des_t *pGateLib)
FUNCTION DEFINITIONS ///.
Definition: verCore.c:104
Abc_Ntk_t * Ver_ParseFindOrCreateNetwork(Ver_Man_t *pMan, char *pName)
Definition: verCore.c:301
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
int Ver_StreamGetFileSize(Ver_Stream_t *p)
Definition: verStream.c:192
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Abc_Des_t * pDesign
Definition: abc.h:180
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
char * Mio_GateReadName(Mio_Gate_t *pGate)
Definition: mioApi.c:143
int Ver_ParseMaxBoxSize(Vec_Ptr_t *vUndefs)
Definition: verCore.c:2709
Mio_Gate_t * Mio_LibraryReadConst0(Mio_Library_t *pLib)
Definition: mioApi.c:49
static void Abc_LatchSetInit0(Abc_Obj_t *pLatch)
Definition: abc.h:418
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
char * pName
Definition: abc.h:158
int fHiePath
Definition: abc.h:183
int fHieVisited
Definition: abc.h:182
int Ver_ParseConnectDefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2310
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
static Abc_Obj_t * Abc_NtkCreateNet(Abc_Ntk_t *pNtk)
Definition: abc.h:307
Ver_SignalType_t
DECLARATIONS ///.
Definition: verCore.c:33
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328