ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
verCore.c
Go to the documentation of this file.
1
20
21#include "ver.h"
22#include "map/mio/mio.h"
23#include "base/main/main.h"
24
25ABC_NAMESPACE_IMPL_START
26
27
31
32// types of verilog signals
41
42// types of verilog gates
53
54static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Des_t * pGateLib );
55static void Ver_ParseStop( Ver_Man_t * p );
56static void Ver_ParseFreeData( Ver_Man_t * p );
57static void Ver_ParseInternal( Ver_Man_t * p );
58static int Ver_ParseModule( Ver_Man_t * p );
59static int Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType );
60static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
61static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
62static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
63static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType );
64static int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk );
65static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
66static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
67static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
68static int Ver_ParseAttachBoxes( Ver_Man_t * pMan );
69
70static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
71static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
72static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
73static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
74
75static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan );
76
77static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); }
78static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
79
80int glo_fMapped = 0; // this is bad!
81
82typedef struct Ver_Bundle_t_ Ver_Bundle_t;
83struct 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
92
104Ver_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
142void Ver_ParseStop( Ver_Man_t * p )
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
165Abc_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
200void Ver_ParseInternal( Ver_Man_t * pMan )
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." );
217 Ver_ParsePrintErrorMessage( pMan );
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 );
241 Ver_ParsePrintErrorMessage( pMan );
242 return;
243 }
244 }
245}
246
258void Ver_ParseFreeData( Ver_Man_t * p )
259{
260 if ( p->pDesign )
261 {
262 Abc_DesFree( p->pDesign, NULL );
263 p->pDesign = NULL;
264 }
265}
266
278void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
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
301Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
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
328Abc_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
351int 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 );
366 Ver_ParsePrintErrorMessage( pMan );
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 );
383 Ver_ParsePrintErrorMessage( pMan );
384 return 0;
385 }
386 }
387 return 1;
388}
389
401int Ver_ParseModule( Ver_Man_t * pMan )
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 parenthesis
416 if ( Ver_StreamPopChar(p) != '(' )
417 {
418 sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
419 Ver_ParsePrintErrorMessage( pMan );
420 return 0;
421 }
422
423 // skip to the end of parentheses
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 parenthesis after \"module\"." );
436 Ver_ParsePrintErrorMessage( pMan );
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
547 Ver_ParseRemoveSuffixTable( pMan );
548 return 1;
549}
550
551
563int 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
587int 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
612void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan )
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
635int 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." );
648 Ver_ParsePrintErrorMessage( pMan );
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 parenthesis
658 while ( *pWord && *pWord != ']' )
659 pWord++;
660 if ( *pWord == 0 )
661 {
662 sprintf( pMan->sError, "Cannot find closing bracket in this line." );
663 Ver_ParsePrintErrorMessage( pMan );
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
699int 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 );
712 Ver_ParsePrintErrorMessage( pMan );
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 );
731 Ver_ParsePrintErrorMessage( pMan );
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
753int 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." );
764 Ver_ParsePrintErrorMessage( pMan );
765 return 0;
766 }
767 assert( *pWord == '\'' );
768 pWord++;
769 if ( *pWord != 'b' )
770 {
771 sprintf( pMan->sError, "Currently can only handle binary constants." );
772 Ver_ParsePrintErrorMessage( pMan );
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." );
783 Ver_ParsePrintErrorMessage( pMan );
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
805int 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 ;)." );
877 Ver_ParsePrintErrorMessage( pMan );
878 return 0;
879}
880
892int 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, ")" );
906 Ver_StreamPopChar(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 );
934 Ver_ParsePrintErrorMessage( pMan );
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 );
942 Ver_ParsePrintErrorMessage( pMan );
943 return 0;
944 }
945 if ( Symbol == '<' )
946 Ver_StreamPopChar(p);
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 );
965 Ver_ParsePrintErrorMessage( pMan );
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
991int 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 );
1024 Ver_ParsePrintErrorMessage( pMan );
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 );
1032 Ver_ParsePrintErrorMessage( pMan );
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." );
1048 Ver_ParsePrintErrorMessage( pMan );
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) );
1063 Ver_ParsePrintErrorMessage( pMan );
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
1087int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
1088{
1089 char Buffer[1000], Buffer2[2000];
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 );
1133 Ver_ParsePrintErrorMessage( pMan );
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 );
1144 Ver_ParsePrintErrorMessage( pMan );
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 );
1157 Ver_ParsePrintErrorMessage( pMan );
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 );
1179 Ver_ParsePrintErrorMessage( pMan );
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 );
1204 Ver_ParsePrintErrorMessage( pMan );
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 );
1211 Ver_ParsePrintErrorMessage( pMan );
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) );
1225 Ver_ParsePrintErrorMessage( pMan );
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" ) )
1234 pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0((Mio_Library_t *)Abc_FrameReadLibGen());
1235 else if ( !strcmp( pEquation, "1\'b1" ) )
1236 pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1((Mio_Library_t *)Abc_FrameReadLibGen());
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." );
1248 Ver_ParsePrintErrorMessage( pMan );
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
1254 pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf((Mio_Library_t *)Abc_FrameReadLibGen());
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) );
1258 Ver_ParsePrintErrorMessage( pMan );
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 {
1275 Ver_ParsePrintErrorMessage( pMan );
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 );
1303 Ver_ParsePrintErrorMessage( pMan );
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
1330int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType )
1331{
1332 extern void Ver_StreamMove( Ver_Stream_t * p );
1333 Ver_Stream_t * p = pMan->pReader;
1334 Abc_Obj_t * pNet, * pNode;
1335 char * pWord, Symbol;
1336
1337 // convert from the blackbox into the network with local functions representated by AIGs
1338 if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1339 return 0;
1340 Ver_StreamMove( p );
1341
1342 // this is gate name - throw it away
1343 if ( Ver_StreamPopChar(p) != '(' )
1344 {
1345 sprintf( pMan->sError, "Cannot parse a standard gate (expected opening parenthesis)." );
1346 Ver_ParsePrintErrorMessage( pMan );
1347 return 0;
1348 }
1349 Ver_ParseSkipComments( pMan );
1350
1351 // create the node
1352 pNode = Abc_NtkCreateNode( pNtk );
1353
1354 // parse pairs of formal/actural inputs
1355 while ( 1 )
1356 {
1357 // parse the output name
1358 pWord = Ver_ParseGetName( pMan );
1359 if ( pWord == NULL )
1360 return 0;
1361 // get the net corresponding to this output
1362 pNet = Ver_ParseFindNet( pNtk, pWord );
1363 if ( pNet == NULL )
1364 {
1365 sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1366 Ver_ParsePrintErrorMessage( pMan );
1367 return 0;
1368 }
1369 // if this is the first net, add it as an output
1370 if ( Abc_ObjFanoutNum(pNode) == 0 )
1371 Abc_ObjAddFanin( pNet, pNode );
1372 else
1373 Abc_ObjAddFanin( pNode, pNet );
1374 // check if it is the end of gate
1375 Ver_ParseSkipComments( pMan );
1376 Symbol = Ver_StreamPopChar(p);
1377 if ( Symbol == ')' )
1378 break;
1379 // skip comma
1380 if ( Symbol != ',' )
1381 {
1382 sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing parenthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1383 Ver_ParsePrintErrorMessage( pMan );
1384 return 0;
1385 }
1386 Ver_ParseSkipComments( pMan );
1387 }
1388 if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
1389 {
1390 sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1391 Ver_ParsePrintErrorMessage( pMan );
1392 return 0;
1393 }
1394
1395 // check if it is the end of gate
1396 Ver_ParseSkipComments( pMan );
1397 if ( Ver_StreamPopChar(p) != ';' )
1398 {
1399 sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1400 Ver_ParsePrintErrorMessage( pMan );
1401 return 0;
1402 }
1403 // add logic function
1404 if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
1405 pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1406 else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
1407 pNode->pData = Hop_CreateOr( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1408 else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
1409 pNode->pData = Hop_CreateExor( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1410 else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
1411 pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1412 if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
1413 pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
1414 return 1;
1415}
1416
1428int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
1429{
1430 Ver_Stream_t * p = pMan->pReader;
1431 Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
1432 char * pWord, Symbol;
1433
1434 // convert from the blackbox into the network with local functions representated by AIGs
1435 if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1436 return 0;
1437
1438 // this is gate name - throw it away
1439 if ( Ver_StreamPopChar(p) != '(' )
1440 {
1441 sprintf( pMan->sError, "Cannot parse a standard gate (expected opening parenthesis)." );
1442 Ver_ParsePrintErrorMessage( pMan );
1443 return 0;
1444 }
1445 Ver_ParseSkipComments( pMan );
1446
1447 // parse the output name
1448 pWord = Ver_ParseGetName( pMan );
1449 if ( pWord == NULL )
1450 return 0;
1451 // get the net corresponding to this output
1452 pNetLo = Ver_ParseFindNet( pNtk, pWord );
1453 if ( pNetLo == NULL )
1454 {
1455 sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1456 Ver_ParsePrintErrorMessage( pMan );
1457 return 0;
1458 }
1459
1460 // check if it is the end of gate
1461 Ver_ParseSkipComments( pMan );
1462 Symbol = Ver_StreamPopChar(p);
1463 if ( Symbol == ')' )
1464 {
1465 sprintf( pMan->sError, "Cannot parse the flop." );
1466 Ver_ParsePrintErrorMessage( pMan );
1467 return 0;
1468 }
1469 // skip comma
1470 if ( Symbol != ',' )
1471 {
1472 sprintf( pMan->sError, "Cannot parse the flop." );
1473 Ver_ParsePrintErrorMessage( pMan );
1474 return 0;
1475 }
1476 Ver_ParseSkipComments( pMan );
1477
1478 // parse the output name
1479 pWord = Ver_ParseGetName( pMan );
1480 if ( pWord == NULL )
1481 return 0;
1482 // get the net corresponding to this output
1483 pNetLi = Ver_ParseFindNet( pNtk, pWord );
1484 if ( pNetLi == NULL )
1485 {
1486 sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1487 Ver_ParsePrintErrorMessage( pMan );
1488 return 0;
1489 }
1490
1491 // check if it is the end of gate
1492 Ver_ParseSkipComments( pMan );
1493 Symbol = Ver_StreamPopChar(p);
1494 if ( Symbol != ')' )
1495 {
1496 sprintf( pMan->sError, "Cannot parse the flop." );
1497 Ver_ParsePrintErrorMessage( pMan );
1498 return 0;
1499 }
1500
1501 // check if it is the end of gate
1502 Ver_ParseSkipComments( pMan );
1503 if ( Ver_StreamPopChar(p) != ';' )
1504 {
1505 sprintf( pMan->sError, "Cannot parse the flop." );
1506 Ver_ParsePrintErrorMessage( pMan );
1507 return 0;
1508 }
1509
1510 // create the latch
1511 pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
1512 Abc_LatchSetInit0( pLatch );
1513 return 1;
1514}
1515
1527int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
1528{
1529 Mio_Pin_t * pGatePin;
1530 int i;
1531 for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
1532 if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
1533 return i;
1534 if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
1535 return i;
1536 if ( Mio_GateReadTwin(pGate) && strcmp(pName, Mio_GateReadOutName(Mio_GateReadTwin(pGate))) == 0 )
1537 return i+1;
1538 return -1;
1539}
1540
1552int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
1553{
1554 Ver_Stream_t * p = pMan->pReader;
1555 Abc_Obj_t * pNetActual, * pNode, * pNode2 = NULL;
1556 char * pWord, Symbol;
1557 int Input, i, nFanins = Mio_GateReadPinNum(pGate);
1558
1559 // convert from the blackbox into the network with local functions representated by gates
1560 if ( 1 != pMan->fMapped )
1561 {
1562 sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
1563 Ver_ParsePrintErrorMessage( pMan );
1564 return 0;
1565 }
1566
1567 // update the network type if needed
1568 if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
1569 return 0;
1570
1571 // parse the directive and set the pointers to the PIs/POs of the gate
1572 pWord = Ver_ParseGetName( pMan );
1573 if ( pWord == NULL )
1574 return 0;
1575 // this is gate name - throw it away
1576 if ( Ver_StreamPopChar(p) != '(' )
1577 {
1578 sprintf( pMan->sError, "Cannot parse gate %s (expected opening parenthesis).", Mio_GateReadName(pGate) );
1579 Ver_ParsePrintErrorMessage( pMan );
1580 return 0;
1581 }
1582 Ver_ParseSkipComments( pMan );
1583
1584 // start the node
1585 pNode = Abc_NtkCreateNode( pNtk );
1586 pNode->pData = pGate;
1587 if ( Mio_GateReadTwin(pGate) )
1588 {
1589 pNode2 = Abc_NtkCreateNode( pNtk );
1590 pNode2->pData = Mio_GateReadTwin(pGate);
1591 }
1592 // parse pairs of formal/actural inputs
1593 Vec_IntClear( pMan->vPerm );
1594 while ( 1 )
1595 {
1596 // process one pair of formal/actual parameters
1597 if ( Ver_StreamPopChar(p) != '.' )
1598 {
1599 sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
1600 Ver_ParsePrintErrorMessage( pMan );
1601 return 0;
1602 }
1603
1604 // parse the formal name
1605 pWord = Ver_ParseGetName( pMan );
1606 if ( pWord == NULL )
1607 return 0;
1608
1609 // find the corresponding pin of the gate
1610 Input = Ver_FindGateInput( pGate, pWord );
1611 if ( Input == -1 )
1612 {
1613 sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
1614 Ver_ParsePrintErrorMessage( pMan );
1615 return 0;
1616 }
1617
1618 // open the parenthesis
1619 if ( Ver_StreamPopChar(p) != '(' )
1620 {
1621 sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening parenthesis).", pWord, Mio_GateReadName(pGate) );
1622 Ver_ParsePrintErrorMessage( pMan );
1623 return 0;
1624 }
1625
1626 // parse the actual name
1627 pWord = Ver_ParseGetName( pMan );
1628 if ( pWord == NULL )
1629 return 0;
1630 // check if the name is complemented
1631 assert( pWord[0] != '~' );
1632/*
1633 fCompl = (pWord[0] == '~');
1634 if ( fCompl )
1635 {
1636 fComplUsed = 1;
1637 pWord++;
1638 if ( pNtk->pData == NULL )
1639 pNtk->pData = Extra_MmFlexStart();
1640 }
1641*/
1642 // get the actual net
1643 pNetActual = Ver_ParseFindNet( pNtk, pWord );
1644 if ( pNetActual == NULL )
1645 {
1646 sprintf( pMan->sError, "Actual net %s is missing.", pWord );
1647 Ver_ParsePrintErrorMessage( pMan );
1648 return 0;
1649 }
1650
1651 // close the parenthesis
1652 if ( Ver_StreamPopChar(p) != ')' )
1653 {
1654 sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing parenthesis).", pWord, Mio_GateReadName(pGate) );
1655 Ver_ParsePrintErrorMessage( pMan );
1656 return 0;
1657 }
1658
1659 // add the fanin
1660 if ( Input < nFanins )
1661 {
1662 Vec_IntPush( pMan->vPerm, Input );
1663 Abc_ObjAddFanin( pNode, pNetActual ); // fanin
1664 if ( pNode2 )
1665 Abc_ObjAddFanin( pNode2, pNetActual ); // fanin
1666 }
1667 else if ( Input == nFanins )
1668 Abc_ObjAddFanin( pNetActual, pNode ); // fanout
1669 else if ( Input == nFanins + 1 )
1670 Abc_ObjAddFanin( pNetActual, pNode2 ); // fanout
1671 else
1672 assert( 0 );
1673
1674 // check if it is the end of gate
1675 Ver_ParseSkipComments( pMan );
1676 Symbol = Ver_StreamPopChar(p);
1677 if ( Symbol == ')' )
1678 break;
1679
1680 // skip comma
1681 if ( Symbol != ',' )
1682 {
1683 sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing parenthesis).", pWord, Mio_GateReadName(pGate) );
1684 Ver_ParsePrintErrorMessage( pMan );
1685 return 0;
1686 }
1687 Ver_ParseSkipComments( pMan );
1688 }
1689
1690 // check that the gate as the same number of input
1691 if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
1692 {
1693 sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
1694 Ver_ParsePrintErrorMessage( pMan );
1695 return 0;
1696 }
1697
1698 // check if it is the end of gate
1699 Ver_ParseSkipComments( pMan );
1700 if ( Ver_StreamPopChar(p) != ';' )
1701 {
1702 sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
1703 Ver_ParsePrintErrorMessage( pMan );
1704 return 0;
1705 }
1706
1707 // check if we need to permute the inputs
1708 Vec_IntForEachEntry( pMan->vPerm, Input, i )
1709 if ( Input != i )
1710 break;
1711 if ( i < Vec_IntSize(pMan->vPerm) )
1712 {
1713 // add the fanin numnbers to the end of the permuation array
1714 for ( i = 0; i < nFanins; i++ )
1715 Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
1716 // write the fanin numbers into their corresponding places (according to the gate)
1717 for ( i = 0; i < nFanins; i++ )
1718 Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
1719 }
1720 return 1;
1721}
1722
1734int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
1735{
1736 char Buffer[1000];
1737 Ver_Stream_t * p = pMan->pReader;
1738 Ver_Bundle_t * pBundle;
1739 Vec_Ptr_t * vBundles;
1740 Abc_Obj_t * pNetActual;
1741 Abc_Obj_t * pNode;
1742 char * pWord, Symbol;
1743 int fCompl, fFormalIsGiven;
1744 int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
1745
1746 // gate the name of the box
1747 pWord = Ver_ParseGetName( pMan );
1748 if ( pWord == NULL )
1749 return 0;
1750
1751 // create a box with this name
1752 pNode = Abc_NtkCreateBlackbox( pNtk );
1753 pNode->pData = pNtkBox;
1754 Abc_ObjAssignName( pNode, pWord, NULL );
1755
1756 // continue parsing the box
1757 if ( Ver_StreamPopChar(p) != '(' )
1758 {
1759 sprintf( pMan->sError, "Cannot parse box %s (expected opening parenthesis).", Abc_ObjName(pNode) );
1760 Ver_ParsePrintErrorMessage( pMan );
1761 return 0;
1762 }
1763 Ver_ParseSkipComments( pMan );
1764
1765 // parse pairs of formal/actual inputs
1766 vBundles = Vec_PtrAlloc( 16 );
1767 pNode->pCopy = (Abc_Obj_t *)vBundles;
1768 while ( 1 )
1769 {
1770 // allocate the bundle (formal name + array of actual nets)
1771 pBundle = ABC_ALLOC( Ver_Bundle_t, 1 );
1772 pBundle->pNameFormal = NULL;
1773 pBundle->vNetsActual = Vec_PtrAlloc( 4 );
1774 Vec_PtrPush( vBundles, pBundle );
1775
1776 // process one pair of formal/actual parameters
1777 fFormalIsGiven = 0;
1778 if ( Ver_StreamScanChar(p) == '.' )
1779 {
1780 fFormalIsGiven = 1;
1781 if ( Ver_StreamPopChar(p) != '.' )
1782 {
1783 sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) );
1784 Ver_ParsePrintErrorMessage( pMan );
1785 return 0;
1786 }
1787
1788 // parse the formal name
1789 pWord = Ver_ParseGetName( pMan );
1790 if ( pWord == NULL )
1791 return 0;
1792
1793 // save the name
1794 pBundle->pNameFormal = Extra_UtilStrsav( pWord );
1795
1796 // open the parenthesis
1797 if ( Ver_StreamPopChar(p) != '(' )
1798 {
1799 sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening parenthesis).", pWord, Abc_ObjName(pNode));
1800 Ver_ParsePrintErrorMessage( pMan );
1801 return 0;
1802 }
1803 Ver_ParseSkipComments( pMan );
1804 }
1805
1806 // check if this is the beginning of {} expression
1807 Symbol = Ver_StreamScanChar(p);
1808
1809 // consider the case of vector-inputs
1810 if ( Symbol == '{' )
1811 {
1812 // skip this char
1813 Ver_StreamPopChar(p);
1814
1815 // read actual names
1816 i = 0;
1817 fQuit = 0;
1818 while ( 1 )
1819 {
1820 // parse the formal name
1821 Ver_ParseSkipComments( pMan );
1822 pWord = Ver_ParseGetName( pMan );
1823 if ( pWord == NULL )
1824 return 0;
1825
1826 // check if the last char is a closing brace
1827 if ( pWord[strlen(pWord)-1] == '}' )
1828 {
1829 pWord[strlen(pWord)-1] = 0;
1830 fQuit = 1;
1831 }
1832 if ( pWord[0] == 0 )
1833 break;
1834
1835 // check for constant
1836 if ( pWord[0] >= '1' && pWord[0] <= '9' )
1837 {
1838 if ( !Ver_ParseConstant( pMan, pWord ) )
1839 return 0;
1840 // add constant MSB to LSB
1841 for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
1842 {
1843 // get the actual net
1844 sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
1845 pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1846 if ( pNetActual == NULL )
1847 {
1848 sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
1849 Ver_ParsePrintErrorMessage( pMan );
1850 return 0;
1851 }
1852 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1853 }
1854 }
1855 else
1856 {
1857 // get the suffix of the form [m:n]
1858 if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
1859 Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1860 else
1861 Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1862
1863 // generate signals
1864 if ( nMsb == -1 && nLsb == -1 )
1865 {
1866 // get the actual net
1867 pNetActual = Ver_ParseFindNet( pNtk, pWord );
1868 if ( pNetActual == NULL )
1869 {
1870 if ( !strncmp(pWord, "Open_", 5) ||
1871 !strncmp(pWord, "dct_unconnected", 15) )
1872 pNetActual = Abc_NtkCreateNet( pNtk );
1873 else
1874 {
1875 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1876 Ver_ParsePrintErrorMessage( pMan );
1877 return 0;
1878 }
1879 }
1880 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1881 i++;
1882 }
1883 else
1884 {
1885 // go from MSB to LSB
1886 assert( nMsb >= 0 && nLsb >= 0 );
1887 Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1888 for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
1889 {
1890 // get the actual net
1891 sprintf( Buffer, "%s[%d]", pWord, Bit );
1892 pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1893 if ( pNetActual == NULL )
1894 {
1895 if ( !strncmp(pWord, "Open_", 5) ||
1896 !strncmp(pWord, "dct_unconnected", 15) )
1897 pNetActual = Abc_NtkCreateNet( pNtk );
1898 else
1899 {
1900 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1901 Ver_ParsePrintErrorMessage( pMan );
1902 return 0;
1903 }
1904 }
1905 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1906 }
1907 }
1908 }
1909
1910 if ( fQuit )
1911 break;
1912
1913 // skip comma
1914 Ver_ParseSkipComments( pMan );
1915 Symbol = Ver_StreamPopChar(p);
1916 if ( Symbol == '}' )
1917 break;
1918 if ( Symbol != ',' )
1919 {
1920 sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
1921 Ver_ParsePrintErrorMessage( pMan );
1922 return 0;
1923 }
1924 }
1925 }
1926 else
1927 {
1928 // get the next word
1929 pWord = Ver_ParseGetName( pMan );
1930 if ( pWord == NULL )
1931 return 0;
1932 // consider the case of empty name
1933 fCompl = 0;
1934 if ( pWord[0] == 0 )
1935 {
1936 pNetActual = Abc_NtkCreateNet( pNtk );
1937 Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
1938 }
1939 else
1940 {
1941 // get the actual net
1942 flag=0;
1943 pNetActual = Ver_ParseFindNet( pNtk, pWord );
1944 if ( pNetActual == NULL )
1945 {
1946 Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1947 if ( nMsb == -1 && nLsb == -1 )
1948 {
1949 Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1950 if ( nMsb == -1 && nLsb == -1 )
1951 {
1952 if ( !strncmp(pWord, "Open_", 5) ||
1953 !strncmp(pWord, "dct_unconnected", 15) )
1954 {
1955 pNetActual = Abc_NtkCreateNet( pNtk );
1956 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1957 }
1958 else
1959 {
1960 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1961 Ver_ParsePrintErrorMessage( pMan );
1962 return 0;
1963 }
1964 }
1965 else
1966 {
1967 flag=1;
1968 }
1969 }
1970 else
1971 {
1972 flag=1;
1973 }
1974 if (flag)
1975 {
1976 Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1977 for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
1978 {
1979 // get the actual net
1980 sprintf( Buffer, "%s[%d]", pWord, Bit );
1981 pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1982 if ( pNetActual == NULL )
1983 {
1984 if ( !strncmp(pWord, "Open_", 5) ||
1985 !strncmp(pWord, "dct_unconnected", 15))
1986 pNetActual = Abc_NtkCreateNet( pNtk );
1987 else
1988 {
1989 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1990 Ver_ParsePrintErrorMessage( pMan );
1991 return 0;
1992 }
1993 }
1994 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1995 }
1996 }
1997 }
1998 else
1999 {
2000 Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
2001 }
2002 }
2003 }
2004
2005 if ( fFormalIsGiven )
2006 {
2007 // close the parenthesis
2008 Ver_ParseSkipComments( pMan );
2009 if ( Ver_StreamPopChar(p) != ')' )
2010 {
2011 sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing parenthesis).", pWord, Abc_ObjName(pNode) );
2012 Ver_ParsePrintErrorMessage( pMan );
2013 return 0;
2014 }
2015 Ver_ParseSkipComments( pMan );
2016 }
2017
2018 // check if it is the end of gate
2019 Symbol = Ver_StreamPopChar(p);
2020 if ( Symbol == ')' )
2021 break;
2022 // skip comma
2023 if ( Symbol != ',' )
2024 {
2025 sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) );
2026 Ver_ParsePrintErrorMessage( pMan );
2027 return 0;
2028 }
2029 Ver_ParseSkipComments( pMan );
2030 }
2031
2032 // check if it is the end of gate
2033 Ver_ParseSkipComments( pMan );
2034 if ( Ver_StreamPopChar(p) != ';' )
2035 {
2036 sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) );
2037 Ver_ParsePrintErrorMessage( pMan );
2038 return 0;
2039 }
2040
2041 return 1;
2042}
2043
2055void Ver_ParseFreeBundle( Ver_Bundle_t * pBundle )
2056{
2057 ABC_FREE( pBundle->pNameFormal );
2058 Vec_PtrFree( pBundle->vNetsActual );
2059 ABC_FREE( pBundle );
2060}
2061
2073int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
2074{
2075 Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
2076 Abc_Ntk_t * pNtk = pBox->pNtk;
2077 Abc_Ntk_t * pNtkBox = (Abc_Ntk_t *)pBox->pData;
2078 Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
2079 Ver_Bundle_t * pBundle;
2080 char * pNameFormal;
2081 int i, k, j, iBundle, Length;
2082
2083 assert( !Ver_ObjIsConnected(pBox) );
2084 assert( Ver_NtkIsDefined(pNtkBox) );
2085 assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
2086
2087/*
2088 // clean the PI/PO nets
2089 Abc_NtkForEachPi( pNtkBox, pTerm, i )
2090 Abc_ObjFanout0(pTerm)->pCopy = NULL;
2091 Abc_NtkForEachPo( pNtkBox, pTerm, i )
2092 Abc_ObjFanin0(pTerm)->pCopy = NULL;
2093*/
2094
2095 // check the number of actual nets is the same as the number of formal nets
2096 if ( Vec_PtrSize(vBundles) > Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2097 {
2098 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.",
2099 Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2100 // free the bundling
2101 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2102 Ver_ParseFreeBundle( pBundle );
2103 Vec_PtrFree( vBundles );
2104 pBox->pCopy = NULL;
2105 Ver_ParsePrintErrorMessage( pMan );
2106 return 0;
2107 }
2108
2109 // check if some of them do not have formal names
2110 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2111 if ( pBundle->pNameFormal == NULL )
2112 break;
2113 if ( k < Vec_PtrSize(vBundles) )
2114 {
2115 printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
2116 // add all actual nets in the bundles
2117 iBundle = 0;
2118 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2119 iBundle += Vec_PtrSize(pBundle->vNetsActual);
2120
2121 // check the number of actual nets is the same as the number of formal nets
2122 if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2123 {
2124 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.",
2125 Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2126 // free the bundling
2127 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2128 Ver_ParseFreeBundle( pBundle );
2129 Vec_PtrFree( vBundles );
2130 pBox->pCopy = NULL;
2131 Ver_ParsePrintErrorMessage( pMan );
2132 return 0;
2133 }
2134 // connect bundles in the natural order
2135 iBundle = 0;
2136 Abc_NtkForEachPi( pNtkBox, pTerm, i )
2137 {
2138 pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2139 // the bundle is found - add the connections - using order LSB to MSB
2140 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2141 {
2142 pTermNew = Abc_NtkCreateBi( pNtk );
2143 Abc_ObjAddFanin( pBox, pTermNew );
2144 Abc_ObjAddFanin( pTermNew, pNetAct );
2145 i++;
2146 }
2147 i--;
2148 }
2149 // create fanins of the box
2150 Abc_NtkForEachPo( pNtkBox, pTerm, i )
2151 {
2152 pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2153 // the bundle is found - add the connections - using order LSB to MSB
2154 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2155 {
2156 pTermNew = Abc_NtkCreateBo( pNtk );
2157 Abc_ObjAddFanin( pTermNew, pBox );
2158 Abc_ObjAddFanin( pNetAct, pTermNew );
2159 i++;
2160 }
2161 i--;
2162 }
2163
2164 // free the bundling
2165 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2166 Ver_ParseFreeBundle( pBundle );
2167 Vec_PtrFree( vBundles );
2168 pBox->pCopy = NULL;
2169 return 1;
2170 }
2171
2172 // bundles arrive in any order - but inside each bundle the order is MSB to LSB
2173 // make sure every formal PI has a corresponding net
2174 Abc_NtkForEachPi( pNtkBox, pTerm, i )
2175 {
2176 // get the name of this formal net
2177 pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
2178 // try to find the bundle with this formal net
2179 pBundle = NULL;
2180 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2181 if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2182 break;
2183 assert( pBundle != NULL );
2184 // if the bundle is not found, try without parentheses
2185 if ( k == Vec_PtrSize(vBundles) )
2186 {
2187 pBundle = NULL;
2188 Length = strlen(pNameFormal);
2189 if ( pNameFormal[Length-1] == ']' )
2190 {
2191 // find the opening brace
2192 for ( Length--; Length >= 0; Length-- )
2193 if ( pNameFormal[Length] == '[' )
2194 break;
2195 // compare names before brace
2196 if ( Length > 0 )
2197 {
2198 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2199 if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2200 break;
2201 if ( j == Vec_PtrSize(vBundles) )
2202 pBundle = NULL;
2203 }
2204 }
2205 if ( pBundle == NULL )
2206 {
2207 sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.",
2208 pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2209 Ver_ParsePrintErrorMessage( pMan );
2210 return 0;
2211 }
2212 }
2213 // the bundle is found - add the connections - using order LSB to MSB
2214 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2215 {
2216 pTermNew = Abc_NtkCreateBi( pNtk );
2217 Abc_ObjAddFanin( pBox, pTermNew );
2218 Abc_ObjAddFanin( pTermNew, pNetAct );
2219 i++;
2220 }
2221 i--;
2222 }
2223
2224 // connect those formal POs that do have nets
2225 Abc_NtkForEachPo( pNtkBox, pTerm, i )
2226 {
2227 // get the name of this PI
2228 pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
2229 // try to find this formal net in the bundle
2230 pBundle = NULL;
2231 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2232 if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2233 break;
2234 assert( pBundle != NULL );
2235 // if the name is not found, try without parentheses
2236 if ( k == Vec_PtrSize(vBundles) )
2237 {
2238 pBundle = NULL;
2239 Length = strlen(pNameFormal);
2240 if ( pNameFormal[Length-1] == ']' )
2241 {
2242 // find the opening brace
2243 for ( Length--; Length >= 0; Length-- )
2244 if ( pNameFormal[Length] == '[' )
2245 break;
2246 // compare names before brace
2247 if ( Length > 0 )
2248 {
2249 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2250 if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2251 break;
2252 if ( j == Vec_PtrSize(vBundles) )
2253 pBundle = NULL;
2254 }
2255 }
2256 if ( pBundle == NULL )
2257 {
2258 char Buffer[1000];
2259// printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
2260// pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2261 pTermNew = Abc_NtkCreateBo( pNtk );
2262 sprintf( Buffer, "_temp_net%d", Abc_ObjId(pTermNew) );
2263 pNetAct = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2264 Abc_ObjAddFanin( pTermNew, pBox );
2265 Abc_ObjAddFanin( pNetAct, pTermNew );
2266 continue;
2267 }
2268 }
2269 // the bundle is found - add the connections
2270 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2271 {
2272 if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
2273 {
2274 sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.",
2275 pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
2276 // free the bundling
2277 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2278 Ver_ParseFreeBundle( pBundle );
2279 Vec_PtrFree( vBundles );
2280 pBox->pCopy = NULL;
2281 Ver_ParsePrintErrorMessage( pMan );
2282 return 0;
2283 }
2284 pTermNew = Abc_NtkCreateBo( pNtk );
2285 Abc_ObjAddFanin( pTermNew, pBox );
2286 Abc_ObjAddFanin( pNetAct, pTermNew );
2287 i++;
2288 }
2289 i--;
2290 }
2291
2292 // free the bundling
2293 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2294 Ver_ParseFreeBundle( pBundle );
2295 Vec_PtrFree( vBundles );
2296 pBox->pCopy = NULL;
2297 return 1;
2298}
2299
2300
2312int Ver_ParseConnectDefBoxes( Ver_Man_t * pMan )
2313{
2314 Abc_Ntk_t * pNtk;
2315 Abc_Obj_t * pBox;
2316 int i, k, RetValue = 1;
2317 // go through all the modules
2318 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2319 {
2320 // go through all the boxes of this module
2321 Abc_NtkForEachBox( pNtk, pBox, k )
2322 {
2323 if ( Abc_ObjIsLatch(pBox) )
2324 continue;
2325 // skip internal boxes of the blackboxes
2326 if ( pBox->pData == NULL )
2327 continue;
2328 // if the network is undefined, it will be connected later
2329 if ( !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2330 {
2331 RetValue = 2;
2332 continue;
2333 }
2334 // connect the box
2335 if ( !Ver_ParseConnectBox( pMan, pBox ) )
2336 return 0;
2337 // if the network is a true blackbox, skip
2338 if ( Abc_NtkHasBlackbox((Abc_Ntk_t *)pBox->pData) )
2339 continue;
2340 // convert the box to the whitebox
2341 Abc_ObjBlackboxToWhitebox( pBox );
2342 }
2343 }
2344 return RetValue;
2345}
2346
2358Vec_Ptr_t * Ver_ParseCollectUndefBoxes( Ver_Man_t * pMan )
2359{
2360 Vec_Ptr_t * vUndefs;
2361 Abc_Ntk_t * pNtk, * pNtkBox;
2362 Abc_Obj_t * pBox;
2363 int i, k;
2364 // clear the module structures
2365 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2366 pNtk->pData = NULL;
2367 // go through all the blackboxes
2368 vUndefs = Vec_PtrAlloc( 16 );
2369 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2370 {
2371 Abc_NtkForEachBlackbox( pNtk, pBox, k )
2372 {
2373 pNtkBox = (Abc_Ntk_t *)pBox->pData;
2374 if ( pNtkBox == NULL )
2375 continue;
2376 if ( Ver_NtkIsDefined(pNtkBox) )
2377 continue;
2378 if ( pNtkBox->pData == NULL )
2379 {
2380 // save the box
2381 Vec_PtrPush( vUndefs, pNtkBox );
2382 pNtkBox->pData = Vec_PtrAlloc( 16 );
2383 }
2384 // save the instance
2385 Vec_PtrPush( (Vec_Ptr_t *)pNtkBox->pData, pBox );
2386 }
2387 }
2388 return vUndefs;
2389}
2390
2402void Ver_ParseReportUndefBoxes( Ver_Man_t * pMan )
2403{
2404 Abc_Ntk_t * pNtk;
2405 Abc_Obj_t * pBox;
2406 int i, k, nBoxes;
2407 // clean
2408 nBoxes = 0;
2409 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2410 {
2411 pNtk->fHiePath = 0;
2412 if ( !Ver_NtkIsDefined(pNtk) )
2413 nBoxes++;
2414 }
2415 // count
2416 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2417 Abc_NtkForEachBlackbox( pNtk, pBox, k )
2418 if ( pBox->pData && !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2419 ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
2420 // print the stats
2421 printf( "Warning: The design contains %d undefined object types interpreted as blackboxes:\n", nBoxes );
2422 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2423 if ( !Ver_NtkIsDefined(pNtk) )
2424 printf( "%s (%d) ", Abc_NtkName(pNtk), pNtk->fHiePath );
2425 printf( "\n" );
2426 // clean
2427 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2428 pNtk->fHiePath = 0;
2429}
2430
2442int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
2443{
2444 Abc_Ntk_t * pNtk;
2445 Ver_Bundle_t * pBundle;
2446 Abc_Obj_t * pBox, * pNet;
2447 int i, k, j, m;
2448 // go through undef box types
2449 Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2450 // go through instances of this type
2451 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2452 // go through the bundles of this instance
2453 Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2454 // go through the actual nets of this bundle
2455 if ( pBundle )
2456 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2457 {
2458 if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
2459 if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
2460 return 1;
2461 }
2462 return 0;
2463}
2464
2476int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
2477{
2478 Ver_Bundle_t * pBundle = NULL;
2479 Abc_Obj_t * pBox, * pNet;
2480 int k, j, m;
2481 // go through instances of this type
2482 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2483 {
2484 // find a bundle with the given name in this instance
2485 Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2486 if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
2487 break;
2488 // skip non-driven bundles
2489 if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2490 continue;
2491 // check if all nets are driven in this bundle
2492 assert(pBundle); // Verify that pBundle was assigned to.
2493 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2494 if ( Abc_ObjFaninNum(pNet) > 0 )
2495 return 1;
2496 }
2497 return 0;
2498}
2499
2511Ver_Bundle_t * Ver_ParseGetNondrivenBundle( Abc_Ntk_t * pNtk, int Counter )
2512{
2513 Ver_Bundle_t * pBundle;
2514 Abc_Obj_t * pBox, * pNet;
2515 int k, m;
2516 // go through instances of this type
2517 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2518 {
2519 if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2520 continue;
2521 // get the bundle given distance away
2522 pBundle = (Ver_Bundle_t *)Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
2523 if ( pBundle == NULL )
2524 continue;
2525 // go through the actual nets of this bundle
2526 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2527 if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
2528 return pBundle;
2529 }
2530 return NULL;
2531}
2532
2544int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 )
2545{
2546 char Buffer[200];
2547 char * pName;
2548 Ver_Bundle_t * pBundle = NULL;
2549 Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
2550 int k, j, m;
2551
2552 // drive this net in the undef box
2553 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle0->vNetsActual, pNetAct, m )
2554 {
2555 // create the formal net
2556 if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
2557 sprintf( Buffer, "%s", pBundle0->pNameFormal );
2558 else
2559 sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
2560 assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2561 pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2562 // connect it to the box
2563 pTerm = Abc_NtkCreateBo( pNtk );
2564 assert( Abc_NtkBoxNum(pNtk) <= 1 );
2565 pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2566 Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
2567 Abc_ObjAddFanin( pNetFormal, pTerm );
2568 Abc_ObjAddFanin( pTerm, pBox );
2569 }
2570
2571 // go through instances of this type
2572 pName = Extra_UtilStrsav(pBundle0->pNameFormal);
2573 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2574 {
2575 // find a bundle with the given name in this instance
2576 Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2577 if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
2578 break;
2579 // skip non-driven bundles
2580 if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2581 continue;
2582 // check if any nets are driven in this bundle
2583 assert(pBundle); // Verify pBundle was assigned to.
2584 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2585 if ( Abc_ObjFaninNum(pNetAct) > 0 )
2586 {
2587 sprintf( pMan->sError, "Missing specification of the I/Os of undefined box \"%s\".", Abc_NtkName(pNtk) );
2588 Ver_ParsePrintErrorMessage( pMan );
2589 return 0;
2590 }
2591 // drive the nets by the undef box
2592 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2593 {
2594 pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
2595 Abc_ObjAddFanin( pTermNew, pBox );
2596 Abc_ObjAddFanin( pNetAct, pTermNew );
2597 }
2598 // remove the bundle
2599 Ver_ParseFreeBundle( pBundle ); pBundle = NULL;
2600 Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2601 }
2602 ABC_FREE( pName );
2603 return 1;
2604}
2605
2606
2618int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
2619{
2620 char Buffer[200];
2621 Ver_Bundle_t * pBundle;
2622 Abc_Ntk_t * pNtk;
2623 Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
2624 int i, k, j, m, CountCur, CountTotal = -1;
2625 // iterate through the undef boxes
2626 Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2627 {
2628 // count the number of unconnected bundles for instances of this type of box
2629 CountTotal = -1;
2630 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2631 {
2632 CountCur = 0;
2633 Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2634 CountCur += (pBundle != NULL);
2635 if ( CountTotal == -1 )
2636 CountTotal = CountCur;
2637 else if ( CountTotal != CountCur )
2638 {
2639 sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.",
2640 CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
2641 Ver_ParsePrintErrorMessage( pMan );
2642 return 0;
2643 }
2644 }
2645
2646 // create formals
2647 pBox = (Abc_Obj_t *)Vec_PtrEntry( (Vec_Ptr_t *)pNtk->pData, 0 );
2648 Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2649 {
2650 if ( pBundle == NULL )
2651 continue;
2652 Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2653 {
2654 // find create the formal net
2655 if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
2656 sprintf( Buffer, "%s", pBundle->pNameFormal );
2657 else
2658 sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
2659 assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2660 pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2661 // connect
2662 pTerm = Abc_NtkCreateBi( pNtk );
2663 assert( Abc_NtkBoxNum(pNtk) <= 1 );
2664 pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2665 Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
2666 Abc_ObjAddFanin( pTerm, pNetFormal );
2667 Abc_ObjAddFanin( pBox2, pTerm );
2668 }
2669 }
2670
2671 // go through all the boxes
2672 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2673 {
2674 // go through all the bundles
2675 Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2676 {
2677 if ( pBundle == NULL )
2678 continue;
2679 // drive the nets by the undef box
2680 Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2681 {
2682 pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
2683 Abc_ObjAddFanin( pBox, pTermNew );
2684 Abc_ObjAddFanin( pTermNew, pNetAct );
2685 }
2686 // remove the bundle
2687 Ver_ParseFreeBundle( pBundle );
2688 Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2689 }
2690
2691 // free the bundles
2692 Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
2693 pBox->pCopy = NULL;
2694 }
2695 }
2696 return 1;
2697}
2698
2699
2711int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs )
2712{
2713 Abc_Ntk_t * pNtk;
2714 Abc_Obj_t * pBox;
2715 int i, k, nMaxSize = 0;
2716 // go through undef box types
2717 Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2718 // go through instances of this type
2719 Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2720 // check the number of bundles of this instance
2721 if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2722 nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
2723 return nMaxSize;
2724}
2725
2737void Ver_ParsePrintLog( Ver_Man_t * pMan )
2738{
2739 Abc_Ntk_t * pNtk, * pNtkBox;
2740 Abc_Obj_t * pBox;
2741 FILE * pFile;
2742 char * pNameGeneric;
2743 char Buffer[1000];
2744 int i, k, Count1 = 0;
2745
2746 // open the log file
2747 pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
2748 sprintf( Buffer, "%s.log", pNameGeneric );
2749 ABC_FREE( pNameGeneric );
2750 pFile = fopen( Buffer, "w" );
2751
2752 // count the total number of instances and how many times they occur
2753 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2754 pNtk->fHieVisited = 0;
2755 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2756 Abc_NtkForEachBox( pNtk, pBox, k )
2757 {
2758 if ( Abc_ObjIsLatch(pBox) )
2759 continue;
2760 pNtkBox = (Abc_Ntk_t *)pBox->pData;
2761 if ( pNtkBox == NULL )
2762 continue;
2763 pNtkBox->fHieVisited++;
2764 }
2765 // print each box and its stats
2766 fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
2767 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2768 {
2769 fprintf( pFile, "%-50s : ", Abc_NtkName(pNtk) );
2770 if ( !Ver_NtkIsDefined(pNtk) )
2771 fprintf( pFile, "undefbox" );
2772 else if ( Abc_NtkHasBlackbox(pNtk) )
2773 fprintf( pFile, "blackbox" );
2774 else
2775 fprintf( pFile, "logicbox" );
2776 fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
2777// fprintf( pFile, "\n " );
2778 fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
2779 fprintf( pFile, " po = %4d", Abc_NtkPoNum(pNtk) );
2780 fprintf( pFile, " nd = %8d", Abc_NtkNodeNum(pNtk) );
2781 fprintf( pFile, " lat = %6d", Abc_NtkLatchNum(pNtk) );
2782 fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
2783 fprintf( pFile, "\n" );
2784 Count1 += (Abc_NtkPoNum(pNtk) == 1);
2785 }
2786 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2787 pNtk->fHieVisited = 0;
2788 fprintf( pFile, "The number of modules with one output = %d (%.2f %%).\n", Count1, 100.0 * Count1/Vec_PtrSize(pMan->pDesign->vModules) );
2789
2790 // report instances with dangling outputs
2791 if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2792 {
2793 Vec_Ptr_t * vBundles;
2794 Ver_Bundle_t * pBundle;
2795 int j, nActNets, Counter = 0;
2796 // count the number of instances with dangling outputs
2797 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2798 {
2799 Abc_NtkForEachBox( pNtk, pBox, k )
2800 {
2801 if ( Abc_ObjIsLatch(pBox) )
2802 continue;
2803 vBundles = (Vec_Ptr_t *)pBox->pCopy;
2804 pNtkBox = (Abc_Ntk_t *)pBox->pData;
2805 if ( pNtkBox == NULL )
2806 continue;
2807 if ( !Ver_NtkIsDefined(pNtkBox) )
2808 continue;
2809 // count the number of actual nets
2810 nActNets = 0;
2811 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2812 nActNets += Vec_PtrSize(pBundle->vNetsActual);
2813 // the box is defined and will be connected
2814 if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2815 Counter++;
2816 }
2817 }
2818 if ( Counter == 0 )
2819 fprintf( pFile, "The outputs of all box instances are connected.\n" );
2820 else
2821 {
2822 fprintf( pFile, "\n" );
2823 fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
2824 // enumerate through the boxes
2825 Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2826 {
2827 Abc_NtkForEachBox( pNtk, pBox, k )
2828 {
2829 if ( Abc_ObjIsLatch(pBox) )
2830 continue;
2831 vBundles = (Vec_Ptr_t *)pBox->pCopy;
2832 pNtkBox = (Abc_Ntk_t *)pBox->pData;
2833 if ( pNtkBox == NULL )
2834 continue;
2835 if ( !Ver_NtkIsDefined(pNtkBox) )
2836 continue;
2837 // count the number of actual nets
2838 nActNets = 0;
2839 Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2840 nActNets += Vec_PtrSize(pBundle->vNetsActual);
2841 // the box is defined and will be connected
2842 if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2843 fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
2844 Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
2845 }
2846 }
2847 }
2848 }
2849 fclose( pFile );
2850 printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
2851}
2852
2853
2872int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
2873{
2874 int fPrintLog = 0;
2875 Abc_Ntk_t * pNtk = NULL;
2876 Ver_Bundle_t * pBundle;
2877 Vec_Ptr_t * vUndefs;
2878 int i, RetValue, Counter, nMaxBoxSize;
2879
2880 // print the log file
2881 if ( fPrintLog && pMan->pDesign->vModules && Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2882 Ver_ParsePrintLog( pMan );
2883
2884 // connect defined boxes
2885 RetValue = Ver_ParseConnectDefBoxes( pMan );
2886 if ( RetValue < 2 )
2887 return RetValue;
2888
2889 // report the boxes
2890 Ver_ParseReportUndefBoxes( pMan );
2891
2892 // collect undef box types and their actual instances
2893 vUndefs = Ver_ParseCollectUndefBoxes( pMan );
2894 assert( Vec_PtrSize( vUndefs ) > 0 );
2895
2896 // go through all undef box types
2897 Counter = 0;
2898 nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
2899 while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
2900 {
2901 // go through undef box types
2902 pBundle = NULL;
2903 Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2904 if ( (pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter )) )
2905 break;
2906 if ( pBundle == NULL )
2907 {
2908 Counter++;
2909 continue;
2910 }
2911 // drive this bundle by this box
2912 if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
2913 return 0;
2914 }
2915
2916 // make all the remaining bundles the drivers of undefs
2917 if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
2918 return 0;
2919
2920 // cleanup
2921 Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2922 {
2923 Vec_PtrFree( (Vec_Ptr_t *)pNtk->pData );
2924 pNtk->pData = NULL;
2925 }
2926 Vec_PtrFree( vUndefs );
2927 return 1;
2928}
2929
2930
2942Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
2943{
2944 Abc_Obj_t * pNet, * pTerm;
2945 // get the PI net
2946// pNet = Ver_ParseFindNet( pNtk, pName );
2947// if ( pNet )
2948// printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
2949 pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2950 // add the PI node
2951 pTerm = Abc_NtkCreatePi( pNtk );
2952 Abc_ObjAddFanin( pNet, pTerm );
2953 return pTerm;
2954}
2955
2967Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
2968{
2969 Abc_Obj_t * pNet, * pTerm;
2970 // get the PO net
2971// pNet = Ver_ParseFindNet( pNtk, pName );
2972// if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
2973// printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
2974 pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2975 // add the PO node
2976 pTerm = Abc_NtkCreatePo( pNtk );
2977 Abc_ObjAddFanin( pTerm, pNet );
2978 return pTerm;
2979}
2980
2992Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO )
2993{
2994 Abc_Obj_t * pLatch, * pTerm;
2995 // add the BO terminal
2996 pTerm = Abc_NtkCreateBi( pNtk );
2997 Abc_ObjAddFanin( pTerm, pNetLI );
2998 // add the latch box
2999 pLatch = Abc_NtkCreateLatch( pNtk );
3000 Abc_ObjAddFanin( pLatch, pTerm );
3001 // add the BI terminal
3002 pTerm = Abc_NtkCreateBo( pNtk );
3003 Abc_ObjAddFanin( pTerm, pLatch );
3004 // get the LO net
3005 Abc_ObjAddFanin( pNetLO, pTerm );
3006 // set latch name
3007 Abc_ObjAssignName( pLatch, Abc_ObjName(pNetLO), "L" );
3008 Abc_LatchSetInitDc( pLatch );
3009 return pLatch;
3010}
3011
3023Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
3024{
3025 Abc_Obj_t * pObj;
3026 pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
3027 pNet = Abc_NtkCreateNet( pNtk );
3028 Abc_ObjAddFanin( pNet, pObj );
3029 return pNet;
3030}
3031
3032
3036
3037
3038ABC_NAMESPACE_IMPL_END
3039
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition abcObj.c:587
Abc_NtkAlloc
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition abcNtk.c:53
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition abc.h:520
Abc_NtkCheckRead
ABC_DLL int Abc_NtkCheckRead(Abc_Ntk_t *pNtk)
Definition abcCheck.c:80
Abc_NtkCreateNodeBuf
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeBuf(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition abcObj.c:706
Abc_DesFree
ABC_DLL void Abc_DesFree(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition abcLib.c:94
Abc_NtkForEachBlackbox
#define Abc_NtkForEachBlackbox(pNtk, pObj, i)
Definition abc.h:512
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition abcNames.c:69
Abc_NtkFinalizeRead
ABC_DLL void Abc_NtkFinalizeRead(Abc_Ntk_t *pNtk)
Definition abcNtk.c:413
ABC_NTK_NETLIST
@ ABC_NTK_NETLIST
Definition abc.h:56
Abc_DesCreate
ABC_DLL Abc_Des_t * Abc_DesCreate(char *pName)
DECLARATIONS ///.
Definition abcLib.c:45
Abc_Des_t
struct Abc_Des_t_ Abc_Des_t
BASIC TYPES ///.
Definition abc.h:114
Abc_DesFindModelByName
ABC_DLL Abc_Ntk_t * Abc_DesFindModelByName(Abc_Des_t *p, char *pName)
Definition abcLib.c:249
Abc_NtkCreateNodeInv
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition abcObj.c:674
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
Abc_DesAddModel
ABC_DLL int Abc_DesAddModel(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition abcLib.c:226
ABC_FUNC_BLACKBOX
@ ABC_FUNC_BLACKBOX
Definition abc.h:70
ABC_FUNC_AIG
@ ABC_FUNC_AIG
Definition abc.h:67
ABC_FUNC_MAP
@ ABC_FUNC_MAP
Definition abc.h:68
Abc_NtkForEachBox
#define Abc_NtkForEachBox(pNtk, pObj, i)
Definition abc.h:498
Abc_NtkFindNet
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition abcObj.c:515
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameReadLibGen
ABC_DLL void * Abc_FrameReadLibGen()
Definition mainFrame.c:59
GateType
GateType
Definition csat_apis.h:50
p
Cube * p
Definition exorList.c:222
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition extraUtilUtil.c:179
Extra_FileNameGeneric
char * Extra_FileNameGeneric(char *FileName)
Definition extraUtilFile.c:172
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Hop_CreateOr
Hop_Obj_t * Hop_CreateOr(Hop_Man_t *p, int nVars)
Definition hopOper.c:341
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_CreateAnd
Hop_Obj_t * Hop_CreateAnd(Hop_Man_t *p, int nVars)
Definition hopOper.c:320
Hop_CreateExor
Hop_Obj_t * Hop_CreateExor(Hop_Man_t *p, int nVars)
Definition hopOper.c:362
Hop_ManStop
void Hop_ManStop(Hop_Man_t *p)
Definition hopMan.c:84
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
glo_fMapped
int glo_fMapped
Definition verCore.c:80
Mio_GateReadPins
Mio_Pin_t * Mio_GateReadPins(Mio_Gate_t *pGate)
Definition mioApi.c:173
Mio_LibraryReadConst0
Mio_Gate_t * Mio_LibraryReadConst0(Mio_Library_t *pLib)
Definition mioApi.c:51
Mio_GateReadPinNum
int Mio_GateReadPinNum(Mio_Gate_t *pGate)
Definition mioApi.c:177
Mio_Library_t
struct Mio_LibraryStruct_t_ Mio_Library_t
Definition mio.h:42
Mio_GateReadTwin
Mio_Gate_t * Mio_GateReadTwin(Mio_Gate_t *pGate)
Definition mioApi.c:176
Mio_LibraryReadGateByName
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition mioApi.c:105
Mio_PinReadName
char * Mio_PinReadName(Mio_Pin_t *pPin)
Definition mioApi.c:208
Mio_GateReadName
char * Mio_GateReadName(Mio_Gate_t *pGate)
Definition mioApi.c:169
Mio_PinReadNext
Mio_Pin_t * Mio_PinReadNext(Mio_Pin_t *pPin)
Definition mioApi.c:217
Mio_LibraryReadConst1
Mio_Gate_t * Mio_LibraryReadConst1(Mio_Library_t *pLib)
Definition mioApi.c:52
Mio_Pin_t
struct Mio_PinStruct_t_ Mio_Pin_t
Definition mio.h:44
Mio_GateReadOutName
char * Mio_GateReadOutName(Mio_Gate_t *pGate)
Definition mioApi.c:170
Mio_Gate_t
struct Mio_GateStruct_t_ Mio_Gate_t
Definition mio.h:43
Mio_LibraryReadBuf
Mio_Gate_t * Mio_LibraryReadBuf(Mio_Library_t *pLib)
Definition mioApi.c:49
st__strhash
int st__strhash(const char *string, int modulus)
Definition st.c:449
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition st.c:114
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition st.c:72
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition st.c:171
st__free_table
void st__free_table(st__table *table)
Definition st.c:81
st__is_member
#define st__is_member(table, key)
Definition st.h:70
st__foreach_item
#define st__foreach_item(table, gen, key, value)
Definition st.h:107
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::fHieVisited
int fHieVisited
Definition abc.h:182
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Ntk_t_::pData
void * pData
Definition abc.h:203
Abc_Ntk_t_::pSpec
char * pSpec
Definition abc.h:159
Abc_Ntk_t_::fHiePath
int fHiePath
Definition abc.h:183
Abc_Ntk_t_::ntkFunc
Abc_NtkFunc_t ntkFunc
Definition abc.h:157
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::vFanins
Vec_Int_t vFanins
Definition abc.h:143
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
Ver_Bundle_t_
Definition verCore.c:84
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition verCore.c:86
Ver_Bundle_t_::pNameFormal
char * pNameFormal
Definition verCore.c:85
st__generator
Definition st.h:64
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
memset
char * memset()
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strcpy
char * strcpy()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Ver_ParseInsertsSuffix
int Ver_ParseInsertsSuffix(Ver_Man_t *pMan, char *pWord, int nMsb, int nLsb)
Definition verCore.c:587
Ver_ParseCollectUndefBoxes
Vec_Ptr_t * Ver_ParseCollectUndefBoxes(Ver_Man_t *pMan)
Definition verCore.c:2358
Ver_ParseMaxBoxSize
int Ver_ParseMaxBoxSize(Vec_Ptr_t *vUndefs)
Definition verCore.c:2711
Ver_Bundle_t
struct Ver_Bundle_t_ Ver_Bundle_t
Definition verCore.c:82
Ver_ParseConstant
int Ver_ParseConstant(Ver_Man_t *pMan, char *pWord)
Definition verCore.c:753
Ver_ParseLookupSuffix
int Ver_ParseLookupSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition verCore.c:563
Ver_ParseFormalNetsAreDriven
int Ver_ParseFormalNetsAreDriven(Abc_Ntk_t *pNtk, char *pNameFormal)
Definition verCore.c:2476
Ver_ParseDriveInputs
int Ver_ParseDriveInputs(Ver_Man_t *pMan, Vec_Ptr_t *vUndefs)
Definition verCore.c:2618
Ver_SignalType_t
Ver_SignalType_t
DECLARATIONS ///.
Definition verCore.c:33
VER_SIG_WIRE
@ VER_SIG_WIRE
Definition verCore.c:39
VER_SIG_OUTPUT
@ VER_SIG_OUTPUT
Definition verCore.c:36
VER_SIG_INOUT
@ VER_SIG_INOUT
Definition verCore.c:37
VER_SIG_REG
@ VER_SIG_REG
Definition verCore.c:38
VER_SIG_NONE
@ VER_SIG_NONE
Definition verCore.c:34
VER_SIG_INPUT
@ VER_SIG_INPUT
Definition verCore.c:35
Ver_ParseCheckNondrivenNets
int Ver_ParseCheckNondrivenNets(Vec_Ptr_t *vUndefs)
Definition verCore.c:2442
Ver_ParseConnectDefBoxes
int Ver_ParseConnectDefBoxes(Ver_Man_t *pMan)
Definition verCore.c:2312
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition verCore.c:328
Ver_ParseFile
Abc_Des_t * Ver_ParseFile(char *pFileName, Abc_Des_t *pGateLib, int fCheck, int fUseMemMan)
MACRO DEFINITIONS ///.
Definition verCore.c:165
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition verCore.c:278
Ver_ParseSignalPrefix
int Ver_ParseSignalPrefix(Ver_Man_t *pMan, char **ppWord, int *pnMsb, int *pnLsb)
Definition verCore.c:635
Ver_ParseReportUndefBoxes
void Ver_ParseReportUndefBoxes(Ver_Man_t *pMan)
Definition verCore.c:2402
Ver_GateType_t
Ver_GateType_t
Definition verCore.c:43
VER_GATE_BUF
@ VER_GATE_BUF
Definition verCore.c:47
VER_GATE_OR
@ VER_GATE_OR
Definition verCore.c:45
VER_GATE_NAND
@ VER_GATE_NAND
Definition verCore.c:48
VER_GATE_NOT
@ VER_GATE_NOT
Definition verCore.c:51
VER_GATE_AND
@ VER_GATE_AND
Definition verCore.c:44
VER_GATE_NOR
@ VER_GATE_NOR
Definition verCore.c:49
VER_GATE_XNOR
@ VER_GATE_XNOR
Definition verCore.c:50
VER_GATE_XOR
@ VER_GATE_XOR
Definition verCore.c:46
Ver_ParseDriveFormal
int Ver_ParseDriveFormal(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_Bundle_t *pBundle0)
Definition verCore.c:2544
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition verCore.c:351
Ver_ParseFreeBundle
void Ver_ParseFreeBundle(Ver_Bundle_t *pBundle)
Definition verCore.c:2055
Ver_FindGateInput
int Ver_FindGateInput(Mio_Gate_t *pGate, char *pName)
Definition verCore.c:1527
Ver_ParsePrintLog
void Ver_ParsePrintLog(Ver_Man_t *pMan)
Definition verCore.c:2737
Ver_ParseFindOrCreateNetwork
Abc_Ntk_t * Ver_ParseFindOrCreateNetwork(Ver_Man_t *pMan, char *pName)
Definition verCore.c:301
Ver_ParseGetNondrivenBundle
Ver_Bundle_t * Ver_ParseGetNondrivenBundle(Abc_Ntk_t *pNtk, int Counter)
Definition verCore.c:2511
Ver_ParseSignalSuffix
int Ver_ParseSignalSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition verCore.c:699
Ver_StreamMove
void Ver_StreamMove(Ver_Stream_t *p)
Definition verStream.c:455
Ver_StreamGetCurPosition
int Ver_StreamGetCurPosition(Ver_Stream_t *p)
Definition verStream.c:208
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition verParse.c:45
Ver_Stream_t
struct Ver_Stream_t_ Ver_Stream_t
Definition ver.h:46
Ver_StreamGetWord
char * Ver_StreamGetWord(Ver_Stream_t *p, char *pCharsToStop)
Definition verStream.c:397
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition verStream.c:275
Ver_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ver_Man_t_ Ver_Man_t
INCLUDES ///.
Definition ver.h:45
Ver_StreamAlloc
Ver_Stream_t * Ver_StreamAlloc(char *pFileName)
FUNCTION DEFINITIONS ///.
Definition verStream.c:74
Ver_StreamSkipToChars
void Ver_StreamSkipToChars(Ver_Stream_t *p, char *pCharsToStop)
Definition verStream.c:349
Ver_StreamScanChar
char Ver_StreamScanChar(Ver_Stream_t *p)
Definition verStream.c:258
Ver_FormulaParser
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
Ver_StreamFree
void Ver_StreamFree(Ver_Stream_t *p)
Definition verStream.c:157
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition verParse.c:91
Ver_StreamGetLineNumber
int Ver_StreamGetLineNumber(Ver_Stream_t *p)
Definition verStream.c:224
Ver_FormulaReduction
void * Ver_FormulaReduction(char *pFormula, void *pMan, Vec_Ptr_t *vNames, char *pErrorMessage)
Definition verFormula.c:435
Ver_StreamGetFileSize
int Ver_StreamGetFileSize(Ver_Stream_t *p)
Definition verStream.c:192