ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcNpnSave.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "aig/aig/aig.h"
23
25
26
30
31typedef struct Npn_Obj_t_ Npn_Obj_t;
32typedef struct Npn_Man_t_ Npn_Man_t;
33
35{
36 word uTruth; // truth table
37 int Count; // occurrences
38 int iNext; // next entry
39};
41{
42 Npn_Obj_t * pBuffer; // all NPN entries
43 int * pBins; // hash table
44 int nBins; // hash table size
45 int nBufferSize; // buffer size
46 int nEntries; // entry count
47};
48
49static inline Npn_Obj_t * Npn_ManObj( Npn_Man_t * p, int i ) { assert( i < p->nBufferSize ); return i ? p->pBuffer + i : NULL; }
50static inline int Npn_ManObjNum( Npn_Man_t * p, Npn_Obj_t * pObj ) { assert( p->pBuffer < pObj ); return pObj - p->pBuffer; }
51
52static word Truth[8] = {
53 ABC_CONST(0xAAAAAAAAAAAAAAAA),
54 ABC_CONST(0xCCCCCCCCCCCCCCCC),
55 ABC_CONST(0xF0F0F0F0F0F0F0F0),
56 ABC_CONST(0xFF00FF00FF00FF00),
57 ABC_CONST(0xFFFF0000FFFF0000),
58 ABC_CONST(0xFFFFFFFF00000000),
59 ABC_CONST(0x0000000000000000),
60 ABC_CONST(0xFFFFFFFFFFFFFFFF)
61};
62
63static Npn_Man_t * pNpnMan = NULL;
64
68
80void Npn_TruthPermute_rec( char * pStr, int mid, int end )
81{
82 static int count = 0;
83 char * pTemp = Abc_UtilStrsav(pStr);
84 char e;
85 int i;
86 if ( mid == end )
87 {
88 printf( "%03d: %s\n", count++, pTemp );
89 return ;
90 }
91 for ( i = mid; i <= end; i++ )
92 {
93 e = pTemp[mid];
94 pTemp[mid] = pTemp[i];
95 pTemp[i] = e;
96
97 Npn_TruthPermute_rec( pTemp, mid + 1, end );
98
99 e = pTemp[mid];
100 pTemp[mid] = pTemp[i];
101 pTemp[i] = e;
102 }
103 ABC_FREE( pTemp );
104}
105
117static inline int Npn_TruthHasVar( word t, int v )
118{
119 return ((t & Truth[v]) >> (1<<v)) != (t & ~Truth[v]);
120}
121
133static inline int Npn_TruthSupport( word t )
134{
135 int v, Supp = 0;
136 for ( v = 0; v < 6; v++ )
137 if ( Npn_TruthHasVar( t, v ) )
138 Supp |= (1 << v);
139 return Supp;
140}
141
153static inline int Npn_TruthSuppSize( word t, int nVars )
154{
155 int v, nSupp = 0;
156 assert( nVars <= 6 );
157 for ( v = 0; v < nVars; v++ )
158 if ( Npn_TruthHasVar( t, v ) )
159 nSupp++;
160 return nSupp;
161}
162
174static inline int Npn_TruthIsMinBase( word t )
175{
176 int Supp = Npn_TruthSupport(t);
177 return (Supp & (Supp+1)) == 0;
178}
179
191word Npn_TruthPadWord( word uTruth, int nVars )
192{
193 if ( nVars == 6 )
194 return uTruth;
195 if ( nVars <= 5 )
196 uTruth = ((uTruth & ABC_CONST(0x00000000FFFFFFFF)) << 32) | (uTruth & ABC_CONST(0x00000000FFFFFFFF));
197 if ( nVars <= 4 )
198 uTruth = ((uTruth & ABC_CONST(0x0000FFFF0000FFFF)) << 16) | (uTruth & ABC_CONST(0x0000FFFF0000FFFF));
199 if ( nVars <= 3 )
200 uTruth = ((uTruth & ABC_CONST(0x00FF00FF00FF00FF)) << 8) | (uTruth & ABC_CONST(0x00FF00FF00FF00FF));
201 if ( nVars <= 2 )
202 uTruth = ((uTruth & ABC_CONST(0x0F0F0F0F0F0F0F0F)) << 4) | (uTruth & ABC_CONST(0x0F0F0F0F0F0F0F0F));
203 if ( nVars <= 1 )
204 uTruth = ((uTruth & ABC_CONST(0x3333333333333333)) << 2) | (uTruth & ABC_CONST(0x3333333333333333));
205 if ( nVars == 0 )
206 uTruth = ((uTruth & ABC_CONST(0x5555555555555555)) << 1) | (uTruth & ABC_CONST(0x5555555555555555));
207 return uTruth;
208}
209
221static inline int Npn_TruthCountOnes( word t )
222{
223 t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
224 t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
225 t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
226 t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
227 t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
228 return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
229}
230
242static inline word Npn_TruthChangePhase( word t, int v )
243{
244 return ((t & Truth[v]) >> (1<<v)) | ((t & ~Truth[v]) << (1<<v));
245}
246
258static inline word Npn_TruthSwapAdjacentVars( word t, int v )
259{
260 static word PMasks[5][3] = {
261 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
262 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
263 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
264 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
265 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
266 };
267 assert( v < 6 );
268 return (t & PMasks[v][0]) | ((t & PMasks[v][1]) << (1 << v)) | ((t & PMasks[v][2]) >> (1 << v));
269}
270
282static inline word Npn_TruthCanon( word t, int nVars, int * pPhase )
283{
284 int fUsePolarity = 0;
285 int fUsePermutation = 0;
286 char Temp, pSigs[13], pCanonPerm[6];
287 int v, fChange, CanonPhase = 0;
288 assert( nVars < 7 );
289 pSigs[12] = Npn_TruthCountOnes( t );
290 if ( pSigs[12] > 32 )
291 {
292 t = ~t;
293 pSigs[12] = 64 - pSigs[12];
294 CanonPhase |= (1 << 6);
295 }
296 if ( fUsePolarity || fUsePermutation )
297 {
298 for ( v = 0; v < nVars; v++ )
299 {
300 pCanonPerm[v] = v;
301 pSigs[2*v+1] = Npn_TruthCountOnes( t & Truth[v] );
302 pSigs[2*v] = pSigs[12] - pSigs[2*v+1];
303 }
304 }
305 if ( fUsePolarity )
306 {
307 for ( v = 0; v < nVars; v++ )
308 {
309 if ( pSigs[2*v] >= pSigs[2*v+1] )
310 continue;
311 CanonPhase |= (1 << v);
312 Temp = pSigs[2*v];
313 pSigs[2*v] = pSigs[2*v+1];
314 pSigs[2*v+1] = Temp;
315 t = Npn_TruthChangePhase( t, v );
316 }
317 }
318 if ( fUsePermutation )
319 {
320 do {
321 fChange = 0;
322 for ( v = 0; v < nVars-1; v++ )
323 {
324 if ( fUsePolarity )
325 {
326 if ( pSigs[2*v] >= pSigs[2*(v+1)] )
327 continue;
328 }
329 else
330 {
331 if ( Abc_MinInt(pSigs[2*v],pSigs[2*v+1]) >= Abc_MinInt(pSigs[2*(v+1)],pSigs[2*(v+1)+1]) )
332 continue;
333 }
334 fChange = 1;
335
336 Temp = pCanonPerm[v];
337 pCanonPerm[v] = pCanonPerm[v+1];
338 pCanonPerm[v+1] = Temp;
339
340 Temp = pSigs[2*v];
341 pSigs[2*v] = pSigs[2*(v+1)];
342 pSigs[2*(v+1)] = Temp;
343
344 Temp = pSigs[2*v+1];
345 pSigs[2*v+1] = pSigs[2*(v+1)+1];
346 pSigs[2*(v+1)+1] = Temp;
347
348 t = Npn_TruthSwapAdjacentVars( t, v );
349 }
350 } while ( fChange );
351 }
352 if ( pPhase )
353 {
354 *pPhase = 0;
355 for ( v = 0; v < nVars; v++ )
356 *pPhase |= (pCanonPerm[v] << (4 * v));
357 *pPhase |= (CanonPhase << 24);
358 }
359 return t;
360}
361
362
374static inline int Npn_ManHash( Npn_Man_t * p, word uTruth )
375{
376 word Key = (uTruth * (word)101) ^ (uTruth * (word)733) ^ (uTruth * (word)1777);
377 return (int)(Key % (word)p->nBins);
378}
379
392{
393 Npn_Obj_t * pEntry, * pNext;
394 int * pBinsOld, * ppPlace;
395 int nBinsOld, Counter, i;
396 abctime clk;
397 assert( p->pBins != NULL );
398clk = Abc_Clock();
399 // save the old Bins
400 pBinsOld = p->pBins;
401 nBinsOld = p->nBins;
402 // get the new Bins
403 p->nBins = Abc_PrimeCudd( 3 * nBinsOld );
404 p->pBins = ABC_CALLOC( int, p->nBins );
405 // rehash the entries from the old table
406 Counter = 1;
407 for ( i = 0; i < nBinsOld; i++ )
408 for ( pEntry = Npn_ManObj(p, pBinsOld[i]),
409 pNext = pEntry ? Npn_ManObj(p, pEntry->iNext) : NULL;
410 pEntry;
411 pEntry = pNext,
412 pNext = pEntry ? Npn_ManObj(p, pEntry->iNext) : NULL )
413 {
414 // get the place where this entry goes
415 ppPlace = p->pBins + Npn_ManHash( p, pEntry->uTruth );
416 // add the entry to the list
417 pEntry->iNext = *ppPlace;
418 *ppPlace = Npn_ManObjNum( p, pEntry );
419 Counter++;
420 }
421 assert( Counter == p->nEntries );
422 ABC_FREE( pBinsOld );
423//ABC_PRT( "Hash table resizing time", Abc_Clock() - clk );
424}
425
438{
439 Npn_Obj_t * pEntry;
440 int * pPlace, Key = Npn_ManHash( p, uTruth );
441 // resize the link storage if needed
442 if ( p->nEntries == p->nBufferSize )
443 {
444 p->nBufferSize *= 2;
445 p->pBuffer = ABC_REALLOC( Npn_Obj_t, p->pBuffer, p->nBufferSize );
446 }
447 // find the entry
448 for ( pEntry = Npn_ManObj(p, p->pBins[Key]),
449 pPlace = p->pBins + Key;
450 pEntry;
451 pPlace = &pEntry->iNext,
452 pEntry = Npn_ManObj(p, pEntry->iNext) )
453 if ( pEntry->uTruth == uTruth )
454 {
455 pEntry->Count++;
456 return pEntry;
457 }
458 // create new entry
459 *pPlace = p->nEntries;
460 assert( p->nEntries < p->nBufferSize );
461 pEntry = Npn_ManObj( p, p->nEntries++ );
462 pEntry->uTruth = uTruth;
463 pEntry->Count = 1;
464 pEntry->iNext = 0;
465 // resize the table if needed
466 if ( p->nEntries > 3 * p->nBins )
467 Npn_ManResize( p );
468 return pEntry;
469}
470
482void Npn_ManRead( Npn_Man_t * p, char * pFileName )
483{
484 char pBuffer[1000];
485 char * pToken;
486 Npn_Obj_t * pEntry;
487 unsigned Truth[2];
488 word uTruth;
489 FILE * pFile = fopen( pFileName, "r" );
490 if ( pFile == NULL )
491 {
492 Abc_Print( -1, "Cannot open NPN function file \"%s\".\n", pFileName );
493 return;
494 }
495 // read lines from the file
496 while ( fgets( pBuffer, 1000, pFile ) != NULL )
497 {
498 pToken = strtok( pBuffer, " \t\n" );
499 if ( pToken == NULL )
500 continue;
501 if ( pToken[0] == '#' )
502 continue;
503 if ( strlen(pToken) != 16 )
504 {
505 Abc_Print( 0, "Skipping token %s that does not look like a 16-digit hex number.\n" );
506 continue;
507 }
508 // extract truth table
509 Extra_ReadHexadecimal( Truth, pToken, 6 );
510 uTruth = (((word)Truth[1]) << 32) | (word)Truth[0];
511 // add truth table
512 pEntry = Npn_ManAdd( p, uTruth );
513 assert( pEntry->Count == 1 );
514 // read area
515 pToken = strtok( NULL, " \t\n" );
516 pEntry->Count = atoi(pToken);
517 }
518 fclose( pFile );
519}
520
532static int Npn_ManCompareEntries( Npn_Obj_t ** pp1, Npn_Obj_t ** pp2 )
533{
534 if ( (*pp1)->Count > (*pp2)->Count )
535 return -1;
536 if ( (*pp1)->Count < (*pp2)->Count )
537 return 1;
538 return 0;
539}
540
552void Npn_ManWrite( Npn_Man_t * p, char * pFileName )
553{
554 Vec_Ptr_t * vEntries;
555 Npn_Obj_t * pEntry;
556 FILE * pFile = fopen( pFileName, "w" );
557 int i;
558 if ( pFile == NULL )
559 {
560 Abc_Print( -1, "Cannot open NPN function file \"%s\".\n", pFileName );
561 return;
562 }
563 vEntries = Vec_PtrAlloc( p->nEntries );
564 for ( i = 0; i < p->nBins; i++ )
565 for ( pEntry = Npn_ManObj(p, p->pBins[i]); pEntry; pEntry = Npn_ManObj(p, pEntry->iNext) )
566 Vec_PtrPush( vEntries, pEntry );
567 Vec_PtrSort( vEntries, (int (*)(const void *, const void *))Npn_ManCompareEntries );
568 Vec_PtrForEachEntry( Npn_Obj_t *, vEntries, pEntry, i )
569 {
570 Extra_PrintHexadecimal( pFile, (unsigned *)&pEntry->uTruth, 6 );
571 fprintf( pFile, " %d %d\n", pEntry->Count, Npn_TruthSuppSize(pEntry->uTruth, 6) );
572 }
573 fclose( pFile );
574 Vec_PtrFree( vEntries );
575}
576
588Npn_Man_t * Npn_ManStart( char * pFileName )
589{
590 Npn_Man_t * p;
591 p = ABC_CALLOC( Npn_Man_t, 1 );
592 if ( pFileName == NULL )
593 {
594 p->nBufferSize = 1000000;
595 p->nBufferSize = 100;
596 p->pBuffer = ABC_ALLOC( Npn_Obj_t, p->nBufferSize );
597 p->nBins = Abc_PrimeCudd( p->nBufferSize / 2 );
598 p->pBins = ABC_CALLOC( int, p->nBins );
599 p->nEntries = 1;
600 }
601 else
602 {
603 FILE * pFile = fopen( pFileName, "r" );
604 if ( pFile == NULL )
605 {
606 Abc_Print( -1, "Cannot open NPN function file \"%s\".\n", pFileName );
607 return NULL;
608 }
609 fclose( pFile );
610 p->nBufferSize = 4 * ( Extra_FileSize(pFileName) / 20 );
611 p->pBuffer = ABC_ALLOC( Npn_Obj_t, p->nBufferSize );
612 p->nBins = Abc_PrimeCudd( p->nBufferSize / 2 );
613 p->pBins = ABC_CALLOC( int, p->nBins );
614 p->nEntries = 1;
615 Npn_ManRead( p, pFileName );
616 }
617 return p;
618}
619
632{
633 ABC_FREE( p->pBuffer );
634 ABC_FREE( p->pBins );
635 ABC_FREE( p );
636}
637
650{
651 if ( pNpnMan != NULL )
652 {
653 Npn_ManStop( pNpnMan );
654 pNpnMan = NULL;
655 }
656}
657
669void Npn_ManLoad( char * pFileName )
670{
671// Npn_TruthPermute_rec( "012345", 0, 5 );
672 if ( pNpnMan != NULL )
673 {
674 Abc_Print( 1, "Removing old table with %d entries.\n", pNpnMan->nEntries );
675 Npn_ManStop( pNpnMan );
676 }
677 pNpnMan = Npn_ManStart( pFileName );
678 Abc_Print( 1, "Created new table with %d entries from file \"%s\".\n", pNpnMan->nEntries, pFileName );
679}
680
692void Npn_ManSave( char * pFileName )
693{
694 if ( pNpnMan == NULL )
695 {
696 Abc_Print( 1, "There is no table with entries.\n" );
697 return;
698 }
699 Npn_ManWrite( pNpnMan, pFileName );
700 Abc_Print( 1, "Dumped table with %d entries from file \"%s\".\n", pNpnMan->nEntries, pFileName );
701}
702
714void Npn_ManSaveOne( unsigned * puTruth, int nVars )
715{
716 word uTruth = (((word)puTruth[1]) << 32) | (word)puTruth[0];
717 assert( nVars >= 0 && nVars <= 6 );
718 if ( pNpnMan == NULL )
719 {
720 Abc_Print( 1, "Creating new table with 0 entries.\n" );
721 pNpnMan = Npn_ManStart( NULL );
722 }
723 // skip truth tables that do not depend on some vars
724 if ( !Npn_TruthIsMinBase( uTruth ) )
725 return;
726 // extend truth table to look like 6-input
727 uTruth = Npn_TruthPadWord( uTruth, nVars );
728 // semi(!)-NPN-canonize the truth table
729 uTruth = Npn_TruthCanon( uTruth, 6, NULL );
730 // add to storage
731 Npn_ManAdd( pNpnMan, uTruth );
732}
733
737
738
740
void Npn_ManRead(Npn_Man_t *p, char *pFileName)
Definition abcNpnSave.c:482
void Npn_TruthPermute_rec(char *pStr, int mid, int end)
FUNCTION DEFINITIONS ///.
Definition abcNpnSave.c:80
void Npn_ManClean()
Definition abcNpnSave.c:649
void Npn_ManSave(char *pFileName)
Definition abcNpnSave.c:692
void Npn_ManSaveOne(unsigned *puTruth, int nVars)
Definition abcNpnSave.c:714
Npn_Obj_t * Npn_ManAdd(Npn_Man_t *p, word uTruth)
Definition abcNpnSave.c:437
struct Npn_Man_t_ Npn_Man_t
Definition abcNpnSave.c:32
word Npn_TruthPadWord(word uTruth, int nVars)
Definition abcNpnSave.c:191
void Npn_ManLoad(char *pFileName)
Definition abcNpnSave.c:669
void Npn_ManWrite(Npn_Man_t *p, char *pFileName)
Definition abcNpnSave.c:552
void Npn_ManResize(Npn_Man_t *p)
Definition abcNpnSave.c:391
typedefABC_NAMESPACE_IMPL_START struct Npn_Obj_t_ Npn_Obj_t
DECLARATIONS ///.
Definition abcNpnSave.c:31
void Npn_ManStop(Npn_Man_t *p)
Definition abcNpnSave.c:631
Npn_Man_t * Npn_ManStart(char *pFileName)
Definition abcNpnSave.c:588
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
int Extra_FileSize(char *pFileName)
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
void Extra_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
int nBufferSize
Definition abcNpnSave.c:45
Npn_Obj_t * pBuffer
Definition abcNpnSave.c:42
int * pBins
Definition abcNpnSave.c:43
word uTruth
Definition abcNpnSave.c:36
#define assert(ex)
Definition util_old.h:213
int strlen()
char * strtok()
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