ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bblif.c
Go to the documentation of this file.
1
20
21#include <stdio.h>
22#include <stdlib.h>
23#include <string.h>
24#include <assert.h>
25
27#include "bblif.h"
28
30
31
35
36// vector of integers
37typedef struct Vec_Int_t_ Vec_Int_t;
39{
40 int nCap;
41 int nSize;
42 int * pArray;
43};
44
45// vector of characters
46typedef struct Vec_Str_t_ Vec_Str_t;
48{
49 int nCap;
50 int nSize;
51 char * pArray;
52};
53
54// network object
56{
57 int Id; // user ID
58 int Fnc; // functionality
59 unsigned fCi : 1; // combinational input
60 unsigned fCo : 1; // combinational output
61 unsigned fBox : 1; // subcircuit
62 unsigned fMark : 1; // temporary mark
63 unsigned nFanins : 28; // fanin number
64 int pFanins[0]; // fanin array
65};
66
67// object function
68typedef struct Bbl_Fnc_t_ Bbl_Fnc_t;
70{
71 int nWords; // word number
72 int pWords[0]; // word array
73};
74
75// object function
76typedef struct Bbl_Ent_t_ Bbl_Ent_t;
78{
79 int iFunc; // function handle
80 int iNext; // next entry handle
81};
82
83// data manager
85{
86 // data pool
87 Vec_Str_t * pName; // design name
88 Vec_Str_t * pObjs; // vector of objects
89 Vec_Str_t * pFncs; // vector of functions
90 // construction
91 Vec_Int_t * vId2Obj; // mapping user IDs into objects
92 Vec_Int_t * vObj2Id; // mapping objects into user IDs
93 Vec_Int_t * vFaninNums; // mapping user IDs into fanin number
94 // file contents
95 int nFileSize; // file size
96 char * pFileData; // file contents
97 // other data
98 Vec_Str_t * pEnts; // vector of entries
99 int SopMap[17][17]; // mapping vars x cubes into entry handles
100};
101
102static inline int Bbl_ObjIsCi( Bbl_Obj_t * pObj ) { return pObj->fCi; }
103static inline int Bbl_ObjIsCo( Bbl_Obj_t * pObj ) { return pObj->fCo; }
104static inline int Bbl_ObjIsNode( Bbl_Obj_t * pObj ) { return!pObj->fCi && !pObj->fCo; }
105
106static inline int Bbl_ObjFaninNum( Bbl_Obj_t * pObj ) { return pObj->nFanins; }
107static inline Bbl_Obj_t * Bbl_ObjFanin( Bbl_Obj_t * pObj, int i ) { return (Bbl_Obj_t *)(((char *)pObj) - pObj->pFanins[i]); }
108
109static inline int Bbl_ObjSize( Bbl_Obj_t * pObj ) { return sizeof(Bbl_Obj_t) + sizeof(int) * pObj->nFanins; }
110static inline int Bbl_FncSize( Bbl_Fnc_t * pFnc ) { return sizeof(Bbl_Fnc_t) + sizeof(int) * pFnc->nWords; }
111
112static inline Bbl_Obj_t * Bbl_VecObj( Vec_Str_t * p, int h ) { return (Bbl_Obj_t *)(p->pArray + h); }
113static inline Bbl_Fnc_t * Bbl_VecFnc( Vec_Str_t * p, int h ) { return (Bbl_Fnc_t *)(p->pArray + h); }
114static inline Bbl_Ent_t * Bbl_VecEnt( Vec_Str_t * p, int h ) { return (Bbl_Ent_t *)(p->pArray + h); }
115
116static inline char * Bbl_ManSop( Bbl_Man_t * p, int h ) { return (char *)Bbl_VecFnc(p->pFncs, h)->pWords; }
117static inline Bbl_Obj_t * Bbl_ManObj( Bbl_Man_t * p, int Id ) { return Bbl_VecObj(p->pObjs, p->vId2Obj->pArray[Id]); }
118
119#define Bbl_ManForEachObj_int( p, pObj, h ) \
120 for ( h = 0; (h < p->nSize) && (pObj = Bbl_VecObj(p,h)); h += Bbl_ObjSize(pObj) )
121#define Bbl_ManForEachFnc_int( p, pObj, h ) \
122 for ( h = 0; (h < p->nSize) && (pObj = Bbl_VecFnc(p,h)); h += Bbl_FncSize(pObj) )
123#define Bbl_ObjForEachFanin_int( pObj, pFanin, i ) \
124 for ( i = 0; (i < (int)pObj->nFanins) && (pFanin = Bbl_ObjFanin(pObj,i)); i++ )
125
126#define BBLIF_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
127#define BBLIF_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
128#define BBLIF_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
129#define BBLIF_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
130#define BBLIF_REALLOC(type, obj, num) \
131 ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
132 ((type *) malloc(sizeof(type) * (num))))
133
137
149static inline Vec_Int_t * Vec_IntAlloc( int nCap )
150{
151 Vec_Int_t * p;
152 p = BBLIF_ALLOC( Vec_Int_t, 1 );
153 if ( nCap > 0 && nCap < 16 )
154 nCap = 16;
155 p->nSize = 0;
156 p->nCap = nCap;
157 p->pArray = p->nCap? BBLIF_ALLOC( int, p->nCap ) : NULL;
158 return p;
159}
160
172static inline Vec_Int_t * Vec_IntStart( int nSize )
173{
174 Vec_Int_t * p;
175 p = Vec_IntAlloc( nSize );
176 p->nSize = nSize;
177 memset( p->pArray, 0, sizeof(int) * nSize );
178 return p;
179}
180
192static inline Vec_Int_t * Vec_IntStartNatural( int nSize )
193{
194 Vec_Int_t * p;
195 int i;
196 p = Vec_IntAlloc( nSize );
197 p->nSize = nSize;
198 for ( i = 0; i < nSize; i++ )
199 p->pArray[i] = i;
200 return p;
201}
202
214static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
215{
216 Vec_Int_t * p;
217 p = BBLIF_ALLOC( Vec_Int_t, 1 );
218 p->nSize = nSize;
219 p->nCap = nSize;
220 p->pArray = pArray;
221 return p;
222}
223
235static inline void Vec_IntFree( Vec_Int_t * p )
236{
237 BBLIF_FREE( p->pArray );
238 BBLIF_FREE( p );
239}
240
252static inline int Vec_IntSize( Vec_Int_t * p )
253{
254 return p->nSize;
255}
256
268static inline int Vec_IntEntry( Vec_Int_t * p, int i )
269{
270 assert( i >= 0 && i < p->nSize );
271 return p->pArray[i];
272}
273
285static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
286{
287 assert( i >= 0 && i < p->nSize );
288 p->pArray[i] = Entry;
289}
290
302static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
303{
304 assert( i >= 0 && i < p->nSize );
305 p->pArray[i] += Addition;
306}
307
319static inline int Vec_IntEntryLast( Vec_Int_t * p )
320{
321 assert( p->nSize > 0 );
322 return p->pArray[p->nSize-1];
323}
324
336static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
337{
338 if ( p->nCap >= nCapMin )
339 return;
340 p->pArray = BBLIF_REALLOC( int, p->pArray, nCapMin );
341 assert( p->pArray );
342 p->nCap = nCapMin;
343}
344
356static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Fill )
357{
358 int i;
359 Vec_IntGrow( p, nSize );
360 for ( i = 0; i < nSize; i++ )
361 p->pArray[i] = Fill;
362 p->nSize = nSize;
363}
364
376static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Fill )
377{
378 int i;
379 if ( p->nSize >= nSize )
380 return;
381 if ( nSize > 2 * p->nCap )
382 Vec_IntGrow( p, nSize );
383 else if ( nSize > p->nCap )
384 Vec_IntGrow( p, 2 * p->nCap );
385 for ( i = p->nSize; i < nSize; i++ )
386 p->pArray[i] = Fill;
387 p->nSize = nSize;
388}
389
401static inline int Vec_IntGetEntry( Vec_Int_t * p, int i )
402{
403 Vec_IntFillExtra( p, i + 1, 0 );
404 return Vec_IntEntry( p, i );
405}
406
418static inline void Vec_IntSetEntry( Vec_Int_t * p, int i, int Entry )
419{
420 Vec_IntFillExtra( p, i + 1, 0 );
421 Vec_IntWriteEntry( p, i, Entry );
422}
423
435static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
436{
437 assert( p->nSize >= nSizeNew );
438 p->nSize = nSizeNew;
439}
440
452static inline void Vec_IntClear( Vec_Int_t * p )
453{
454 p->nSize = 0;
455}
456
468static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
469{
470 if ( p->nSize == p->nCap )
471 {
472 if ( p->nCap < 16 )
473 Vec_IntGrow( p, 16 );
474 else
475 Vec_IntGrow( p, 2 * p->nCap );
476 }
477 p->pArray[p->nSize++] = Entry;
478}
479
480
481
482
483
495static inline Vec_Str_t * Vec_StrAlloc( int nCap )
496{
497 Vec_Str_t * p;
498 p = BBLIF_ALLOC( Vec_Str_t, 1 );
499 if ( nCap > 0 && nCap < 16 )
500 nCap = 16;
501 p->nSize = 0;
502 p->nCap = nCap;
503 p->pArray = p->nCap? BBLIF_ALLOC( char, p->nCap ) : NULL;
504 return p;
505}
506
518static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
519{
520 Vec_Str_t * p;
521 p = BBLIF_ALLOC( Vec_Str_t, 1 );
522 p->nSize = nSize;
523 p->nCap = nSize;
524 p->pArray = pArray;
525 return p;
526}
527
539char * Vec_StrFetch( Vec_Str_t * p, int nBytes )
540{
541 while ( p->nSize + nBytes > p->nCap )
542 {
543 p->pArray = BBLIF_REALLOC( char, p->pArray, 3 * p->nCap );
544 p->nCap *= 3;
545 }
546 p->nSize += nBytes;
547 return p->pArray + p->nSize - nBytes;
548}
549
561void Vec_StrWrite( FILE * pFile, Vec_Str_t * p )
562{
563 fwrite( &p->nSize, sizeof(int), 1, pFile );
564 fwrite( p->pArray, sizeof(char), p->nSize, pFile );
565}
566
578Vec_Str_t * Vec_StrRead( char ** ppStr )
579{
580 Vec_Str_t * p;
581 char * pStr = *ppStr;
582 p = Vec_StrAlloc( 0 );
583 p->nSize = *(int *)pStr;
584 p->pArray = pStr + sizeof(int);
585 *ppStr = pStr + sizeof(int) + p->nSize * sizeof(char);
586 return p;
587}
588
600static inline int Vec_StrSize( Vec_Str_t * p )
601{
602 return p->nSize;
603}
604
616static inline void Vec_StrFree( Vec_Str_t * p )
617{
618 BBLIF_FREE( p->pArray );
619 BBLIF_FREE( p );
620}
621
622
623
624
625
637int Bbl_ManFileSize( char * pFileName )
638{
639 FILE * pFile;
640 int nFileSize;
641 pFile = fopen( pFileName, "r" );
642 if ( pFile == NULL )
643 {
644 printf( "Bbl_ManFileSize(): The file is unavailable (absent or open).\n" );
645 return 0;
646 }
647 fseek( pFile, 0, SEEK_END );
648 nFileSize = ftell( pFile );
649 fclose( pFile );
650 return nFileSize;
651}
652
664char * Bbl_ManFileRead( char * pFileName )
665{
666 FILE * pFile;
667 char * pContents;
668 int nFileSize;
669 int RetValue;
670 nFileSize = Bbl_ManFileSize( pFileName );
671 pFile = fopen( pFileName, "rb" );
672 pContents = BBLIF_ALLOC( char, nFileSize );
673 RetValue = fread( pContents, nFileSize, 1, pFile );
674 fclose( pFile );
675 return pContents;
676}
677
678
679
691void Bbl_ManDumpBinaryBlif( Bbl_Man_t * p, char * pFileName )
692{
693 FILE * pFile;
694 pFile = fopen( pFileName, "wb" );
695 Vec_StrWrite( pFile, p->pName );
696 Vec_StrWrite( pFile, p->pObjs );
697 Vec_StrWrite( pFile, p->pFncs );
698 fclose( pFile );
699}
700
712Bbl_Man_t * Bbl_ManReadBinaryBlif( char * pFileName )
713{
714 Bbl_Man_t * p;
715 Bbl_Obj_t * pObj;
716 char * pBuffer;
717 int h;
718 p = BBLIF_ALLOC( Bbl_Man_t, 1 );
719 memset( p, 0, sizeof(Bbl_Man_t) );
720 p->nFileSize = Bbl_ManFileSize( pFileName );
721 p->pFileData = Bbl_ManFileRead( pFileName );
722 // extract three managers
723 pBuffer = p->pFileData;
724 p->pName = Vec_StrRead( &pBuffer );
725 p->pObjs = Vec_StrRead( &pBuffer );
726 p->pFncs = Vec_StrRead( &pBuffer );
727 assert( pBuffer - p->pFileData == p->nFileSize );
728 // remember original IDs in the objects
729 p->vObj2Id = Vec_IntAlloc( 1000 );
730 Bbl_ManForEachObj_int( p->pObjs, pObj, h )
731 {
732 Vec_IntPush( p->vObj2Id, pObj->Id );
733 pObj->Id = Vec_IntSize(p->vObj2Id) - 1;
734 }
735 return p;
736}
737
750{
751 Bbl_Obj_t * pObj;
752 Bbl_Fnc_t * pFnc;
753 int h, nFuncs = 0, nNodes = 0, nObjs = 0;
754 Bbl_ManForEachObj_int( p->pObjs, pObj, h )
755 nObjs++, nNodes += Bbl_ObjIsNode(pObj);
756 Bbl_ManForEachFnc_int( p->pFncs, pFnc, h )
757 nFuncs++;
758 printf( "Total objects = %7d. Total nodes = %7d. Unique functions = %7d.\n", nObjs, nNodes, nFuncs );
759 printf( "Name manager = %5.2f MB\n", 1.0*Vec_StrSize(p->pName)/(1 << 20) );
760 printf( "Objs manager = %5.2f MB\n", 1.0*Vec_StrSize(p->pObjs)/(1 << 20) );
761 printf( "Fncs manager = %5.2f MB\n", 1.0*Vec_StrSize(p->pFncs)/(1 << 20) );
762}
763
776{
777 if ( p->vId2Obj ) Vec_IntFree( p->vId2Obj );
778 if ( p->vObj2Id ) Vec_IntFree( p->vObj2Id );
779 if ( p->vFaninNums ) Vec_IntFree( p->vFaninNums );
780 if ( p->pFileData )
781 {
782 BBLIF_FREE( p->pFileData );
783 p->pName->pArray = NULL;
784 p->pObjs->pArray = NULL;
785 p->pFncs->pArray = NULL;
786 }
787 if ( p->pEnts )
788 Vec_StrFree( p->pEnts );
789 Vec_StrFree( p->pName );
790 Vec_StrFree( p->pObjs );
791 Vec_StrFree( p->pFncs );
792 BBLIF_FREE( p );
793}
794
806Bbl_Man_t * Bbl_ManStart( char * pName )
807{
808 Bbl_Man_t * p;
809 int nLength;
810 p = BBLIF_ALLOC( Bbl_Man_t, 1 );
811 memset( p, 0, sizeof(Bbl_Man_t) );
812 nLength = pName? 4 * ((strlen(pName) + 1) / 4 + 1) : 0;
813 p->pName = Vec_StrAlloc( nLength );
814 p->pName->nSize = p->pName->nCap;
815 if ( pName )
816 strcpy( p->pName->pArray, pName );
817 p->pObjs = Vec_StrAlloc( 1 << 16 );
818 p->pFncs = Vec_StrAlloc( 1 << 16 );
819 p->pEnts = Vec_StrAlloc( 1 << 16 ); p->pEnts->nSize = 1;
820 p->vId2Obj = Vec_IntStart( 1 << 10 );
821 p->vFaninNums = Vec_IntStart( 1 << 10 );
822 return p;
823}
824
825
826
827
839void Bbl_ManSortCubes( char ** pCubes, int nCubes, int nVars )
840{
841 char * pTemp;
842 int i, j, best_i;
843 for ( i = 0; i < nCubes-1; i++ )
844 {
845 best_i = i;
846 for (j = i+1; j < nCubes; j++)
847 if ( memcmp( pCubes[j], pCubes[best_i], (size_t)nVars ) < 0 )
848 best_i = j;
849 pTemp = pCubes[i]; pCubes[i] = pCubes[best_i]; pCubes[best_i] = pTemp;
850 }
851}
852
864char * Bbl_ManSortSop( char * pSop, int nVars )
865{
866 char ** pCubes, * pSopNew;
867 int c, Length, nCubes;
868 Length = strlen(pSop);
869 assert( Length % (nVars + 3) == 0 );
870 nCubes = Length / (nVars + 3);
871 if ( nCubes < 2 )
872 {
873 pSopNew = BBLIF_ALLOC( char, Length + 1 );
874 memcpy( pSopNew, pSop, (size_t)(Length + 1) );
875 return pSopNew;
876 }
877 pCubes = BBLIF_ALLOC( char *, nCubes );
878 for ( c = 0; c < nCubes; c++ )
879 pCubes[c] = pSop + c * (nVars + 3);
880 if ( nCubes < 300 )
881 Bbl_ManSortCubes( pCubes, nCubes, nVars );
882 pSopNew = BBLIF_ALLOC( char, Length + 1 );
883 for ( c = 0; c < nCubes; c++ )
884 memcpy( pSopNew + c * (nVars + 3), pCubes[c], (size_t)(nVars + 3) );
885 BBLIF_FREE( pCubes );
886 pSopNew[nCubes * (nVars + 3)] = 0;
887 return pSopNew;
888}
889
901int Bbl_ManCreateEntry( Bbl_Man_t * p, int iFunc, int iNext )
902{
903 Bbl_Ent_t * pEnt;
904 pEnt = (Bbl_Ent_t *)Vec_StrFetch( p->pEnts, 2 * sizeof(int) );
905 pEnt->iFunc = iFunc;
906 pEnt->iNext = iNext;
907 return (char *)pEnt - p->pEnts->pArray;
908}
909
921int Bbl_ManSopCheckUnique( Bbl_Man_t * p, char * pSop, int nVars, int nCubes, int iFunc )
922{
923 Bbl_Fnc_t * pFnc;
924 Bbl_Ent_t * pEnt;
925 int h, Length = strlen(pSop) + 1;
926 int nWords = (Length / 4 + (Length % 4 > 0));
927 if ( nVars > 16 ) nVars = 16;
928 if ( nCubes > 16 ) nCubes = 16;
929// if ( nVars == 16 && nCubes == 16 )
930// return iFunc;
931 for ( h = p->SopMap[nVars][nCubes]; h; h = pEnt->iNext )
932 {
933 pEnt = Bbl_VecEnt( p->pEnts, h );
934 pFnc = Bbl_VecFnc( p->pFncs, pEnt->iFunc );
935 assert( nVars == 16 || nCubes == 16 || pFnc->nWords == nWords );
936 if ( pFnc->nWords == nWords && memcmp( pFnc->pWords, pSop, (size_t)Length ) == 0 )
937 return pEnt->iFunc;
938 }
939 p->SopMap[nVars][nCubes] = Bbl_ManCreateEntry( p, iFunc, p->SopMap[nVars][nCubes] );
940 return iFunc;
941}
942
954int Bbl_ManSaveSop( Bbl_Man_t * p, char * pSop, int nVars )
955{
956 Bbl_Fnc_t * pFnc;
957 char * pSopNew;
958 int iFunc, Length = strlen(pSop) + 1;
959 int nWords = Length / 4 + (Length % 4 > 0);
960 // reorder cubes to semi-canicize SOPs
961 pSopNew = Bbl_ManSortSop( pSop, nVars );
962 // get the candidate location
963 iFunc = Bbl_ManSopCheckUnique( p, pSopNew, nVars, Length / (nVars + 3), Vec_StrSize(p->pFncs) );
964// iFunc = Vec_StrSize(p->pFncs);
965 if ( iFunc == Vec_StrSize(p->pFncs) )
966 { // store this SOP
967 pFnc = (Bbl_Fnc_t *)Vec_StrFetch( p->pFncs, sizeof(Bbl_Fnc_t) + nWords * sizeof(int) );
968 pFnc->pWords[nWords-1] = 0;
969 pFnc->nWords = nWords;
970 strcpy( (char *)pFnc->pWords, pSopNew );
971 assert( iFunc == (char *)pFnc - p->pFncs->pArray );
972 }
973 BBLIF_FREE( pSopNew );
974 return iFunc;
975}
976
988void Bbl_ManCreateObject( Bbl_Man_t * p, Bbl_Type_t Type, int ObjId, int nFanins, char * pSop )
989{
990 Bbl_Obj_t * pObj;
991 if ( Type == BBL_OBJ_CI && nFanins != 0 )
992 {
993 printf( "Attempting to create a combinational input with %d fanins (should be 0).\n", nFanins );
994 return;
995 }
996 if ( Type == BBL_OBJ_CO && nFanins != 1 )
997 {
998 printf( "Attempting to create a combinational output with %d fanins (should be 1).\n", nFanins );
999 return;
1000 }
1001 pObj = (Bbl_Obj_t *)Vec_StrFetch( p->pObjs, sizeof(Bbl_Obj_t) + nFanins * sizeof(int) );
1002 memset( pObj, 0, sizeof(Bbl_Obj_t) );
1003 Vec_IntSetEntry( p->vId2Obj, ObjId, (char *)pObj - p->pObjs->pArray );
1004 Vec_IntSetEntry( p->vFaninNums, ObjId, 0 );
1005 pObj->fCi = (Type == BBL_OBJ_CI);
1006 pObj->fCo = (Type == BBL_OBJ_CO);
1007 pObj->Id = ObjId;
1008 pObj->Fnc = pSop? Bbl_ManSaveSop(p, pSop, nFanins) : -1;
1009 pObj->nFanins = nFanins;
1010}
1011
1023void Bbl_ManAddFanin( Bbl_Man_t * p, int ObjId, int FaninId )
1024{
1025 Bbl_Obj_t * pObj, * pFanin;
1026 int iFanin;
1027 pObj = Bbl_ManObj( p, ObjId );
1028 if ( Bbl_ObjIsCi(pObj) )
1029 {
1030 printf( "Bbl_ManAddFanin(): Cannot add fanin of the combinational input (Id = %d).\n", ObjId );
1031 return;
1032 }
1033 pFanin = Bbl_ManObj( p, FaninId );
1034 if ( Bbl_ObjIsCo(pFanin) )
1035 {
1036 printf( "Bbl_ManAddFanin(): Cannot add fanout of the combinational output (Id = %d).\n", FaninId );
1037 return;
1038 }
1039 iFanin = Vec_IntEntry( p->vFaninNums, ObjId );
1040 if ( iFanin >= (int)pObj->nFanins )
1041 {
1042 printf( "Bbl_ManAddFanin(): Trying to add more fanins to object (Id = %d) than declared (%d).\n", ObjId, pObj->nFanins );
1043 return;
1044 }
1045 assert( iFanin < (int)pObj->nFanins );
1046 Vec_IntWriteEntry( p->vFaninNums, ObjId, iFanin+1 );
1047 pObj->pFanins[iFanin] = (char *)pObj - (char *)pFanin;
1048}
1049
1050
1063{
1064 Bbl_Obj_t * pObj;
1065 int h, RetValue = 1;
1066 Bbl_ManForEachObj_int( p->pObjs, pObj, h )
1067 {
1068 if ( Bbl_ObjIsNode(pObj) && pObj->Fnc == -1 )
1069 RetValue = 0, printf( "Bbl_ManCheck(): Node %d does not have function specified.\n", pObj->Id );
1070 if ( Bbl_ObjIsCi(pObj) && pObj->Fnc != -1 )
1071 RetValue = 0, printf( "Bbl_ManCheck(): CI with %d has function specified.\n", pObj->Id );
1072 if ( Bbl_ObjIsCo(pObj) && pObj->Fnc != -1 )
1073 RetValue = 0, printf( "Bbl_ManCheck(): CO with %d has function specified.\n", pObj->Id );
1074 if ( Vec_IntEntry(p->vFaninNums, pObj->Id) != (int)pObj->nFanins )
1075 RetValue = 0, printf( "Bbl_ManCheck(): Object %d has less fanins (%d) than declared (%d).\n",
1076 pObj->Id, Vec_IntEntry(p->vFaninNums, pObj->Id), pObj->nFanins );
1077 }
1078 return RetValue;
1079}
1080
1081
1093int Bbl_ObjIsInput( Bbl_Obj_t * p ) { return Bbl_ObjIsCi(p); }
1094int Bbl_ObjIsOutput( Bbl_Obj_t * p ) { return Bbl_ObjIsCo(p); }
1095int Bbl_ObjIsLut( Bbl_Obj_t * p ) { return Bbl_ObjIsNode(p); }
1096int Bbl_ObjId( Bbl_Obj_t * p ) { return p->Id; }
1097int Bbl_ObjIdOriginal( Bbl_Man_t * pMan, Bbl_Obj_t * p ) { assert(0); return Vec_IntEntry(pMan->vObj2Id, p->Id); }
1098int Bbl_ObjFaninNumber( Bbl_Obj_t * p ) { return Bbl_ObjFaninNum(p); }
1099char * Bbl_ObjSop( Bbl_Man_t * pMan, Bbl_Obj_t * p ) { return Bbl_ManSop(pMan, p->Fnc); }
1100int Bbl_ObjIsMarked( Bbl_Obj_t * p ) { return p->fMark; }
1101void Bbl_ObjMark( Bbl_Obj_t * p ) { p->fMark = 1; }
1102int Bbl_ObjFncHandle( Bbl_Obj_t * p ) { return p->Fnc; }
1103
1116{
1117 return p->pName->pArray;
1118}
1119
1132{
1133 return p->pFncs->nSize;
1134}
1135
1148{
1149 return Bbl_VecObj( p->pObjs, 0 );
1150}
1151
1164{
1165 char * pNext = (char *)pObj + Bbl_ObjSize(pObj);
1166 char * pEdge = p->pObjs->pArray + p->pObjs->nSize;
1167 return (Bbl_Obj_t *)(pNext < pEdge ? pNext : NULL);
1168}
1169
1182{
1183 return Bbl_ObjFaninNum(p) ? Bbl_ObjFanin( p, 0 ) : NULL;
1184}
1185
1198{
1199 Bbl_Obj_t * pFanin;
1200 int i;
1201 Bbl_ObjForEachFanin_int( p, pFanin, i )
1202 if ( pFanin == pPrev )
1203 break;
1204 return i < Bbl_ObjFaninNum(p) - 1 ? Bbl_ObjFanin( p, i+1 ) : NULL;
1205}
1206
1218void Bbl_ManDumpBlif( Bbl_Man_t * p, char * pFileName )
1219{
1220 FILE * pFile;
1221 Bbl_Obj_t * pObj, * pFanin;
1222 pFile = fopen( pFileName, "w" );
1223 fprintf( pFile, "# Test file written by Bbl_ManDumpBlif() in ABC.\n" );
1224 fprintf( pFile, ".model %s\n", Bbl_ManName(p) );
1225 // write objects
1226 Bbl_ManForEachObj( p, pObj )
1227 {
1228 if ( Bbl_ObjIsInput(pObj) )
1229 fprintf( pFile, ".inputs %d\n", Bbl_ObjId(pObj) );
1230 else if ( Bbl_ObjIsOutput(pObj) )
1231 fprintf( pFile, ".outputs %d\n", Bbl_ObjId(pObj) );
1232 else if ( Bbl_ObjIsLut(pObj) )
1233 {
1234 fprintf( pFile, ".names" );
1235 Bbl_ObjForEachFanin( pObj, pFanin )
1236 fprintf( pFile, " %d", Bbl_ObjId(pFanin) );
1237 fprintf( pFile, " %d\n", Bbl_ObjId(pObj) );
1238 fprintf( pFile, "%s", Bbl_ObjSop(p, pObj) );
1239 }
1240 else assert( 0 );
1241 }
1242 // write output drivers
1243 Bbl_ManForEachObj( p, pObj )
1244 {
1245 if ( !Bbl_ObjIsOutput(pObj) )
1246 continue;
1247 fprintf( pFile, ".names" );
1248 Bbl_ObjForEachFanin( pObj, pFanin )
1249 fprintf( pFile, " %d", Bbl_ObjId(pFanin) );
1250 fprintf( pFile, " %d\n", Bbl_ObjId(pObj) );
1251 fprintf( pFile, "1 1\n" );
1252 }
1253 fprintf( pFile, ".end\n" );
1254 fclose( pFile );
1255}
1256
1273char * Bbl_ManTruthToSop( unsigned * pTruth, int nVars )
1274{
1275 char * pResult, * pTemp;
1276 int nMints, nOnes, b, v;
1277 assert( nVars >= 0 && nVars <= 16 );
1278 nMints = (1 << nVars);
1279 // count the number of ones
1280 nOnes = 0;
1281 for ( b = 0; b < nMints; b++ )
1282 nOnes += ((pTruth[b>>5] >> (b&31)) & 1);
1283 // handle constants
1284 if ( nOnes == 0 || nOnes == nMints )
1285 {
1286 pResult = pTemp = BBLIF_ALLOC( char, nVars + 4 );
1287 for ( v = 0; v < nVars; v++ )
1288 *pTemp++ = '-';
1289 *pTemp++ = ' ';
1290 *pTemp++ = nOnes? '1' : '0';
1291 *pTemp++ = '\n';
1292 *pTemp++ = 0;
1293 assert( pTemp - pResult == nVars + 4 );
1294 return pResult;
1295 }
1296 pResult = pTemp = BBLIF_ALLOC( char, nOnes * (nVars + 3) + 1 );
1297 for ( b = 0; b < nMints; b++ )
1298 {
1299 if ( ((pTruth[b>>5] >> (b&31)) & 1) == 0 )
1300 continue;
1301 for ( v = 0; v < nVars; v++ )
1302 *pTemp++ = ((b >> v) & 1)? '1' : '0';
1303 *pTemp++ = ' ';
1304 *pTemp++ = '1';
1305 *pTemp++ = '\n';
1306 }
1307 *pTemp++ = 0;
1308 assert( pTemp - pResult == nOnes * (nVars + 3) + 1 );
1309 return pResult;
1310}
1311
1323static inline void Bbl_ManSopToTruthElem( int nVars, unsigned ** pVars )
1324{
1325 unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
1326 int i, k, nWords;
1327 nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
1328 for ( i = 0; i < nVars; i++ )
1329 {
1330 if ( i < 5 )
1331 {
1332 for ( k = 0; k < nWords; k++ )
1333 pVars[i][k] = Masks[i];
1334 }
1335 else
1336 {
1337 for ( k = 0; k < nWords; k++ )
1338 if ( k & (1 << (i-5)) )
1339 pVars[i][k] = ~(unsigned)0;
1340 else
1341 pVars[i][k] = 0;
1342 }
1343 }
1344}
1345
1362unsigned * Bbl_ManSopToTruth( char * pSop, int nVars )
1363{
1364 unsigned * pTruth, * pCube, * pVars[16];
1365 int nWords = nVars <= 5 ? 1 : (1 << (nVars - 5));
1366 int v, c, w, nCubes, fCompl = 0;
1367 if ( pSop == NULL )
1368 return NULL;
1369 if ( strlen(pSop) % (nVars + 3) != 0 )
1370 {
1371 printf( "Bbl_ManSopToTruth(): SOP is represented incorrectly.\n" );
1372 return NULL;
1373 }
1374 // create storage for TTs of the result, elementary variables and the temp cube
1375 pTruth = BBLIF_ALLOC( unsigned, nWords );
1376 pVars[0] = BBLIF_ALLOC( unsigned, nWords * (nVars+1) );
1377 for ( v = 1; v < nVars; v++ )
1378 pVars[v] = pVars[v-1] + nWords;
1379 pCube = pVars[v-1] + nWords;
1380 Bbl_ManSopToTruthElem( nVars, pVars );
1381 // iterate through the cubes
1382 memset( pTruth, 0, sizeof(unsigned) * nWords );
1383 nCubes = strlen(pSop) / (nVars + 3);
1384 for ( c = 0; c < nCubes; c++ )
1385 {
1386 fCompl = (pSop[nVars+1] == '0');
1387 memset( pCube, 0xff, sizeof(unsigned) * nWords );
1388 // iterate through the literals of the cube
1389 for ( v = 0; v < nVars; v++ )
1390 if ( pSop[v] == '1' )
1391 for ( w = 0; w < nWords; w++ )
1392 pCube[w] &= pVars[v][w];
1393 else if ( pSop[v] == '0' )
1394 for ( w = 0; w < nWords; w++ )
1395 pCube[w] &= ~pVars[v][w];
1396 // add cube to storage
1397 for ( w = 0; w < nWords; w++ )
1398 pTruth[w] |= pCube[w];
1399 // go to the next cube
1400 pSop += (nVars + 3);
1401 }
1402 BBLIF_FREE( pVars[0] );
1403 if ( fCompl )
1404 for ( w = 0; w < nWords; w++ )
1405 pTruth[w] = ~pTruth[w];
1406 return pTruth;
1407}
1408
1409
1422void Bbl_ManTestTruth( char * pSop, int nVars )
1423{
1424 unsigned * pTruth;
1425 char * pSopNew;
1426 pTruth = Bbl_ManSopToTruth( pSop, nVars );
1427 pSopNew = Bbl_ManTruthToSop( pTruth, nVars );
1428 printf( "Old SOP:\n%s\n", pSop );
1429 printf( "New SOP:\n%s\n", pSopNew );
1430 BBLIF_FREE( pSopNew );
1431 BBLIF_FREE( pTruth );
1432}
1433
1447{
1448/*
1449 # There are contents of a BLIF file representing a half-adder:
1450 .model hadder
1451 .inputs a // ID = 1
1452 .inputs b // ID = 2
1453 .inputs cin // ID = 3
1454 .outputs s // ID = 4
1455 .outputs cout // ID = 5
1456 .names a b cin s_driver // ID = 6
1457 100 1
1458 010 1
1459 001 1
1460 111 1
1461 .names a b cin cout_driver // ID = 7
1462 -11 1
1463 1-1 1
1464 11- 1
1465 .names s_driver s
1466 1 1
1467 .names cout_driver cout
1468 1 1
1469 .end
1470*/
1471 Bbl_Man_t * p;
1472 // start the data manager
1473 p = Bbl_ManStart( "hadder" );
1474 // create CIs
1475 Bbl_ManCreateObject( p, BBL_OBJ_CI, 1, 0, NULL ); // a
1476 Bbl_ManCreateObject( p, BBL_OBJ_CI, 2, 0, NULL ); // b
1477 Bbl_ManCreateObject( p, BBL_OBJ_CI, 3, 0, NULL ); // cin
1478 // create COs
1479 Bbl_ManCreateObject( p, BBL_OBJ_CO, 4, 1, NULL ); // s
1480 Bbl_ManCreateObject( p, BBL_OBJ_CO, 5, 1, NULL ); // cout
1481 // create internal nodes
1482 Bbl_ManCreateObject( p, BBL_OBJ_NODE, 6, 3, "100 1\n010 1\n001 1\n111 1\n" ); // s_driver
1483 Bbl_ManCreateObject( p, BBL_OBJ_NODE, 7, 3, "-11 1\n1-1 1\n11- 1\n" ); // cout_driver
1484 // add fanins of node 6
1485 Bbl_ManAddFanin( p, 6, 1 ); // s_driver <- a
1486 Bbl_ManAddFanin( p, 6, 2 ); // s_driver <- b
1487 Bbl_ManAddFanin( p, 6, 3 ); // s_driver <- cin
1488 // add fanins of node 7
1489 Bbl_ManAddFanin( p, 7, 1 ); // cout_driver <- a
1490 Bbl_ManAddFanin( p, 7, 2 ); // cout_driver <- b
1491 Bbl_ManAddFanin( p, 7, 3 ); // cout_driver <- cin
1492 // add fanins of COs
1493 Bbl_ManAddFanin( p, 4, 6 ); // s <- s_driver
1494 Bbl_ManAddFanin( p, 5, 7 ); // cout <- cout_driver
1495 // sanity check
1496 Bbl_ManCheck( p );
1497 // write BLIF file as a sanity check
1498 Bbl_ManDumpBlif( p, "hadder.blif" );
1499 // write binary BLIF file
1500 Bbl_ManDumpBinaryBlif( p, "hadder.bblif" );
1501 // remove the manager
1502 Bbl_ManStop( p );
1503
1504
1505// Bbl_ManTestTruth( "100 1\n010 1\n001 1\n111 1\n", 3 );
1506// Bbl_ManTestTruth( "-11 0\n1-1 0\n11- 0\n", 3 );
1507// Bbl_ManTestTruth( "--- 1\n", 3 );
1508}
1509
1510
1511
1515
1516
1518
int nWords
Definition abcNpn.c:127
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
int Bbl_ManFileSize(char *pFileName)
Definition bblif.c:637
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
int Bbl_ManFncSize(Bbl_Man_t *p)
Definition bblif.c:1131
int Bbl_ObjFaninNumber(Bbl_Obj_t *p)
Definition bblif.c:1098
struct Bbl_Fnc_t_ Bbl_Fnc_t
Definition bblif.c:68
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
char * Bbl_ManFileRead(char *pFileName)
Definition bblif.c:664
void Bbl_ManAddFanin(Bbl_Man_t *p, int ObjId, int FaninId)
Definition bblif.c:1023
void Bbl_ManDumpBlif(Bbl_Man_t *p, char *pFileName)
Definition bblif.c:1218
#define BBLIF_ALLOC(type, num)
Definition bblif.c:126
unsigned * Bbl_ManSopToTruth(char *pSop, int nVars)
Definition bblif.c:1362
int Bbl_ManSopCheckUnique(Bbl_Man_t *p, char *pSop, int nVars, int nCubes, int iFunc)
Definition bblif.c:921
void Bbl_ManTestTruth(char *pSop, int nVars)
Definition bblif.c:1422
char * Bbl_ManSortSop(char *pSop, int nVars)
Definition bblif.c:864
struct Bbl_Ent_t_ Bbl_Ent_t
Definition bblif.c:76
void Bbl_ManSortCubes(char **pCubes, int nCubes, int nVars)
Definition bblif.c:839
void Vec_StrWrite(FILE *pFile, Vec_Str_t *p)
Definition bblif.c:561
char * Bbl_ManTruthToSop(unsigned *pTruth, int nVars)
Definition bblif.c:1273
int Bbl_ManSaveSop(Bbl_Man_t *p, char *pSop, int nVars)
Definition bblif.c:954
#define Bbl_ManForEachObj_int(p, pObj, h)
Definition bblif.c:119
int Bbl_ObjIsInput(Bbl_Obj_t *p)
Definition bblif.c:1093
char * Bbl_ManName(Bbl_Man_t *p)
Definition bblif.c:1115
Bbl_Obj_t * Bbl_ObjFaninFirst(Bbl_Obj_t *p)
Definition bblif.c:1181
#define Bbl_ObjForEachFanin_int(pObj, pFanin, i)
Definition bblif.c:123
int Bbl_ObjIsLut(Bbl_Obj_t *p)
Definition bblif.c:1095
int Bbl_ObjIsMarked(Bbl_Obj_t *p)
Definition bblif.c:1100
int Bbl_ManCreateEntry(Bbl_Man_t *p, int iFunc, int iNext)
Definition bblif.c:901
int Bbl_ObjIdOriginal(Bbl_Man_t *pMan, Bbl_Obj_t *p)
Definition bblif.c:1097
int Bbl_ObjIsOutput(Bbl_Obj_t *p)
Definition bblif.c:1094
void Bbl_ManSimpleDemo()
Definition bblif.c:1446
int Bbl_ManCheck(Bbl_Man_t *p)
Definition bblif.c:1062
void Bbl_ManPrintStats(Bbl_Man_t *p)
Definition bblif.c:749
int Bbl_ObjFncHandle(Bbl_Obj_t *p)
Definition bblif.c:1102
#define BBLIF_FREE(obj)
Definition bblif.c:129
Bbl_Man_t * Bbl_ManReadBinaryBlif(char *pFileName)
Definition bblif.c:712
#define Bbl_ManForEachFnc_int(p, pObj, h)
Definition bblif.c:121
void Bbl_ManDumpBinaryBlif(Bbl_Man_t *p, char *pFileName)
Definition bblif.c:691
Bbl_Man_t * Bbl_ManStart(char *pName)
MACRO DEFINITIONS ///.
Definition bblif.c:806
#define BBLIF_REALLOC(type, obj, num)
Definition bblif.c:130
char * Bbl_ObjSop(Bbl_Man_t *pMan, Bbl_Obj_t *p)
Definition bblif.c:1099
int Bbl_ObjId(Bbl_Obj_t *p)
Definition bblif.c:1096
Bbl_Obj_t * Bbl_ObjFaninNext(Bbl_Obj_t *p, Bbl_Obj_t *pPrev)
Definition bblif.c:1197
Vec_Str_t * Vec_StrRead(char **ppStr)
Definition bblif.c:578
void Bbl_ObjMark(Bbl_Obj_t *p)
Definition bblif.c:1101
void Bbl_ManCreateObject(Bbl_Man_t *p, Bbl_Type_t Type, int ObjId, int nFanins, char *pSop)
Definition bblif.c:988
Bbl_Obj_t * Bbl_ManObjFirst(Bbl_Man_t *p)
Definition bblif.c:1147
Bbl_Obj_t * Bbl_ManObjNext(Bbl_Man_t *p, Bbl_Obj_t *pObj)
Definition bblif.c:1163
char * Vec_StrFetch(Vec_Str_t *p, int nBytes)
Definition bblif.c:539
void Bbl_ManStop(Bbl_Man_t *p)
Definition bblif.c:775
struct Bbl_Obj_t_ Bbl_Obj_t
Definition bblif.h:216
Bbl_Type_t
INCLUDES ///.
Definition bblif.h:204
@ BBL_OBJ_CI
Definition bblif.h:206
@ BBL_OBJ_NODE
Definition bblif.h:208
@ BBL_OBJ_CO
Definition bblif.h:207
#define Bbl_ObjForEachFanin(pObj, pFanin)
Definition bblif.h:260
struct Bbl_Man_t_ Bbl_Man_t
Definition bblif.h:213
#define Bbl_ManForEachObj(p, pObj)
Definition bblif.h:257
Cube * p
Definition exorList.c:222
int iNext
Definition bblif.c:80
int iFunc
Definition bblif.c:79
int pWords[0]
Definition bblif.c:72
int nWords
Definition bblif.c:71
int nFileSize
Definition bblif.c:95
Vec_Str_t * pFncs
Definition bblif.c:89
Vec_Int_t * vFaninNums
Definition bblif.c:93
Vec_Int_t * vObj2Id
Definition bblif.c:92
Vec_Str_t * pName
Definition bblif.c:87
Vec_Str_t * pObjs
Definition bblif.c:88
char * pFileData
Definition bblif.c:96
Vec_Str_t * pEnts
Definition bblif.c:98
int SopMap[17][17]
Definition bblif.c:99
Vec_Int_t * vId2Obj
Definition bblif.c:91
int Fnc
Definition bblif.c:58
unsigned fCi
Definition bblif.c:59
int Id
Definition bblif.c:57
int pFanins[0]
Definition bblif.c:64
unsigned fMark
Definition bblif.c:62
unsigned fBox
Definition bblif.c:61
unsigned fCo
Definition bblif.c:60
unsigned nFanins
Definition bblif.c:63
int nSize
Definition bblif.c:41
int nCap
Definition bblif.c:40
int * pArray
Definition bblif.c:42
int nCap
Definition bblif.c:49
int nSize
Definition bblif.c:50
char * pArray
Definition bblif.c:51
#define assert(ex)
Definition util_old.h:213
char * memcpy()
char * memset()
int strlen()
int memcmp()
char * strcpy()
#define SEEK_END
Definition zconf.h:392