ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ioReadBlifMv.c
Go to the documentation of this file.
1
20
21#include "misc/zlib/zlib.h"
22#include "misc/bzlib/bzlib.h"
23#include "base/abc/abc.h"
24#include "misc/vec/vecPtr.h"
25#include "ioAbc.h"
26
28
32
33#define IO_BLIFMV_MAXVALUES 256
34//#define IO_VERBOSE_OUTPUT
35
36typedef struct Io_MvVar_t_ Io_MvVar_t; // parsing var
37typedef struct Io_MvMod_t_ Io_MvMod_t; // parsing model
38typedef struct Io_MvMan_t_ Io_MvMan_t; // parsing manager
39
41
43{
44 int nValues; // the number of values
45 char ** pNames; // the value names
46};
47
49{
50 // file lines
51 char * pName; // .model line
52 Vec_Ptr_t * vInputs; // .inputs lines
53 Vec_Ptr_t * vOutputs; // .outputs lines
54 Vec_Ptr_t * vLatches; // .latch lines
55 Vec_Ptr_t * vFlops; // .flop lines
56 Vec_Ptr_t * vResets; // .reset lines
57 Vec_Ptr_t * vNames; // .names lines
58 Vec_Ptr_t * vSubckts; // .subckt lines
59 Vec_Ptr_t * vShorts; // .short lines
60 Vec_Ptr_t * vOnehots; // .onehot lines
61 Vec_Ptr_t * vMvs; // .mv lines
62 Vec_Ptr_t * vConstrs; // .constraint lines
64 int fBlackBox; // indicates blackbox model
65 // the resulting network
68 // the parent manager
70};
71
73{
74 // general info about file
75 int fBlifMv; // the file is BLIF-MV
76 int fUseReset; // the reset circuitry is added
77 char * pFileName; // the name of the file
78 char * pBuffer; // the contents of the file
79 Vec_Ptr_t * vLines; // the line beginnings
80 // the results of reading
81 Abc_Des_t * pDesign; // the design under construction
82 int nNDnodes; // the counter of ND nodes
83 // intermediate storage for models
84 Vec_Ptr_t * vModels; // vector of models
85 Io_MvMod_t * pLatest; // the current model
86 // current processing info
87 Vec_Ptr_t * vTokens; // the current tokens
88 Vec_Ptr_t * vTokens2; // the current tokens
89 Vec_Str_t * vFunc; // the local function
90 // error reporting
91 char sError[512]; // the error string generated during parsing
92 // statistics
93 int nTablesRead; // the number of processed tables
94 int nTablesLeft; // the number of dangling tables
95};
96
97// static functions
98static Io_MvMan_t * Io_MvAlloc();
99static void Io_MvFree( Io_MvMan_t * p );
100static Io_MvMod_t * Io_MvModAlloc();
101static void Io_MvModFree( Io_MvMod_t * p );
102static char * Io_MvLoadFile( char * pFileName );
103static void Io_MvReadPreparse( Io_MvMan_t * p );
104static int Io_MvReadInterfaces( Io_MvMan_t * p );
105static Abc_Des_t * Io_MvParse( Io_MvMan_t * p );
106static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
107static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
108static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
109static int Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine );
110static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine );
111static int Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine );
112static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
113static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine );
114static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
115static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
116static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
117static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine );
118static int Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine );
119static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
120static Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar );
121
122static int Io_MvCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; }
123static int Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!'; }
124
125extern void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
126
130
142Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
143{
144 FILE * pFile;
145 Io_MvMan_t * p;
146 Abc_Ntk_t * pNtk, * pExdc;
147 Abc_Des_t * pDesign = NULL;
148 char * pDesignName;
149 int RetValue, i;
150 char * pLtlProp;
151
152 // check that the file is available
153 pFile = fopen( pFileName, "rb" );
154 if ( pFile == NULL )
155 {
156 printf( "Io_ReadBlifMv(): The file is unavailable (absent or open).\n" );
157 return 0;
158 }
159 fclose( pFile );
160
161 // start the file reader
162 p = Io_MvAlloc();
163 p->fBlifMv = fBlifMv;
164 p->fUseReset = 1;
165 p->pFileName = pFileName;
166 p->pBuffer = Io_MvLoadFile( pFileName );
167 if ( p->pBuffer == NULL )
168 {
169 Io_MvFree( p );
170 return NULL;
171 }
172 // set the design name
173 pDesignName = Extra_FileNameGeneric( pFileName );
174 p->pDesign = Abc_DesCreate( pDesignName );
175 ABC_FREE( pDesignName );
176 // free the HOP manager
177 Hop_ManStop( (Hop_Man_t *)p->pDesign->pManFunc );
178 p->pDesign->pManFunc = NULL;
179 // prepare the file for parsing
180 Io_MvReadPreparse( p );
181 // parse interfaces of each network and construct the network
182 if ( Io_MvReadInterfaces( p ) )
183 pDesign = Io_MvParse( p );
184 if ( p->sError[0] )
185 fprintf( stdout, "%s\n", p->sError );
186 Io_MvFree( p );
187 if ( pDesign == NULL )
188 return NULL;
189// pDesign should be linked to all models of the design
190
191 // make sure that everything is okay with the network structure
192 if ( fCheck )
193 {
194 Vec_PtrForEachEntry( Abc_Ntk_t *, pDesign->vModules, pNtk, i )
195 {
196 if ( !Abc_NtkCheckRead( pNtk ) )
197 {
198 printf( "Io_ReadBlifMv: The network check has failed for model %s.\n", pNtk->pName );
199 Abc_DesFree( pDesign, NULL );
200 return NULL;
201 }
202 }
203 }
204
205//Abc_DesPrint( pDesign );
206
207 // check if there is an EXDC network
208 if ( Vec_PtrSize(pDesign->vModules) > 1 )
209 {
210 pNtk = (Abc_Ntk_t *)Vec_PtrEntry(pDesign->vModules, 0);
211 Vec_PtrForEachEntryStart( Abc_Ntk_t *, pDesign->vModules, pExdc, i, 1 )
212 if ( !strcmp(pExdc->pName, "EXDC") )
213 {
214 assert( pNtk->pExdc == NULL );
215 pNtk->pExdc = pExdc;
216 Vec_PtrRemove(pDesign->vModules, pExdc);
217 pExdc->pDesign = NULL;
218 i--;
219 }
220 else
221 pNtk = pExdc;
222 }
223
224 // detect top-level model
225 RetValue = Abc_DesFindTopLevelModels( pDesign );
226 pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
227 if ( RetValue > 1 )
228 printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
229 Vec_PtrSize(pDesign->vTops), pNtk->pName );
230
231 // extract the master network
232 pNtk->pDesign = pDesign;
233 pDesign->pManFunc = NULL;
234
235 // verify the design for cyclic dependence
236 assert( Vec_PtrSize(pDesign->vModules) > 0 );
237 if ( Vec_PtrSize(pDesign->vModules) == 1 )
238 {
239// printf( "Warning: The design is not hierarchical.\n" );
240 Abc_DesFree( pDesign, pNtk );
241 pNtk->pDesign = NULL;
242 pNtk->pSpec = Extra_UtilStrsav( pFileName );
243 }
244 else
246
247//Io_WriteBlifMv( pNtk, "_temp_.mv" );
248 if ( pNtk->pSpec == NULL )
249 pNtk->pSpec = Extra_UtilStrsav( pFileName );
250
251 vGlobalLtlArray = Vec_PtrAlloc( 100 );
252 Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
253 Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
254 Vec_PtrFreeP( &vGlobalLtlArray );
255 return pNtk;
256}
257
269static Io_MvMan_t * Io_MvAlloc()
270{
271 Io_MvMan_t * p;
272 p = ABC_ALLOC( Io_MvMan_t, 1 );
273 memset( p, 0, sizeof(Io_MvMan_t) );
274 p->vLines = Vec_PtrAlloc( 512 );
275 p->vModels = Vec_PtrAlloc( 512 );
276 p->vTokens = Vec_PtrAlloc( 512 );
277 p->vTokens2 = Vec_PtrAlloc( 512 );
278 p->vFunc = Vec_StrAlloc( 512 );
279 return p;
280}
281
293static void Io_MvFree( Io_MvMan_t * p )
294{
295 Io_MvMod_t * pMod;
296 int i;
297 if ( p->pDesign )
298 Abc_DesFree( p->pDesign, NULL );
299 if ( p->pBuffer )
300 ABC_FREE( p->pBuffer );
301 if ( p->vLines )
302 Vec_PtrFree( p->vLines );
303 if ( p->vModels )
304 {
305 Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
306 Io_MvModFree( pMod );
307 Vec_PtrFree( p->vModels );
308 }
309 Vec_PtrFree( p->vTokens );
310 Vec_PtrFree( p->vTokens2 );
311 Vec_StrFree( p->vFunc );
312 ABC_FREE( p );
313}
314
326static Io_MvMod_t * Io_MvModAlloc()
327{
328 Io_MvMod_t * p;
329 p = ABC_ALLOC( Io_MvMod_t, 1 );
330 memset( p, 0, sizeof(Io_MvMod_t) );
331 p->vInputs = Vec_PtrAlloc( 512 );
332 p->vOutputs = Vec_PtrAlloc( 512 );
333 p->vLatches = Vec_PtrAlloc( 512 );
334 p->vFlops = Vec_PtrAlloc( 512 );
335 p->vResets = Vec_PtrAlloc( 512 );
336 p->vNames = Vec_PtrAlloc( 512 );
337 p->vSubckts = Vec_PtrAlloc( 512 );
338 p->vShorts = Vec_PtrAlloc( 512 );
339 p->vOnehots = Vec_PtrAlloc( 512 );
340 p->vMvs = Vec_PtrAlloc( 512 );
341 p->vConstrs = Vec_PtrAlloc( 512 );
342 p->vLtlProperties = Vec_PtrAlloc( 512 );
343 return p;
344}
345
357static void Io_MvModFree( Io_MvMod_t * p )
358{
359// if ( p->pNtk )
360// Abc_NtkDelete( p->pNtk );
361 Vec_PtrFree( p->vLtlProperties );
362 Vec_PtrFree( p->vInputs );
363 Vec_PtrFree( p->vOutputs );
364 Vec_PtrFree( p->vLatches );
365 Vec_PtrFree( p->vFlops );
366 Vec_PtrFree( p->vResets );
367 Vec_PtrFree( p->vNames );
368 Vec_PtrFree( p->vSubckts );
369 Vec_PtrFree( p->vShorts );
370 Vec_PtrFree( p->vOnehots );
371 Vec_PtrFree( p->vMvs );
372 Vec_PtrFree( p->vConstrs );
373 ABC_FREE( p );
374}
375
376
377
389static int Io_MvCountChars( char * pLine, char Char )
390{
391 char * pCur;
392 int Counter = 0;
393 for ( pCur = pLine; *pCur; pCur++ )
394 if ( *pCur == Char )
395 Counter++;
396 return Counter;
397}
398
410static char * Io_MvFindArrow( char * pLine )
411{
412 char * pCur;
413 for ( pCur = pLine; *(pCur+1); pCur++ )
414 if ( *pCur == '-' && *(pCur+1) == '>' )
415 {
416 *pCur = ' ';
417 *(pCur+1) = ' ';
418 return pCur;
419 }
420 return NULL;
421}
422
434static void Io_MvCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput )
435{
436 char * pCur;
437 Vec_PtrClear( vTokens );
438 for ( pCur = pInput; pCur < pOutput; pCur++ )
439 {
440 if ( *pCur == 0 )
441 continue;
442 Vec_PtrPush( vTokens, pCur );
443 while ( *++pCur );
444 }
445}
446
458static void Io_MvSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop )
459{
460 char * pCur;
461 // clear spaces
462 for ( pCur = pLine; *pCur != Stop; pCur++ )
463 if ( Io_MvCharIsSpace(*pCur) )
464 *pCur = 0;
465 // collect tokens
466 Io_MvCollectTokens( vTokens, pLine, pCur );
467}
468
480static void Io_MvSplitIntoTokensMv( Vec_Ptr_t * vTokens, char * pLine )
481{
482 char * pCur;
483 // clear spaces
484 for ( pCur = pLine; *pCur != '.' || *(pCur+1) == 'd'; pCur++ )
485 if ( Io_MvCharIsSpace(*pCur) )
486 *pCur = 0;
487 // collect tokens
488 Io_MvCollectTokens( vTokens, pLine, pCur );
489}
490
502static void Io_MvSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char )
503{
504 char * pCur;
505 // clear spaces
506 for ( pCur = pLine; *pCur != Stop; pCur++ )
507 if ( Io_MvCharIsSpace(*pCur) || *pCur == Char )
508 *pCur = 0;
509 // collect tokens
510 Io_MvCollectTokens( vTokens, pLine, pCur );
511}
512
524static int Io_MvGetLine( Io_MvMan_t * p, char * pToken )
525{
526 char * pLine;
527 int i;
528 Vec_PtrForEachEntry( char *, p->vLines, pLine, i )
529 if ( pToken < pLine )
530 return i;
531 return -1;
532}
533
545typedef struct buflist {
546 char buf[1<<20];
547 int nBuf;
548 struct buflist * next;
550
551char * Io_MvLoadFileBz2( char * pFileName, long * pnFileSize )
552{
553 FILE * pFile;
554 long nFileSize = 0;
555 char * pContents;
556 BZFILE * b;
557 int bzError, RetValue;
558 struct buflist * pNext;
559 buflist * bufHead = NULL, * buf = NULL;
560
561 pFile = fopen( pFileName, "rb" );
562 if ( pFile == NULL )
563 {
564 Abc_Print( -1, "Io_MvLoadFileBz2(): The file is unavailable (absent or open).\n" );
565 return NULL;
566 }
567 b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0);
568 if (bzError != BZ_OK) {
569 Abc_Print( -1, "Io_MvLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError );
570 return NULL;
571 }
572 do {
573 if (!bufHead)
574 buf = bufHead = ABC_ALLOC( buflist, 1 );
575 else
576 buf = buf->next = ABC_ALLOC( buflist, 1 );
577 nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20);
578 buf->next = NULL;
579 } while (bzError == BZ_OK);
580 if (bzError == BZ_STREAM_END) {
581 // we're okay
582 char * p;
583 int nBytes = 0;
584 BZ2_bzReadClose(&bzError,b);
585 p = pContents = ABC_ALLOC( char, nFileSize + 10 );
586 buf = bufHead;
587 do {
588 memcpy(p+nBytes,buf->buf,(size_t)buf->nBuf);
589 nBytes += buf->nBuf;
590// } while((buf = buf->next));
591 pNext = buf->next;
592 ABC_FREE( buf );
593 } while((buf = pNext));
594 } else if (bzError == BZ_DATA_ERROR_MAGIC) {
595 // not a BZIP2 file
596 BZ2_bzReadClose(&bzError,b);
597 fseek( pFile, 0, SEEK_END );
598 nFileSize = ftell( pFile );
599 if ( nFileSize == 0 )
600 {
601 Abc_Print( -1, "Io_MvLoadFileBz2(): The file is empty.\n" );
602 return NULL;
603 }
604 pContents = ABC_ALLOC( char, nFileSize + 10 );
605 rewind( pFile );
606 RetValue = fread( pContents, nFileSize, 1, pFile );
607 } else {
608 // Some other error.
609 Abc_Print( -1, "Io_MvLoadFileBz2(): Unable to read the compressed BLIF.\n" );
610 return NULL;
611 }
612 fclose( pFile );
613 // finish off the file with the spare .end line
614 // some benchmarks suddenly break off without this line
615 strcpy( pContents + nFileSize, "\n.end\n" );
616 *pnFileSize = nFileSize;
617 return pContents;
618}
619
631static char * Io_MvLoadFileGz( char * pFileName, long * pnFileSize )
632{
633 const int READ_BLOCK_SIZE = 100000;
634 gzFile pFile;
635 char * pContents;
636 long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
637 pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
638 pContents = ABC_ALLOC( char, nFileSize );
639 readBlock = 0;
640 while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
641 //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
642 nFileSize += READ_BLOCK_SIZE;
643 pContents = ABC_REALLOC(char, pContents, nFileSize);
644 ++readBlock;
645 }
646 //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
647 assert( amtRead != -1 ); // indicates a zlib error
648 nFileSize -= (READ_BLOCK_SIZE - amtRead);
649 gzclose(pFile);
650 *pnFileSize = nFileSize;
651 return pContents;
652}
653
665static char * Io_MvLoadFile( char * pFileName )
666{
667 FILE * pFile;
668 long nFileSize;
669 char * pContents;
670 int RetValue;
671 if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
672 return Io_MvLoadFileBz2( pFileName, &nFileSize );
673 if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
674 return Io_MvLoadFileGz( pFileName, &nFileSize );
675 pFile = fopen( pFileName, "rb" );
676 if ( pFile == NULL )
677 {
678 printf( "Io_MvLoadFile(): The file is unavailable (absent or open).\n" );
679 return NULL;
680 }
681 fseek( pFile, 0, SEEK_END );
682 nFileSize = ftell( pFile );
683 if ( nFileSize == 0 )
684 {
685 fclose( pFile );
686 printf( "Io_MvLoadFile(): The file is empty.\n" );
687 return NULL;
688 }
689 pContents = ABC_ALLOC( char, nFileSize + 10 );
690 rewind( pFile );
691 RetValue = fread( pContents, nFileSize, 1, pFile );
692 fclose( pFile );
693 // finish off the file with the spare .end line
694 // some benchmarks suddenly break off without this line
695 strcpy( pContents + nFileSize, "\n.end\n" );
696 return pContents;
697}
698
711{
712 if ( !strstr(p, ".gate") )
713 return;
714 char * q, * pNext, * pShort = (char *)".short"; int i;
715 for ( q = p; *q && (pNext = strstr(q, ".names")); q = pNext ) {
716 for ( i = 0; i < 6; i++ )
717 pNext[i] = pShort[i];
718 while ( *pNext && *pNext++ != '\n' );
719 if ( *pNext == 0 )
720 return;
721 while ( *pNext && *pNext != '\n' )
722 *pNext++ = ' ';
723 if ( *pNext == 0 )
724 return;
725 }
726}
727
745static void Io_MvReadPreparse( Io_MvMan_t * p )
746{
747 char * pCur, * pPrev;
748 int i, fComment = 0;
749 Io_MvReplaceBuffersByShorts( p->pBuffer );
750
751 // parse the buffer into lines and remove comments
752 Vec_PtrPush( p->vLines, p->pBuffer );
753 for ( pCur = p->pBuffer; *pCur; pCur++ )
754 {
755 if ( *pCur == '\n' )
756 {
757 *pCur = 0;
758// if ( *(pCur-1) == '\r' )
759// *(pCur-1) = 0;
760 fComment = 0;
761 Vec_PtrPush( p->vLines, pCur + 1 );
762 }
763 else if ( *pCur == '#' )
764 fComment = 1;
765 // remove comments
766 if ( fComment )
767 *pCur = 0;
768 }
769
770 // unfold the line extensions and sort lines by directive
771 Vec_PtrForEachEntry( char *, p->vLines, pCur, i )
772 {
773 if ( *pCur == 0 )
774 continue;
775 // find previous non-space character
776 for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- )
777 if ( !Io_MvCharIsSpace(*pPrev) )
778 break;
779 // if it is the line extender, overwrite it with spaces
780 if ( pPrev >= p->pBuffer && *pPrev == '\\' )
781 {
782 for ( ; *pPrev; pPrev++ )
783 *pPrev = ' ';
784 *pPrev = ' ';
785 continue;
786 }
787 // skip spaces at the beginning of the line
788 while ( Io_MvCharIsSpace(*pCur++) );
789 // parse directives
790 if ( *(pCur-1) != '.' )
791 continue;
792 if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) || !strncmp(pCur, "gate", 4) )
793 Vec_PtrPush( p->pLatest->vNames, pCur );
794 else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) )
795 continue;
796 else if ( !strncmp( pCur, "ltlformula", 10 ) )
797 Vec_PtrPush( p->pLatest->vLtlProperties, pCur );
798 else if ( !strncmp(pCur, "latch", 5) )
799 Vec_PtrPush( p->pLatest->vLatches, pCur );
800 else if ( !strncmp(pCur, "flop", 4) )
801 Vec_PtrPush( p->pLatest->vFlops, pCur );
802 else if ( !strncmp(pCur, "r ", 2) || !strncmp(pCur, "reset ", 6) )
803 Vec_PtrPush( p->pLatest->vResets, pCur );
804 else if ( !strncmp(pCur, "inputs", 6) )
805 Vec_PtrPush( p->pLatest->vInputs, pCur );
806 else if ( !strncmp(pCur, "outputs", 7) )
807 Vec_PtrPush( p->pLatest->vOutputs, pCur );
808 else if ( !strncmp(pCur, "subckt", 6) )
809 Vec_PtrPush( p->pLatest->vSubckts, pCur );
810 else if ( !strncmp(pCur, "short", 5) )
811 Vec_PtrPush( p->pLatest->vShorts, pCur );
812 else if ( !strncmp(pCur, "onehot", 6) )
813 Vec_PtrPush( p->pLatest->vOnehots, pCur );
814 else if ( p->fBlifMv && !strncmp(pCur, "mv", 2) )
815 Vec_PtrPush( p->pLatest->vMvs, pCur );
816 else if ( !strncmp(pCur, "constraint", 10) )
817 Vec_PtrPush( p->pLatest->vConstrs, pCur );
818 else if ( !strncmp(pCur, "blackbox", 8) )
819 p->pLatest->fBlackBox = 1;
820 else if ( !strncmp(pCur, "model", 5) )
821 {
822 p->pLatest = Io_MvModAlloc();
823 p->pLatest->pName = pCur;
824 p->pLatest->pMan = p;
825 }
826 else if ( !strncmp(pCur, "end", 3) )
827 {
828 if ( p->pLatest )
829 Vec_PtrPush( p->vModels, p->pLatest );
830 p->pLatest = NULL;
831 }
832 else if ( !strncmp(pCur, "exdc", 4) )
833 {
834// fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) );
835 fprintf( stdout, "Warning: The design contains EXDC network.\n" );
836 if ( p->pLatest )
837 Vec_PtrPush( p->vModels, p->pLatest );
838 p->pLatest = Io_MvModAlloc();
839 p->pLatest->pName = NULL;
840 p->pLatest->pMan = p;
841 }
842 else if ( !strncmp(pCur, "attrib", 6) )
843 {}
844 else if ( !strncmp(pCur, "delay", 5) )
845 {}
846 else if ( !strncmp(pCur, "input_", 6) )
847 {}
848 else if ( !strncmp(pCur, "output_", 7) )
849 {}
850 else if ( !strncmp(pCur, "no_merge", 8) )
851 {}
852 else if ( !strncmp(pCur, "wd", 2) )
853 {}
854// else if ( !strncmp(pCur, "inouts", 6) )
855// {}
856 else
857 {
858 pCur--;
859 if ( pCur[strlen(pCur)-1] == '\r' )
860 pCur[strlen(pCur)-1] = 0;
861 fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Io_MvGetLine(p, pCur), pCur );
862 }
863 }
864}
865
877static int Io_MvReadInterfaces( Io_MvMan_t * p )
878{
879 Io_MvMod_t * pMod;
880 char * pLine;
881 int i, k, nOutsOld;
882 // iterate through the models
883 Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
884 {
885 // parse the model
886 if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
887 return 0;
888 // add model to the design
889 if ( !Abc_DesAddModel( p->pDesign, pMod->pNtk ) )
890 {
891 sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName );
892 return 0;
893 }
894 // parse the inputs
895 Vec_PtrForEachEntry( char *, pMod->vInputs, pLine, k )
896 if ( !Io_MvParseLineInputs( pMod, pLine ) )
897 return 0;
898 // parse the outputs
899 Vec_PtrForEachEntry( char *, pMod->vOutputs, pLine, k )
900 if ( !Io_MvParseLineOutputs( pMod, pLine ) )
901 return 0;
902 // parse the constraints
903 nOutsOld = Abc_NtkPoNum(pMod->pNtk);
904 Vec_PtrForEachEntry( char *, pMod->vConstrs, pLine, k )
905 if ( !Io_MvParseLineConstrs( pMod, pLine ) )
906 return 0;
907 pMod->pNtk->nConstrs = Abc_NtkPoNum(pMod->pNtk) - nOutsOld;
908 Vec_PtrForEachEntry( char *, pMod->vLtlProperties, pLine, k )
909 if ( !Io_MvParseLineLtlProperty( pMod, pLine ) )
910 return 0;
911 // report the results
912#ifdef IO_VERBOSE_OUTPUT
913 if ( Vec_PtrSize(p->vModels) > 1 )
914 printf( "Parsed %-32s: PI =%6d PO =%6d ND =%8d FF =%6d B =%6d\n",
915 pMod->pNtk->pName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkPoNum(pMod->pNtk),
916 Vec_PtrSize(pMod->vNames), Vec_PtrSize(pMod->vLatches), Vec_PtrSize(pMod->vSubckts) );
917#endif
918 }
919 return 1;
920}
921
922
934static Abc_Des_t * Io_MvParse( Io_MvMan_t * p )
935{
936 Abc_Des_t * pDesign;
937 Io_MvMod_t * pMod;
938 char * pLine;
939 int i, k;
940 // iterate through the models
941 Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
942 {
943#ifdef IO_VERBOSE_OUTPUT
944 if ( Vec_PtrSize(p->vModels) > 1 )
945 printf( "Parsing model %s...\n", pMod->pNtk->pName );
946#endif
947
948 // check if there any MV lines
949 if ( Vec_PtrSize(pMod->vMvs) > 0 )
950 Abc_NtkStartMvVars( pMod->pNtk );
951 // parse the mv lines
952 Vec_PtrForEachEntry( char *, pMod->vMvs, pLine, k )
953 if ( !Io_MvParseLineMv( pMod, pLine ) )
954 return NULL;
955 // if reset lines are used there should be the same number of them as latches
956 if ( Vec_PtrSize(pMod->vResets) > 0 )
957 {
958 if ( Vec_PtrSize(pMod->vLatches) != Vec_PtrSize(pMod->vResets) )
959 {
960 sprintf( p->sError, "Line %d: Model %s has different number of latches (%d) and reset nodes (%d).",
961 Io_MvGetLine(p, pMod->pName), Abc_NtkName(pMod->pNtk), Vec_PtrSize(pMod->vLatches), Vec_PtrSize(pMod->vResets) );
962 return NULL;
963 }
964 // create binary latch with 1-data and 0-init
965 if ( p->fUseReset )
966 pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
967 }
968 // parse the flops
969 Vec_PtrForEachEntry( char *, pMod->vFlops, pLine, k )
970 if ( !Io_MvParseLineFlop( pMod, pLine ) )
971 return NULL;
972 // parse the latches
973 Vec_PtrForEachEntry( char *, pMod->vLatches, pLine, k )
974 if ( !Io_MvParseLineLatch( pMod, pLine ) )
975 return NULL;
976 // parse the reset lines
977 if ( p->fUseReset )
978 Vec_PtrForEachEntry( char *, pMod->vResets, pLine, k )
979 if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
980 return NULL;
981 // parse the nodes
982 if ( p->fBlifMv )
983 {
984 Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
985 if ( !Io_MvParseLineNamesMv( pMod, pLine, 0 ) )
986 return NULL;
987 }
988 else
989 {
990 Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
991 if ( !Io_MvParseLineNamesBlif( pMod, pLine ) )
992 return NULL;
993 Vec_PtrForEachEntry( char *, pMod->vShorts, pLine, k )
994 if ( !Io_MvParseLineShortBlif( pMod, pLine ) )
995 return NULL;
996 }
997 // parse the subcircuits
998 Vec_PtrForEachEntry( char *, pMod->vSubckts, pLine, k )
999 if ( !Io_MvParseLineSubckt( pMod, pLine ) )
1000 return NULL;
1001
1002 // allow for blackboxes without .blackbox line
1003 if ( Abc_NtkLatchNum(pMod->pNtk) == 0 && Abc_NtkNodeNum(pMod->pNtk) == 0 && Abc_NtkBoxNum(pMod->pNtk) == 0 )
1004 {
1005 if ( pMod->pNtk->ntkFunc == ABC_FUNC_SOP )
1006 {
1007 Mem_FlexStop( (Mem_Flex_t *)pMod->pNtk->pManFunc, 0 );
1008 pMod->pNtk->pManFunc = NULL;
1010 }
1011 }
1012
1013 // finalize the network
1014 Abc_NtkFinalizeRead( pMod->pNtk );
1015 // read the one-hotness lines
1016 if ( Vec_PtrSize(pMod->vOnehots) > 0 )
1017 {
1018 Vec_Int_t * vLine;
1019 Abc_Obj_t * pObj;
1020 // set register numbers
1021 Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
1022 pObj->pNext = (Abc_Obj_t *)(ABC_PTRINT_T)k;
1023 // derive register
1024 pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
1025 Vec_PtrForEachEntry( char *, pMod->vOnehots, pLine, k )
1026 {
1027 vLine = Io_MvParseLineOnehot( pMod, pLine );
1028 if ( vLine == NULL )
1029 return NULL;
1030 Vec_PtrPush( pMod->pNtk->vOnehots, vLine );
1031// printf( "Parsed %d one-hot registers.\n", Vec_IntSize(vLine) );
1032 }
1033 // reset register numbers
1034 Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
1035 pObj->pNext = NULL;
1036 // print the result
1037 printf( "Parsed %d groups of 1-hot registers: { ", Vec_PtrSize(pMod->pNtk->vOnehots) );
1038 Vec_PtrForEachEntry( Vec_Int_t *, pMod->pNtk->vOnehots, vLine, k )
1039 printf( "%d ", Vec_IntSize(vLine) );
1040 printf( "}\n" );
1041 printf( "The total number of 1-hot registers = %d. (%.2f %%)\n",
1042 Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ),
1043 100.0 * Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ) / Abc_NtkLatchNum(pMod->pNtk) );
1044 {
1045 extern void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots );
1046 char * pFileName = Extra_FileNameGenericAppend( pMod->pMan->pFileName, "_1h.blif" );
1047 Abc_GenOneHotIntervals( pFileName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkLatchNum(pMod->pNtk), pMod->pNtk->vOnehots );
1048 printf( "One-hotness condition is written into file \"%s\".\n", pFileName );
1049 }
1050 }
1051 if ( Vec_PtrSize(pMod->vFlops) )
1052 {
1053 printf( "Warning: The parser converted %d .flop lines into .latch lines\n", Vec_PtrSize(pMod->vFlops) );
1054 printf( "(information about set, reset, enable of the flops may be lost).\n" );
1055 }
1056
1057 }
1058 if ( p->nNDnodes )
1059// printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
1060 printf( "Warning: The parser added %d constant 0 nodes to replace non-deterministic nodes.\n", p->nNDnodes );
1061 // return the network
1062 pDesign = p->pDesign;
1063 p->pDesign = NULL;
1064 return pDesign;
1065}
1066
1078static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
1079{
1080 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1081 char * pToken, * pPivot;
1082 if ( pLine == NULL )
1083 {
1085 p->pNtk->pName = Extra_UtilStrsav( "EXDC" );
1086 return 1;
1087 }
1088 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1089 pToken = (char *)Vec_PtrEntry( vTokens, 0 );
1090 assert( !strcmp(pToken, "model") );
1091 if ( Vec_PtrSize(vTokens) != 2 )
1092 {
1093 sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
1094 return 0;
1095 }
1096 if ( p->fBlackBox )
1098 else if ( p->pMan->fBlifMv )
1100 else
1102// for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
1103// if ( *pToken == '/' || *pToken == '\\' )
1104// pPivot = pToken+1;
1105 pPivot = pToken = (char *)Vec_PtrEntry(vTokens, 1);
1106 p->pNtk->pName = Extra_UtilStrsav( pPivot );
1107 return 1;
1108}
1109
1121static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine )
1122{
1123 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1124 char * pToken;
1125 int i;
1126 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1127 pToken = (char *)Vec_PtrEntry(vTokens, 0);
1128 assert( !strcmp(pToken, "inputs") );
1129 Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
1130 Io_ReadCreatePi( p->pNtk, pToken );
1131 return 1;
1132}
1133
1145static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine )
1146{
1147 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1148 char * pToken;
1149 int i;
1150 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1151 pToken = (char *)Vec_PtrEntry(vTokens, 0);
1152 assert( !strcmp(pToken, "outputs") );
1153 Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
1154 Io_ReadCreatePo( p->pNtk, pToken );
1155 return 1;
1156}
1157
1169static int Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine )
1170{
1171 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1172 char * pToken;
1173 int i;
1174 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1175 pToken = (char *)Vec_PtrEntry(vTokens, 0);
1176 assert( !strcmp(pToken, "constraint") );
1177 Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
1178 Io_ReadCreatePo( p->pNtk, pToken );
1179 return 1;
1180}
1181
1193static int Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine )
1194{
1195 int i, j;
1196 int quoteBegin, quoteEnd;
1197 char keyWordLtlFormula[11];
1198 char *actualLtlFormula;
1199
1200 //checking if the line begins with the keyword "ltlformula" and
1201 //progressing the pointer forword
1202 for( i=0; i<10; i++ )
1203 keyWordLtlFormula[i] = pLine[i];
1204 quoteBegin = i;
1205 keyWordLtlFormula[10] = '\0';
1206 assert( strcmp( "ltlformula", keyWordLtlFormula ) == 0 );
1207 while( pLine[i] != '"' )
1208 i++;
1209 quoteBegin = i;
1210 i = strlen( pLine );
1211 while( pLine[i] != '"' )
1212 i--;
1213 quoteEnd = i;
1214 actualLtlFormula = (char *)malloc( sizeof(char) * (quoteEnd - quoteBegin) );
1215 //printf("\nThe input ltl formula = ");
1216 for( i = quoteBegin + 1, j = 0; i<quoteEnd; i++, j++ )
1217 //printf("%c", pLine[i] );
1218 actualLtlFormula[j] = pLine[i];
1219 actualLtlFormula[j] = '\0';
1220 Vec_PtrPush( vGlobalLtlArray, actualLtlFormula );
1221 return 1;
1222}
1223
1224
1236static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
1237{
1238 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1239 Abc_Obj_t * pObj, * pNet;
1240 char * pToken;
1241 int Init;
1242 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1243 pToken = (char *)Vec_PtrEntry(vTokens,0);
1244 assert( !strcmp(pToken, "latch") );
1245 if ( Vec_PtrSize(vTokens) < 3 )
1246 {
1247 sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Io_MvGetLine(p->pMan, pToken) );
1248 return 0;
1249 }
1250 // create latch
1251 if ( p->pResetLatch == NULL )
1252 {
1253 pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), (char *)Vec_PtrEntry(vTokens,2) );
1254 // get initial value
1255 if ( p->pMan->fBlifMv )
1256 Abc_LatchSetInit0( pObj );
1257 else
1258 {
1259 if ( Vec_PtrSize(vTokens) > 6 )
1260 printf( "Warning: Line %d has .latch directive with unrecognized entries (the total of %d entries).\n",
1261 Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
1262 if ( Vec_PtrSize(vTokens) > 3 )
1263 Init = atoi( (char *)Vec_PtrEntryLast(vTokens) );
1264 else
1265 Init = 2;
1266 if ( Init < 0 || Init > 3 )
1267 {
1268 sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
1269 return 0;
1270 }
1271 if ( Init == 0 )
1272 Abc_LatchSetInit0( pObj );
1273 else if ( Init == 1 )
1274 Abc_LatchSetInit1( pObj );
1275 else // if ( Init == 2 )
1276 Abc_LatchSetInitDc( pObj );
1277 }
1278 }
1279 else
1280 {
1281 // get the net corresponding to the output of the latch
1282 pNet = Abc_NtkFindOrCreateNet( p->pNtk, (char *)Vec_PtrEntry(vTokens,2) );
1283 // get the net corresponding to the latch output (feeding into reset MUX)
1284 pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") );
1285 // create latch
1286 pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) );
1287// Abc_LatchSetInit0( pObj );
1288 Abc_LatchSetInit0( pObj );
1289 }
1290 return 1;
1291}
1292
1304static int Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine )
1305{
1306 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1307 Abc_Obj_t * pObj;
1308 char * pToken, * pOutput, * pInput;
1309 int i, Init = 2;
1310 assert( !p->pMan->fBlifMv );
1311 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1312 pToken = (char *)Vec_PtrEntry(vTokens,0);
1313 assert( !strcmp(pToken, "flop") );
1314 // get flop output
1315 Vec_PtrForEachEntry( char *, vTokens, pToken, i )
1316 if ( pToken[0] == 'Q' && pToken[1] == '=' )
1317 break;
1318 if ( i == Vec_PtrSize(vTokens) )
1319 {
1320 sprintf( p->pMan->sError, "Line %d: Cannot find flop output.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
1321 return 0;
1322 }
1323 pOutput = pToken+2;
1324 // get flop input
1325 Vec_PtrForEachEntry( char *, vTokens, pToken, i )
1326 if ( pToken[0] == 'D' && pToken[1] == '=' )
1327 break;
1328 if ( i == Vec_PtrSize(vTokens) )
1329 {
1330 sprintf( p->pMan->sError, "Line %d: Cannot find flop input.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
1331 return 0;
1332 }
1333 pInput = pToken+2;
1334 // create latch
1335 pObj = Io_ReadCreateLatch( p->pNtk, pInput, pOutput );
1336 // get the init value
1337 Vec_PtrForEachEntry( char *, vTokens, pToken, i )
1338 {
1339 if ( !strncmp( pToken, "init=", 5 ) )
1340 {
1341 Init = 0;
1342 if ( pToken[5] == '1' )
1343 Init = 1;
1344 else if ( pToken[5] == '2' )
1345 Init = 2;
1346 else if ( pToken[5] != '0' )
1347 {
1348 sprintf( p->pMan->sError, "Line %d: Cannot read flop init value %s.", Io_MvGetLine(p->pMan, pToken), pToken );
1349 return 0;
1350 }
1351 break;
1352 }
1353 }
1354 if ( Init < 0 || Init > 2 )
1355 {
1356 sprintf( p->pMan->sError, "Line %d: Initial state of the flop is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
1357 return 0;
1358 }
1359 if ( Init == 0 )
1360 Abc_LatchSetInit0( pObj );
1361 else if ( Init == 1 )
1362 Abc_LatchSetInit1( pObj );
1363 else // if ( Init == 2 )
1364 Abc_LatchSetInitDc( pObj );
1365 return 1;
1366}
1367
1379static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
1380{
1381 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1382 Abc_Ntk_t * pModel;
1383 Abc_Obj_t * pBox, * pNet, * pTerm;
1384 char * pToken, * pName, * pName2, ** ppNames;
1385 int nEquals, i, k;
1386 word Last;
1387
1388 // split the line into tokens
1389 nEquals = Io_MvCountChars( pLine, '=' );
1390 Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
1391 pToken = (char *)Vec_PtrEntry(vTokens,0);
1392 assert( !strcmp(pToken, "subckt") );
1393//printf( "%d ", nEquals );
1394
1395 // get the model for this box
1396 pName = (char *)Vec_PtrEntry(vTokens,1);
1397 // skip instance name for now
1398 for ( pToken = pName; *pToken; pToken++ )
1399 if ( *pToken == '|' )
1400 {
1401 *pToken = 0;
1402 break;
1403 }
1404 // find the model
1405 pModel = Abc_DesFindModelByName( p->pMan->pDesign, pName );
1406 if ( pModel == NULL )
1407 {
1408 sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Io_MvGetLine(p->pMan, pToken), pName );
1409 return 0;
1410 }
1411/*
1412 // check if the number of tokens is correct
1413 if ( nEquals != Abc_NtkPiNum(pModel) + Abc_NtkPoNum(pModel) )
1414 {
1415 sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).",
1416 Io_MvGetLine(p->pMan, pToken), nEquals, Abc_NtkPiNum(pModel) + Abc_NtkPoNum(pModel) );
1417 return 0;
1418 }
1419*/
1420 // get the names
1421 ppNames = (char **)Vec_PtrArray(vTokens) + 2 + p->pMan->fBlifMv;
1422
1423 // create the box with these terminals
1424 if ( Abc_NtkHasBlackbox(pModel) )
1425 pBox = Abc_NtkCreateBlackbox( p->pNtk );
1426 else
1427 pBox = Abc_NtkCreateWhitebox( p->pNtk );
1428 pBox->pData = pModel;
1429 if ( p->pMan->fBlifMv )
1430 Abc_ObjAssignName( pBox, (char *)Vec_PtrEntry(vTokens,2), NULL );
1431 // go through formal inputs
1432 Last = 0;
1433 Abc_NtkForEachPi( pModel, pTerm, i )
1434 {
1435 // find this terminal among the actual inputs of the subcircuit
1436 pName2 = NULL;
1437 pName = Abc_ObjName(Abc_ObjFanout0(pTerm));
1438 for ( k = 0; k < nEquals; k++ )
1439 if ( !strcmp( ppNames[2*(int)((k+Last)%nEquals)], pName ) )
1440 {
1441 pName2 = ppNames[2*(int)((k+Last)%nEquals)+1];
1442 Last = k+Last+1;
1443 break;
1444 }
1445
1446 if ( k == nEquals )
1447 {
1448 sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.",
1449 Io_MvGetLine(p->pMan, pToken), pName, Abc_NtkName(pModel) );
1450 return 0;
1451 }
1452
1453 if ( pName2 == NULL )
1454 {
1455 Abc_Obj_t * pNode = Abc_NtkCreateNodeConst0( p->pNtk );
1456 //pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, " 0\n" );
1457 pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNode, "abc") );
1458 Abc_ObjAddFanin( pNet, pNode );
1459 pTerm = Abc_NtkCreateBi( p->pNtk );
1460 Abc_ObjAddFanin( pBox, pTerm );
1461 Abc_ObjAddFanin( pTerm, pNet );
1462 continue;
1463 }
1464 assert( pName2 != NULL );
1465
1466 // create the BI with the actual name
1467 pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName2 );
1468 pTerm = Abc_NtkCreateBi( p->pNtk );
1469 Abc_ObjAddFanin( pBox, pTerm );
1470 Abc_ObjAddFanin( pTerm, pNet );
1471 }
1472 // go through formal outputs
1473 Last = 0;
1474 Abc_NtkForEachPo( pModel, pTerm, i )
1475 {
1476 // find this terminal among the actual outputs of the subcircuit
1477 pName2 = NULL;
1478 pName = Abc_ObjName(Abc_ObjFanin0(pTerm));
1479 for ( k = 0; k < nEquals; k++ )
1480 if ( !strcmp( ppNames[2*((k+Last)%nEquals)], pName ) )
1481 {
1482 pName2 = ppNames[2*((k+Last)%nEquals)+1];
1483 Last = k+Last+1;
1484 break;
1485 }
1486/*
1487 if ( k == nEquals )
1488 {
1489 sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the modell \"%s\" as a formal output of the subcircuit.",
1490 Io_MvGetLine(p->pMan, pToken), pName, Abc_NtkName(pModel) );
1491 return 0;
1492 }
1493*/
1494
1495 // create the BI with the actual name
1496 pTerm = Abc_NtkCreateBo( p->pNtk );
1497 pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName2 == NULL ? Abc_ObjNameSuffix(pTerm, "abc") : pName2 );
1498 Abc_ObjAddFanin( pNet, pTerm );
1499 Abc_ObjAddFanin( pTerm, pBox );
1500 }
1501 return 1;
1502}
1503
1515static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
1516{
1517 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1518// Vec_Ptr_t * vResult;
1519 Vec_Int_t * vResult;
1520 Abc_Obj_t * pNet, * pTerm;
1521 char * pToken;
1522 int nEquals, i;
1523
1524 // split the line into tokens
1525 nEquals = Io_MvCountChars( pLine, '=' );
1526 Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
1527 pToken = (char *)Vec_PtrEntry(vTokens,0);
1528 assert( !strcmp(pToken, "onehot") );
1529
1530 // iterate through the register names
1531// vResult = Vec_PtrAlloc( Vec_PtrSize(vTokens) );
1532 vResult = Vec_IntAlloc( Vec_PtrSize(vTokens) );
1533 Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
1534 {
1535 // check if this register exists
1536 pNet = Abc_NtkFindNet( p->pNtk, pToken );
1537 if ( pNet == NULL )
1538 {
1539 sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" does not exist in the model \"%s\".",
1540 Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
1541 return NULL;
1542 }
1543 // check if this is register output net
1544 pTerm = Abc_ObjFanin0( pNet );
1545 if ( pTerm == NULL || Abc_ObjFanin0(pTerm) == NULL || !Abc_ObjIsLatch(Abc_ObjFanin0(pTerm)) )
1546 {
1547 sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" is not a register in the model \"%s\".",
1548 Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
1549 return NULL;
1550 }
1551 // save register name
1552// Vec_PtrPush( vResult, Abc_ObjName(pNet) );
1553 Vec_IntPush( vResult, (int)(ABC_PTRINT_T)Abc_ObjFanin0(pTerm)->pNext );
1554// printf( "%d(%d) ", (int)Abc_ObjFanin0(pTerm)->pNext, ((int)Abc_ObjFanin0(pTerm)->pData) -1 );
1555 printf( "%d", ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pTerm)->pData)-1 );
1556 }
1557 printf( "\n" );
1558 return vResult;
1559}
1560
1561
1573static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
1574{
1575 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1576 Abc_Obj_t * pObj;
1577 Io_MvVar_t * pVar = NULL;
1578 Mem_Flex_t * pFlex;
1579 char * pName;
1580 int nCommas, nValues, i, k;
1581 // count commas and get the tokens
1582 nCommas = Io_MvCountChars( pLine, ',' );
1583 Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', ',' );
1584 pName = (char *)Vec_PtrEntry(vTokens,0);
1585 assert( !strcmp(pName, "mv") );
1586 // get the number of values
1587 if ( Vec_PtrSize(vTokens) <= nCommas + 2 )
1588 {
1589 sprintf( p->pMan->sError, "Line %d: The number of values in not specified in .mv line.", Io_MvGetLine(p->pMan, pName) );
1590 return 0;
1591 }
1592 nValues = atoi( (char *)Vec_PtrEntry(vTokens,nCommas+2) );
1593 if ( nValues < 2 || nValues > IO_BLIFMV_MAXVALUES )
1594 {
1595 sprintf( p->pMan->sError, "Line %d: The number of values (%d) is incorrect (should be >= 2 and <= %d).",
1596 Io_MvGetLine(p->pMan, pName), nValues, IO_BLIFMV_MAXVALUES );
1597 return 0;
1598 }
1599 // if there is no symbolic values, quit
1600 if ( nValues == 2 && Vec_PtrSize(vTokens) == nCommas + 3 )
1601 return 1;
1602 if ( Vec_PtrSize(vTokens) > nCommas + 3 && Vec_PtrSize(vTokens) - (nCommas + 3) != nValues )
1603 {
1604 sprintf( p->pMan->sError, "Line %d: Wrong number (%d) of symbolic value names (should be %d).",
1605 Io_MvGetLine(p->pMan, pName), Vec_PtrSize(vTokens) - (nCommas + 3), nValues );
1606 return 0;
1607 }
1608 // go through variables
1609 pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( p->pNtk );
1610 for ( i = 0; i <= nCommas; i++ )
1611 {
1612 pName = (char *)Vec_PtrEntry( vTokens, i+1 );
1613 pObj = Abc_NtkFindOrCreateNet( p->pNtk, pName );
1614 // allocate variable
1615 pVar = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
1616 pVar->nValues = nValues;
1617 pVar->pNames = NULL;
1618 // create names
1619 if ( Vec_PtrSize(vTokens) > nCommas + 3 )
1620 {
1621 pVar->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * nValues );
1622 Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nCommas + 3 )
1623 {
1624 pVar->pNames[k-(nCommas + 3)] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pName) + 1 );
1625 strcpy( pVar->pNames[k-(nCommas + 3)], pName );
1626 }
1627 }
1628 // save the variable
1629 Abc_ObjSetMvVar( pObj, pVar );
1630 }
1631 // make sure the names are unique
1632 assert(pVar);
1633 if ( pVar->pNames )
1634 {
1635 for ( i = 0; i < nValues; i++ )
1636 for ( k = i+1; k < nValues; k++ )
1637 if ( !strcmp(pVar->pNames[i], pVar->pNames[k]) )
1638 {
1639 pName = (char *)Vec_PtrEntry(vTokens,0);
1640 sprintf( p->pMan->sError, "Line %d: Symbolic value name \"%s\" is repeated in .mv line.",
1641 Io_MvGetLine(p->pMan, pName), pVar->pNames[i] );
1642 return 0;
1643 }
1644 }
1645 return 1;
1646}
1647
1659static int Io_MvWriteValues( Abc_Obj_t * pNode, Vec_Str_t * vFunc )
1660{
1661 char Buffer[10];
1662 Abc_Obj_t * pFanin;
1663 int i;
1664 // add the fanin number of values
1665 Abc_ObjForEachFanin( pNode, pFanin, i )
1666 {
1667 sprintf( Buffer, "%d", Abc_ObjMvVarNum(pFanin) );
1668 Vec_StrPrintStr( vFunc, Buffer );
1669 Vec_StrPush( vFunc, ' ' );
1670 }
1671 // add the node number of values
1672 sprintf( Buffer, "%d", Abc_ObjMvVarNum(Abc_ObjFanout0(pNode)) );
1673 Vec_StrPrintStr( vFunc, Buffer );
1674 Vec_StrPush( vFunc, '\n' );
1675 return 1;
1676}
1677
1689static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken, Vec_Str_t * vFunc, int iLit )
1690{
1691 char Buffer[16];
1692 Io_MvVar_t * pVar;
1693 Abc_Obj_t * pFanin, * pNet;
1694 char * pCur, * pNext;
1695 int i;
1696 // consider the equality literal
1697 if ( pToken[0] == '=' )
1698 {
1699 // find the fanins
1700 Abc_ObjForEachFanin( pNode, pFanin, i )
1701 if ( !strcmp( Abc_ObjName(pFanin), pToken + 1 ) )
1702 break;
1703 if ( i == Abc_ObjFaninNum(pNode) )
1704 {
1705 sprintf( p->pMan->sError, "Line %d: Node name in the table \"%s\" cannot be found on .names line.",
1706 Io_MvGetLine(p->pMan, pToken), pToken + 1 );
1707 return 0;
1708 }
1709 Vec_StrPush( vFunc, '=' );
1710 sprintf( Buffer, "%d", i );
1711 Vec_StrPrintStr( vFunc, Buffer );
1712 Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
1713 return 1;
1714 }
1715 // consider regular literal
1716 assert( iLit < Abc_ObjFaninNum(pNode) );
1717 pNet = iLit >= 0 ? Abc_ObjFanin(pNode, iLit) : Abc_ObjFanout0(pNode);
1718 pVar = (Io_MvVar_t *)Abc_ObjMvVar( pNet );
1719 // if the var is absent or has no symbolic values quit
1720 if ( pVar == NULL || pVar->pNames == NULL )
1721 {
1722 Vec_StrPrintStr( vFunc, pToken );
1723 Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
1724 return 1;
1725 }
1726 // parse the literal using symbolic values
1727 for ( pCur = pToken; *pCur; pCur++ )
1728 {
1729 if ( Io_MvCharIsMvSymb(*pCur) )
1730 {
1731 Vec_StrPush( vFunc, *pCur );
1732 continue;
1733 }
1734 // find the next MvSymb char
1735 for ( pNext = pCur+1; *pNext; pNext++ )
1736 if ( Io_MvCharIsMvSymb(*pNext) )
1737 break;
1738 // look for the value name
1739 for ( i = 0; i < pVar->nValues; i++ )
1740 if ( !strncmp( pVar->pNames[i], pCur, pNext-pCur ) )
1741 break;
1742 if ( i == pVar->nValues )
1743 {
1744 *pNext = 0;
1745 sprintf( p->pMan->sError, "Line %d: Cannot find value name \"%s\" among the value names of variable \"%s\".",
1746 Io_MvGetLine(p->pMan, pToken), pCur, Abc_ObjName(pNet) );
1747 return 0;
1748 }
1749 // value name is found
1750 sprintf( Buffer, "%d", i );
1751 Vec_StrPrintStr( vFunc, Buffer );
1752 // update the pointer
1753 pCur = pNext - 1;
1754 }
1755 Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
1756 return 1;
1757}
1758
1770static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vTokens2, int nInputs, int nOutputs, int iOut )
1771{
1772 Vec_Str_t * vFunc = p->pMan->vFunc;
1773 char * pFirst, * pToken;
1774 int iStart, i;
1775 // prepare the place for the cover
1776 Vec_StrClear( vFunc );
1777 // write the number of values
1778// Io_MvWriteValues( pNode, vFunc );
1779 // get the first token
1780 pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
1781 if ( pFirst[0] == '.' )
1782 {
1783 // write the default literal
1784 Vec_StrPush( vFunc, 'd' );
1785 pToken = (char *)Vec_PtrEntry(vTokens2, 1 + iOut);
1786 if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
1787 return NULL;
1788 iStart = 1 + nOutputs;
1789 }
1790 else
1791 iStart = 0;
1792 // write the remaining literals
1793 while ( iStart < Vec_PtrSize(vTokens2) )
1794 {
1795 // input literals
1796 for ( i = 0; i < nInputs; i++ )
1797 {
1798 pToken = (char *)Vec_PtrEntry( vTokens2, iStart + i );
1799 if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, i ) )
1800 return NULL;
1801 }
1802 // output literal
1803 pToken = (char *)Vec_PtrEntry( vTokens2, iStart + nInputs + iOut );
1804 if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
1805 return NULL;
1806 // update the counter
1807 iStart += nInputs + nOutputs;
1808 }
1809 Vec_StrPush( vFunc, '\0' );
1810 return Vec_StrArray( vFunc );
1811}
1812
1824static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
1825{
1826 char Buffer[50];
1827 Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pOutNet;
1828 Io_MvVar_t * pVar;
1829 // make sure the reset latch exists
1830 assert( p->pResetLatch != NULL );
1831 // get the reset net
1832 pResetLONet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch));
1833 // get the output net
1834 pOutNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
1835 // get the data nets
1836 pData0Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_reset") );
1837 pData1Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_out") );
1838 // duplicate MV variables
1839 if ( Abc_NtkMvVar(p->pNtk) )
1840 {
1841 pVar = (Io_MvVar_t *)Abc_ObjMvVar( pOutNet );
1842 Abc_ObjSetMvVar( pData0Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
1843 Abc_ObjSetMvVar( pData1Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
1844 }
1845 // create the node
1846 pNode = Abc_NtkCreateNode( p->pNtk );
1847 // create the output net
1848 Abc_ObjAddFanin( pOutNet, pNode );
1849 // create the function
1850 if ( p->pMan->fBlifMv )
1851 {
1852// Vec_Att_t * p = Abc_NtkMvVar( pNtk );
1853// int nValues = Abc_ObjMvVarNum(pOutNet);
1854// sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
1855 sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
1856 pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, Buffer );
1857 }
1858 else
1859 pNode->pData = Abc_SopCreateMux( (Mem_Flex_t *)p->pNtk->pManFunc );
1860 // add nets
1861 Abc_ObjAddFanin( pNode, pResetLONet );
1862 Abc_ObjAddFanin( pNode, pData1Net );
1863 Abc_ObjAddFanin( pNode, pData0Net );
1864 return pData0Net;
1865}
1866
1878static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Ptr_t * vTokens2, int nInputs, int nOutputs, int iOut, int fReset )
1879{
1880 Abc_Obj_t * pNet, * pNode;
1881 char * pName;
1882 // get the output name
1883 pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + iOut );
1884 // create the node
1885 if ( fReset )
1886 {
1887 pNet = Abc_NtkFindNet( p->pNtk, pName );
1888 if ( pNet == NULL )
1889 {
1890 sprintf( p->pMan->sError, "Line %d: Latch with output signal \"%s\" does not exist.", Io_MvGetLine(p->pMan, pName), pName );
1891 return 0;
1892 }
1893/*
1894 if ( !Abc_ObjIsBo(Abc_ObjFanin0(pNet)) )
1895 {
1896 sprintf( p->pMan->sError, "Line %d: Reset line \"%s\" defines signal that is not a latch output.", Io_MvGetLine(p->pMan, pName), pName );
1897 return 0;
1898 }
1899*/
1900 // construct the reset circuit and get the reset net feeding into it
1901 pNet = Io_MvParseAddResetCircuit( p, pName );
1902 // create fanins
1903 pNode = Io_ReadCreateNode( p->pNtk, Abc_ObjName(pNet), (char **)(vTokens->pArray + 1), nInputs );
1904 assert( nInputs == Vec_PtrSize(vTokens) - 2 );
1905 }
1906 else
1907 {
1908 pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
1909 if ( Abc_ObjFaninNum(pNet) > 0 )
1910 {
1911 sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
1912 return 0;
1913 }
1914 pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), nInputs );
1915 }
1916 // create the cover
1917 pNode->pData = Io_MvParseTableMv( p, pNode, vTokens2, nInputs, nOutputs, iOut );
1918 if ( pNode->pData == NULL )
1919 return 0;
1920 pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
1921//printf( "Finished parsing node \"%s\" with table:\n%s\n", pName, pNode->pData );
1922 return 1;
1923}
1924
1936static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
1937{
1938 Vec_Ptr_t * vTokens = p->pMan->vTokens;
1939 Vec_Ptr_t * vTokens2 = p->pMan->vTokens2;
1940 Abc_Obj_t * pNet;
1941 char * pName, * pFirst, * pArrow;
1942 int nInputs, nOutputs, nLiterals, nLines, i;
1943 assert( p->pMan->fBlifMv );
1944 // get the arrow if it is present
1945 pArrow = Io_MvFindArrow( pLine );
1946 if ( !p->pMan->fBlifMv && pArrow )
1947 {
1948 sprintf( p->pMan->sError, "Line %d: Multi-output node symbol (->) in binary BLIF file.", Io_MvGetLine(p->pMan, pLine) );
1949 return 0;
1950 }
1951 // split names line into tokens
1952 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1953 if ( fReset )
1954 assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "r") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "reset") );
1955 else
1956 assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "table") );
1957 // find the number of inputs and outputs
1958 nInputs = Vec_PtrSize(vTokens) - 2;
1959 nOutputs = 1;
1960 if ( pArrow != NULL )
1961 {
1962 for ( i = Vec_PtrSize(vTokens) - 2; i >= 1; i-- )
1963 if ( pArrow < (char*)Vec_PtrEntry(vTokens,i) )
1964 {
1965 nInputs--;
1966 nOutputs++;
1967 }
1968 }
1969 // split table into tokens
1970 pName = (char *)Vec_PtrEntryLast( vTokens );
1971 Io_MvSplitIntoTokensMv( vTokens2, pName + strlen(pName) );
1972 pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
1973 if ( pFirst[0] == '.' )
1974 {
1975 assert( pFirst[1] == 'd' );
1976 nLiterals = Vec_PtrSize(vTokens2) - 1 - nOutputs;
1977 }
1978 else
1979 nLiterals = Vec_PtrSize(vTokens2);
1980 // check the number of lines
1981 if ( nLiterals % (nInputs + nOutputs) != 0 )
1982 {
1983 sprintf( p->pMan->sError, "Line %d: Wrong number of literals in the table of node \"%s\". (Spaces inside literals are not allowed.)", Io_MvGetLine(p->pMan, pFirst), pName );
1984 return 0;
1985 }
1986 // check for the ND table
1987 nLines = nLiterals / (nInputs + nOutputs);
1988 if ( nInputs == 0 && nLines > 1 )
1989 {
1990 // add the outputs to the PIs
1991 for ( i = 0; i < nOutputs; i++ )
1992 {
1993 pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i );
1994 // get the net corresponding to this node
1995 pNet = Abc_NtkFindOrCreateNet(p->pNtk, pName);
1996 if ( fReset )
1997 {
1998 assert( p->pResetLatch != NULL );
1999 // construct the reset circuit and get the reset net feeding into it
2000 pNet = Io_MvParseAddResetCircuit( p, pName );
2001 }
2002 // add the new PI node
2003// Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) );
2004// fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName );
2005 p->pMan->nNDnodes++;
2007 }
2008 return 1;
2009 }
2010 // iterate through the outputs
2011 for ( i = 0; i < nOutputs; i++ )
2012 {
2013 if ( !Io_MvParseLineNamesMvOne( p, vTokens, vTokens2, nInputs, nOutputs, i, fReset ) )
2014 return 0;
2015 }
2016 return 1;
2017}
2018
2019
2031static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
2032{
2033 Vec_Ptr_t * vTokens = p->pMan->vTokens;
2034 Vec_Str_t * vFunc = p->pMan->vFunc;
2035 char * pProduct, * pOutput, c;
2036 int i, Polarity = -1;
2037
2038 p->pMan->nTablesRead++;
2039 // get the tokens
2040 Io_MvSplitIntoTokens( vTokens, pTable, '.' );
2041 if ( Vec_PtrSize(vTokens) == 0 )
2042 return Abc_SopCreateConst0( (Mem_Flex_t *)p->pNtk->pManFunc );
2043 if ( Vec_PtrSize(vTokens) == 1 )
2044 {
2045 pOutput = (char *)Vec_PtrEntry( vTokens, 0 );
2046 c = pOutput[0];
2047 if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
2048 {
2049 sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
2050 return NULL;
2051 }
2052 return pOutput[0] == '0' ? Abc_SopCreateConst0((Mem_Flex_t *)p->pNtk->pManFunc) : Abc_SopCreateConst1((Mem_Flex_t *)p->pNtk->pManFunc);
2053 }
2054 pProduct = (char *)Vec_PtrEntry( vTokens, 0 );
2055 if ( Vec_PtrSize(vTokens) % 2 == 1 )
2056 {
2057 sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Io_MvGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
2058 return NULL;
2059 }
2060 // parse the table
2061 Vec_StrClear( vFunc );
2062 for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
2063 {
2064 pProduct = (char *)Vec_PtrEntry( vTokens, 2*i + 0 );
2065 pOutput = (char *)Vec_PtrEntry( vTokens, 2*i + 1 );
2066 if ( strlen(pProduct) != (unsigned)nFanins )
2067 {
2068 sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Io_MvGetLine(p->pMan, pProduct), pProduct, nFanins );
2069 return NULL;
2070 }
2071 c = pOutput[0];
2072 if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
2073 {
2074 sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Io_MvGetLine(p->pMan, pProduct), pOutput );
2075 return NULL;
2076 }
2077 if ( Polarity == -1 )
2078 Polarity = (c=='1' || c=='x');
2079 else if ( Polarity != (c=='1' || c=='x') )
2080 {
2081 sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity );
2082 return NULL;
2083 }
2084 // parse one product
2085 Vec_StrPrintStr( vFunc, pProduct );
2086 Vec_StrPush( vFunc, ' ' );
2087 Vec_StrPush( vFunc, pOutput[0] );
2088 Vec_StrPush( vFunc, '\n' );
2089 }
2090 Vec_StrPush( vFunc, '\0' );
2091 return Vec_StrArray( vFunc );
2092}
2093
2105static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
2106{
2107 Vec_Ptr_t * vTokens = p->pMan->vTokens;
2108 Abc_Obj_t * pNet, * pNode;
2109 char * pName;
2110 assert( !p->pMan->fBlifMv );
2111 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
2112 // parse the mapped node
2113 if ( !strcmp((char *)Vec_PtrEntry(vTokens,0), "gate") )
2114 return Io_MvParseLineGateBlif( p, vTokens );
2115 // parse the regular name line
2116 assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") );
2117 pName = (char *)Vec_PtrEntryLast( vTokens );
2118 pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
2119 if ( Abc_ObjFaninNum(pNet) > 0 )
2120 {
2121 sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
2122 return 0;
2123 }
2124 // create fanins
2125 pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), Vec_PtrSize(vTokens) - 2 );
2126 // parse the table of this node
2127 pNode->pData = Io_MvParseTableBlif( p, pName + strlen(pName), Abc_ObjFaninNum(pNode) );
2128 if ( pNode->pData == NULL )
2129 return 0;
2130 pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
2131 return 1;
2132}
2133
2135
2136#include "map/mio/mio.h"
2137#include "base/main/main.h"
2138
2140
2141
2153static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
2154{
2155 Vec_Ptr_t * vTokens = p->pMan->vTokens;
2156 Abc_Obj_t * pNet, * pNode;
2157 char * pName;
2158 assert( !p->pMan->fBlifMv );
2159 Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
2160 if ( Vec_PtrSize(vTokens) != 3 )
2161 {
2162 sprintf( p->pMan->sError, "Line %d: Expecting three entries in the .short line.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
2163 return 0;
2164 }
2165 // parse the regular name line
2166 assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "short") );
2167 pName = (char *)Vec_PtrEntryLast( vTokens );
2168 pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
2169 if ( Abc_ObjFaninNum(pNet) > 0 )
2170 {
2171 sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
2172 return 0;
2173 }
2174 // create fanins
2175 pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), 1 );
2176 // parse the table of this node
2177 if ( p->pNtk->ntkFunc == ABC_FUNC_MAP )
2178 {
2179 Mio_Library_t * pGenlib;
2180 Mio_Gate_t * pGate;
2181 // check that the library is available
2182 pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
2183 if ( pGenlib == NULL )
2184 {
2185 sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
2186 return 0;
2187 }
2188 // get the gate
2189 pGate = Mio_LibraryReadBuf( pGenlib );
2190 if ( pGate == NULL )
2191 {
2192 sprintf( p->pMan->sError, "Line %d: Cannot find buffer gate in the library.", Io_MvGetLine(p->pMan, pName) );
2193 return 0;
2194 }
2195 Abc_ObjSetData( pNode, pGate );
2196 }
2197 else
2198 pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, "1 1\n" );
2199 return 1;
2200}
2201
2213Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
2214{
2215 Mem_Flex_t * pFlex;
2216 Io_MvVar_t * pVarDup;
2217 int i;
2218 if ( pVar == NULL )
2219 return NULL;
2220 pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( pNtk );
2221 assert( pFlex != NULL );
2222 pVarDup = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
2223 pVarDup->nValues = pVar->nValues;
2224 pVarDup->pNames = NULL;
2225 if ( pVar->pNames == NULL )
2226 return pVarDup;
2227 pVarDup->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues );
2228 for ( i = 0; i < pVar->nValues; i++ )
2229 {
2230 pVarDup->pNames[i] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 );
2231 strcpy( pVarDup->pNames[i], pVar->pNames[i] );
2232 }
2233 return pVarDup;
2234}
2235
2247static char * Io_ReadBlifCleanName( char * pName )
2248{
2249 int i, Length;
2250 Length = strlen(pName);
2251 for ( i = 0; i < Length; i++ )
2252 if ( pName[i] == '=' )
2253 return pName + i + 1;
2254 return NULL;
2255}
2256
2268static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
2269{
2270 extern int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_Gate_t * pTwin );
2271 Mio_Library_t * pGenlib;
2272 Mio_Gate_t * pGate;
2273 Abc_Obj_t * pNode;
2274 char ** ppNames, * pName;
2275 int i, nNames;
2276
2277 pName = (char *)vTokens->pArray[0];
2278
2279 // check that the library is available
2280 pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
2281 if ( pGenlib == NULL )
2282 {
2283 sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
2284 return 0;
2285 }
2286
2287 // create a new node and add it to the network
2288 if ( vTokens->nSize < 2 )
2289 {
2290 sprintf( p->pMan->sError, "Line %d: The .gate line has less than two tokens.", Io_MvGetLine(p->pMan, pName) );
2291 return 0;
2292 }
2293
2294 // get the gate
2295 pGate = Mio_LibraryReadGateByName( pGenlib, (char *)vTokens->pArray[1], NULL );
2296 if ( pGate == NULL )
2297 {
2298 sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
2299 return 0;
2300 }
2301
2302 // if this is the first line with gate, update the network type
2303 if ( Abc_NtkNodeNum(p->pNtk) == 0 && p->pNtk->ntkFunc == ABC_FUNC_SOP )
2304 {
2305 assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
2306 p->pNtk->ntkFunc = ABC_FUNC_MAP;
2307 Mem_FlexStop( (Mem_Flex_t *)p->pNtk->pManFunc, 0 );
2308 p->pNtk->pManFunc = pGenlib;
2309 if ( p->pMan && p->pMan->pDesign && Vec_PtrSize(p->pMan->pDesign->vModules) > 0 )
2310 {
2311 Abc_Ntk_t * pModel; int k;
2312 Vec_PtrForEachEntry( Abc_Ntk_t *, p->pMan->pDesign->vModules, pModel, k )
2313 {
2314 if ( pModel == p->pNtk )
2315 continue;
2316 assert( pModel->ntkFunc == ABC_FUNC_SOP );
2317 pModel->ntkFunc = ABC_FUNC_MAP;
2318 Mem_FlexStop( (Mem_Flex_t *)pModel->pManFunc, 0 );
2319 pModel->pManFunc = pGenlib;
2320 }
2321 }
2322 }
2323
2324 // reorder the formal inputs to be in the same order as in the gate
2325 if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate, Mio_GateReadTwin(pGate) ) )
2326 {
2327 sprintf( p->pMan->sError, "Line %d: Mismatch in the fanins of gate \"%s\".", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
2328 return 0;
2329 }
2330
2331 // remove the formal parameter names
2332 for ( i = 2; i < vTokens->nSize; i++ )
2333 {
2334 if ( vTokens->pArray[i] == NULL )
2335 continue;
2336 vTokens->pArray[i] = Io_ReadBlifCleanName( (char *)vTokens->pArray[i] );
2337 if ( vTokens->pArray[i] == NULL )
2338 {
2339 sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) );
2340 return 0;
2341 }
2342 }
2343
2344 // create the node
2345 if ( Mio_GateReadTwin(pGate) == NULL )
2346 {
2347 nNames = vTokens->nSize - 3;
2348 ppNames = (char **)vTokens->pArray + 2;
2349 pNode = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
2350 Abc_ObjSetData( pNode, pGate );
2351 }
2352 else
2353 {
2354 nNames = vTokens->nSize - 4;
2355 ppNames = (char **)vTokens->pArray + 2;
2356 assert( ppNames[nNames] != NULL || ppNames[nNames+1] != NULL );
2357 if ( ppNames[nNames] )
2358 {
2359 pNode = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
2360 Abc_ObjSetData( pNode, pGate );
2361 }
2362 if ( ppNames[nNames+1] )
2363 {
2364 pNode = Io_ReadCreateNode( p->pNtk, ppNames[nNames+1], ppNames, nNames );
2365 Abc_ObjSetData( pNode, Mio_GateReadTwin(pGate) );
2366 }
2367 }
2368
2369 return 1;
2370}
2371
2383static inline void Abc_MapBoxSetPrevNext( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
2384{
2385 Abc_Obj_t * pNode;
2386 pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
2387 Vec_IntWriteEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
2388 pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
2389 Vec_IntWriteEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
2390}
2391static inline int Abc_MapBox2Next( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
2392{
2393 Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
2394 return Vec_IntEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
2395}
2396static inline int Abc_MapBox2Prev( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
2397{
2398 Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
2399 return Vec_IntEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
2400}
2401
2405
2406
2408
void Abc_GenOneHotIntervals(char *pFileName, int nPis, int nRegs, Vec_Ptr_t *vOnehots)
Definition abcGen.c:682
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition abcObj.c:587
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition abcNtk.c:53
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
ABC_DLL int Abc_DesFindTopLevelModels(Abc_Des_t *p)
Definition abcLib.c:293
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition abc.h:520
ABC_DLL int Abc_NtkCheckRead(Abc_Ntk_t *pNtk)
Definition abcCheck.c:80
ABC_DLL void Abc_DesFree(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition abcLib.c:94
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition abc.h:500
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst0(Abc_Ntk_t *pNtk)
Definition abcObj.c:612
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
ABC_DLL char * Abc_SopCreateConst1(Mem_Flex_t *pMan)
Definition abcSop.c:113
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition abcNames.c:69
ABC_DLL void Abc_NtkFinalizeRead(Abc_Ntk_t *pNtk)
Definition abcNtk.c:413
@ ABC_NTK_NETLIST
Definition abc.h:56
ABC_DLL Abc_Des_t * Abc_DesCreate(char *pName)
DECLARATIONS ///.
Definition abcLib.c:45
struct Abc_Des_t_ Abc_Des_t
BASIC TYPES ///.
Definition abc.h:114
ABC_DLL Abc_Ntk_t * Abc_DesFindModelByName(Abc_Des_t *p, char *pName)
Definition abcLib.c:249
ABC_DLL char * Abc_ObjNameSuffix(Abc_Obj_t *pObj, char *pSuffix)
Definition abcNames.c:104
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
ABC_DLL int Abc_DesAddModel(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition abcLib.c:226
@ ABC_FUNC_BLIFMV
Definition abc.h:69
@ ABC_FUNC_BLACKBOX
Definition abc.h:70
@ ABC_FUNC_SOP
Definition abc.h:65
@ ABC_FUNC_MAP
Definition abc.h:68
ABC_DLL int Abc_NtkIsAcyclicHierarchy(Abc_Ntk_t *pNtk)
Definition abcCheck.c:817
ABC_DLL char * Abc_SopCreateConst0(Mem_Flex_t *pMan)
Definition abcSop.c:129
ABC_DLL char * Abc_SopRegister(Mem_Flex_t *pMan, const char *pName)
DECLARATIONS ///.
Definition abcSop.c:62
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition abcObj.c:515
ABC_DLL char * Abc_SopCreateMux(Mem_Flex_t *pMan)
Definition abcSop.c:335
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_DLL void * Abc_FrameReadLibGen()
Definition mainFrame.c:59
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
void BZ_API BZ2_bzReadClose(int *bzerror, BZFILE *b)
Definition bzlib.c:1154
BZFILE *BZ_API BZ2_bzReadOpen(int *bzerror, FILE *f, int verbosity, int small, void *unused, int nUnused)
Definition bzlib.c:1099
int BZ_API BZ2_bzRead(int *bzerror, BZFILE *b, void *buf, int len)
Definition bzlib.c:1173
#define BZ_DATA_ERROR_MAGIC
Definition bzlib.h:43
#define BZ_OK
Definition bzlib.h:34
#define BZ_STREAM_END
Definition bzlib.h:38
void BZFILE
Definition bzlib.h:142
char Char
Cube * p
Definition exorList.c:222
char * Extra_UtilStrsav(const char *s)
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
char * Extra_FileNameGeneric(char *FileName)
ABC_NAMESPACE_IMPL_START int ZEXPORT gzclose(gzFile file)
Definition gzclose.c:18
gzFile ZEXPORT gzopen(const char *path, const char *mode)
Definition gzlib.c:198
int ZEXPORT gzread(gzFile file, voidp buf, unsigned len)
Definition gzread.c:357
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
void Hop_ManStop(Hop_Man_t *p)
Definition hopMan.c:84
Abc_Obj_t * Io_ReadCreateResetLatch(Abc_Ntk_t *pNtk, int fBlifMv)
Definition ioUtil.c:702
Abc_Obj_t * Io_ReadCreatePo(Abc_Ntk_t *pNtk, char *pName)
Definition ioUtil.c:644
Abc_Obj_t * Io_ReadCreatePi(Abc_Ntk_t *pNtk, char *pName)
Definition ioUtil.c:619
Abc_Obj_t * Io_ReadCreateLatch(Abc_Ntk_t *pNtk, char *pNetLI, char *pNetLO)
Definition ioUtil.c:669
Abc_Obj_t * Io_ReadCreateNode(Abc_Ntk_t *pNtk, char *pNameOut, char *pNamesIn[], int nInputs)
Definition ioUtil.c:734
Abc_Ntk_t * Io_ReadBlifMv(char *pFileName, int fBlifMv, int fCheck)
FUNCTION DEFINITIONS ///.
#define IO_BLIFMV_MAXVALUES
DECLARATIONS ///.
Vec_Ptr_t * vGlobalLtlArray
struct Io_MvMod_t_ Io_MvMod_t
struct Io_MvMan_t_ Io_MvMan_t
char * Io_MvLoadFileBz2(char *pFileName, long *pnFileSize)
struct Io_MvVar_t_ Io_MvVar_t
struct buflist buflist
void Io_MvReplaceBuffersByShorts(char *p)
void Abc_NtkStartMvVars(Abc_Ntk_t *pNtk)
DECLARATIONS ///.
Definition abcBlifMv.c:49
int Io_ReadBlifReorderFormalNames(Vec_Ptr_t *vTokens, Mio_Gate_t *pGate, Mio_Gate_t *pTwin)
Definition ioReadBlif.c:561
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
char * Mem_FlexEntryFetch(Mem_Flex_t *p, int nBytes)
Definition mem.c:388
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition mem.c:359
struct Mio_LibraryStruct_t_ Mio_Library_t
Definition mio.h:42
Mio_Gate_t * Mio_GateReadTwin(Mio_Gate_t *pGate)
Definition mioApi.c:176
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition mioApi.c:105
struct Mio_GateStruct_t_ Mio_Gate_t
Definition mio.h:43
Mio_Gate_t * Mio_LibraryReadBuf(Mio_Library_t *pLib)
Definition mioApi.c:49
struct Mem_Flex_t_ Mem_Flex_t
Definition mem.h:34
for(p=first;p->value< newval;p=p->next)
Vec_Ptr_t * vModules
Definition abc.h:225
Vec_Ptr_t * vTops
Definition abc.h:224
void * pManFunc
Definition abc.h:223
char * pName
Definition abc.h:158
Abc_Des_t * pDesign
Definition abc.h:180
int nConstrs
Definition abc.h:173
Abc_Ntk_t * pExdc
Definition abc.h:201
void * pManFunc
Definition abc.h:191
Vec_Ptr_t * vOnehots
Definition abc.h:211
char * pSpec
Definition abc.h:159
Vec_Ptr_t * vLtlProperties
Definition abc.h:169
Abc_NtkFunc_t ntkFunc
Definition abc.h:157
void * pData
Definition abc.h:145
Abc_Obj_t * pNext
Definition abc.h:131
Vec_Ptr_t * vTokens
char * pFileName
Vec_Ptr_t * vModels
char * pBuffer
Vec_Ptr_t * vTokens2
Io_MvMod_t * pLatest
Vec_Str_t * vFunc
Vec_Ptr_t * vLines
char sError[512]
Abc_Des_t * pDesign
Vec_Ptr_t * vResets
Vec_Ptr_t * vSubckts
Vec_Ptr_t * vLatches
Vec_Ptr_t * vInputs
Abc_Obj_t * pResetLatch
Io_MvMan_t * pMan
Vec_Ptr_t * vNames
Vec_Ptr_t * vLtlProperties
Vec_Ptr_t * vShorts
Vec_Ptr_t * vOnehots
Vec_Ptr_t * vOutputs
Vec_Ptr_t * vFlops
Vec_Ptr_t * vConstrs
Vec_Ptr_t * vMvs
Abc_Ntk_t * pNtk
char ** pNames
struct buflist * next
char buf[1<< 20]
#define assert(ex)
Definition util_old.h:213
int strncmp()
char * memcpy()
char * memset()
int strlen()
int strcmp()
char * sprintf()
char * strstr()
char * strcpy()
VOID_HACK rewind()
char * malloc()
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
#define SEEK_END
Definition zconf.h:392
voidp gzFile
Definition zlib.h:1173