ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcNpn.c
Go to the documentation of this file.
1
20
21#include "misc/extra/extra.h"
22#include "misc/vec/vec.h"
23
24#include "bool/kit/kit.h"
25#include "bool/lucky/lucky.h"
26#include "opt/dau/dau.h"
27
29
30
34
35// semi-canonical form types
36// 0 - none
37// 1 - based on counting 1s in cofactors
38// 2 - based on minimum truth table value
39// 3 - exact NPN
40
41// data-structure to store a bunch of truth tables
42typedef struct Abc_TtStore_t_ Abc_TtStore_t;
43struct Abc_TtStore_t_
44{
45 int nVars;
46 int nWords;
47 int nFuncs;
48 word ** pFuncs;
49};
50
51extern Abc_TtStore_t * Abc_TtStoreLoad( char * pFileName, int nVarNum );
52extern void Abc_TtStoreFree( Abc_TtStore_t * p, int nVarNum );
53extern void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p, int fBinary );
54
58
70// returns hash key of the truth table
71static inline int Abc_TruthHashKey( word * pFunc, int nWords, int nTableSize )
72{
73 static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
74 int w;
75 word Key = 0;
76 for ( w = 0; w < nWords; w++ )
77 Key += pFunc[w] * s_BigPrimes[w % 7];
78 return (int)(Key % nTableSize);
79}
80// returns 1 if the entry with this truth table exits
81static inline int Abc_TruthHashLookup( word ** pFuncs, int iThis, int nWords, int * pTable, int * pNexts, int Key )
82{
83 int iThat;
84 for ( iThat = pTable[Key]; iThat != -1; iThat = pNexts[iThat] )
85 if ( !memcmp( pFuncs[iThat], pFuncs[iThis], sizeof(word) * nWords ) )
86 return 1;
87 return 0;
88}
89// hashes truth tables and collects unique ones
91{
92 // allocate hash table
93 int nTableSize = Abc_PrimeCudd(p->nFuncs);
94 int * pTable = ABC_FALLOC( int, nTableSize );
95 int * pNexts = ABC_FALLOC( int, nTableSize );
96 // hash functions
97 int i, k, Key;
98 for ( i = 0; i < p->nFuncs; i++ )
99 {
100 Key = Abc_TruthHashKey( p->pFuncs[i], p->nWords, nTableSize );
101 if ( Abc_TruthHashLookup( p->pFuncs, i, p->nWords, pTable, pNexts, Key ) ) // found equal
102 p->pFuncs[i] = NULL;
103 else // there is no equal (the first time this one occurs so far)
104 pNexts[i] = pTable[Key], pTable[Key] = i;
105 }
106 ABC_FREE( pTable );
107 ABC_FREE( pNexts );
108 // count the number of unqiue functions
109 assert( p->pFuncs[0] != NULL );
110 for ( i = k = 1; i < p->nFuncs; i++ )
111 if ( p->pFuncs[i] != NULL )
112 p->pFuncs[k++] = p->pFuncs[i];
113 return (p->nFuncs = k);
114}
115
127int nWords = 0; // unfortunate global variable
128int Abc_TruthCompare( word ** p1, word ** p2 ) { return memcmp(*p1, *p2, sizeof(word) * nWords); }
130{
131 int i, k;
132 // sort them by value
133 nWords = p->nWords;
134 assert( nWords > 0 );
135 qsort( (void *)p->pFuncs, (size_t)p->nFuncs, sizeof(word *), (int(*)(const void *,const void *))Abc_TruthCompare );
136 // count the number of unqiue functions
137 for ( i = k = 1; i < p->nFuncs; i++ )
138 if ( memcmp( p->pFuncs[i-1], p->pFuncs[i], sizeof(word) * nWords ) )
139 p->pFuncs[k++] = p->pFuncs[i];
140 return (p->nFuncs = k);
141}
142
154void Abc_TruthNpnPrint( char * pCanonPermInit, unsigned uCanonPhase, int nVars )
155{
156 char pCanonPerm[16]; int i;
157 assert( nVars <= 16 );
158 for ( i = 0; i < nVars; i++ )
159 pCanonPerm[i] = pCanonPermInit ? pCanonPermInit[i] : 'a' + i;
160 printf( " %c = ( ", Abc_InfoHasBit(&uCanonPhase, nVars) ? 'Z':'z' );
161 for ( i = 0; i < nVars; i++ )
162 printf( "%c%s", pCanonPerm[i] + ('A'-'a') * Abc_InfoHasBit(&uCanonPhase, pCanonPerm[i]-'a'), i == nVars-1 ? "":"," );
163 printf( " ) " );
164}
165
177void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
178{
179 unsigned pAux[2048];
180 word pAuxWord[1024], pAuxWord1[1024];
181 char pCanonPerm[16];
182 unsigned uCanonPhase=0;
183 abctime clk = Abc_Clock();
184 int i;
185
186 char * pAlgoName = NULL;
187 if ( NpnType == 0 )
188 pAlgoName = "uniqifying ";
189 else if ( NpnType == 1 )
190 pAlgoName = "exact NPN ";
191 else if ( NpnType == 2 )
192 pAlgoName = "counting 1s ";
193 else if ( NpnType == 3 )
194 pAlgoName = "Jake's hybrid fast ";
195 else if ( NpnType == 4 )
196 pAlgoName = "Jake's hybrid good ";
197 else if ( NpnType == 5 )
198 pAlgoName = "new hybrid fast ";
199 else if ( NpnType == 6 )
200 pAlgoName = "new phase flipping ";
201 else if ( NpnType == 7 )
202 pAlgoName = "new hier. matching ";
203 else if ( NpnType == 8 )
204 pAlgoName = "new adap. matching ";
205 else if ( NpnType == 9 )
206 pAlgoName = "adjustable algorithm (heuristic) ";
207 else if ( NpnType == 10 )
208 pAlgoName = "adjustable algorithm (exact) ";
209 else if ( NpnType == 11 )
210 pAlgoName = "new cost-aware exact algorithm ";
211 else if ( NpnType == 12 )
212 pAlgoName = "new hybrid fast (P) ";
213
214 assert( p->nVars <= 16 );
215 if ( pAlgoName )
216 printf( "Applying %-20s to %8d func%s of %2d vars... ",
217 pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
218 if ( fVerbose )
219 printf( "\n" );
220
221 if ( NpnType == 0 )
222 {
223 for ( i = 0; i < p->nFuncs; i++ )
224 {
225 if ( fVerbose )
226 printf( "%7d : ", i );
227 if ( fVerbose )
228 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
229 }
230 }
231 else if ( NpnType == 1 )
232 {
233 permInfo* pi;
235 pi = setPermInfoPtr(p->nVars);
236 for ( i = 0; i < p->nFuncs; i++ )
237 {
238 if ( fVerbose )
239 printf( "%7d : ", i );
240 simpleMinimal(p->pFuncs[i], pAuxWord, pAuxWord1, pi, p->nVars);
241 if ( fVerbose )
242 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
243 }
244 freePermInfoPtr(pi);
245 }
246 else if ( NpnType == 2 )
247 {
248 for ( i = 0; i < p->nFuncs; i++ )
249 {
250 if ( fVerbose )
251 printf( "%7d : ", i );
252 resetPCanonPermArray(pCanonPerm, p->nVars);
253 uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
254 if ( fVerbose )
255 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
256 }
257 }
258 else if ( NpnType == 3 )
259 {
260 for ( i = 0; i < p->nFuncs; i++ )
261 {
262 if ( fVerbose )
263 printf( "%7d : ", i );
264 resetPCanonPermArray(pCanonPerm, p->nVars);
265 uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
266 if ( fVerbose )
267 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
268 }
269 }
270 else if ( NpnType == 4 )
271 {
272 for ( i = 0; i < p->nFuncs; i++ )
273 {
274 if ( fVerbose )
275 printf( "%7d : ", i );
276 resetPCanonPermArray(pCanonPerm, p->nVars);
277 uCanonPhase = luckyCanonicizer_final_fast1( p->pFuncs[i], p->nVars, pCanonPerm );
278 if ( fVerbose )
279 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
280 }
281 }
282 else if ( NpnType == 5 )
283 {
284 for ( i = 0; i < p->nFuncs; i++ )
285 {
286 if ( fVerbose )
287 printf( "%7d : ", i );
288 uCanonPhase = Abc_TtCanonicize( p->pFuncs[i], p->nVars, pCanonPerm );
289 if ( fVerbose )
290 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
291 }
292 }
293 else if ( NpnType == 6 )
294 {
295 for ( i = 0; i < p->nFuncs; i++ )
296 {
297 if ( fVerbose )
298 printf( "%7d : ", i );
299 uCanonPhase = Abc_TtCanonicizePhase( p->pFuncs[i], p->nVars );
300 if ( fVerbose )
301 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
302 }
303 }
304 else if ( NpnType == 7 )
305 {
306 int fExact = 0;
307 Abc_TtHieMan_t * pMan = Abc_TtHieManStart( p->nVars, 5 );
308 for ( i = 0; i < p->nFuncs; i++ )
309 {
310 if ( fVerbose )
311 printf( "%7d : ", i );
312 uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm, fExact );
313 if ( fVerbose )
314// Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
315 printf( "\n" );
316 }
317 // nClasses = Abc_TtManNumClasses( pMan );
318 Abc_TtHieManStop( pMan );
319 }
320 else if ( NpnType == 8 )
321 {
322// typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
323 unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
324 unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
325
326 int fHigh = 1, iEnumThres = 25;
327 Abc_TtHieMan_t * pMan = Abc_TtHieManStart(p->nVars, 5);
328 for ( i = 0; i < p->nFuncs; i++ )
329 {
330 if ( fVerbose )
331 printf( "%7d : ", i );
332 uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm, fHigh*100 + iEnumThres);
333 if ( fVerbose )
334 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
335 }
336 Abc_TtHieManStop(pMan);
337 }
338 else if ( NpnType == 9 || NpnType == 10 || NpnType == 11 )
339 {
340// typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
341 unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
342 unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
343 unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
344
345 Abc_TtHieMan_t * pMan = Abc_TtHieManStart(p->nVars, 5);
346 for ( i = 0; i < p->nFuncs; i++ )
347 {
348 if ( fVerbose )
349 printf( "%7d : ", i );
350 if ( NpnType == 9 )
351 uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm, 125); // -A 8, adjustable algorithm (heuristic)
352 else if ( NpnType == 10 )
353 uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeAda, pMan, p->pFuncs[i], p->nVars, pCanonPerm, 1199); // -A 9, adjustable algorithm (exact)
354 else if ( NpnType == 11 )
355 uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeCA, pMan, p->pFuncs[i], p->nVars, pCanonPerm, 1); // -A 10, new cost-aware exact algorithm
356 if ( fVerbose )
357 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
358 }
359 Abc_TtHieManStop(pMan);
360 }
361 else if ( NpnType == 12 )
362 {
363 for ( i = 0; i < p->nFuncs; i++ )
364 {
365 if ( fVerbose )
366 printf( "%7d : ", i );
367 uCanonPhase = Abc_TtCanonicizePerm( p->pFuncs[i], p->nVars, pCanonPerm );
368 if ( fVerbose )
369 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
370 }
371 }
372 else assert( 0 );
373 clk = Abc_Clock() - clk;
374 printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
375 Abc_PrintTime( 1, "Time", clk );
376}
377
389void Abc_TruthNpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose )
390{
392 char * pFileNameOut;
393
394 // read info from file
395 p = Abc_TtStoreLoad( pFileName, nVarNum );
396 if ( p == NULL )
397 return;
398
399 // consider functions from the file
400 Abc_TruthNpnPerform( p, NpnType, fVerbose );
401
402 // write the result
403 if ( fDumpRes )
404 {
405 if ( fBinary )
406 pFileNameOut = Extra_FileNameGenericAppend( pFileName, "_out.tt" );
407 else
408 pFileNameOut = Extra_FileNameGenericAppend( pFileName, "_out.txt" );
409 Abc_TtStoreWrite( pFileNameOut, p, fBinary );
410 if ( fVerbose )
411 printf( "The resulting functions are written into file \"%s\".\n", pFileNameOut );
412 }
413
414 // delete data-structure
415 Abc_TtStoreFree( p, nVarNum );
416// printf( "Finished computing canonical forms for functions from file \"%s\".\n", pFileName );
417}
418
419
431int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose )
432{
433 if ( fVerbose )
434 printf( "Using truth tables from file \"%s\"...\n", pFileName );
435 if ( NpnType >= 0 && NpnType <= 12 )
436 Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
437 else
438 printf( "Unknown canonical form value (%d).\n", NpnType );
439 fflush( stdout );
440 return 0;
441}
442
446
447
449
int Abc_TruthCompare(word **p1, word **p2)
Definition abcNpn.c:128
int Abc_TruthNpnCountUnique(Abc_TtStore_t *p)
Definition abcNpn.c:90
void Abc_TruthNpnTest(char *pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose)
Definition abcNpn.c:389
void Abc_TruthNpnPrint(char *pCanonPermInit, unsigned uCanonPhase, int nVars)
Definition abcNpn.c:154
int nWords
Definition abcNpn.c:127
int Abc_NpnTest(char *pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose)
Definition abcNpn.c:431
int Abc_TruthNpnCountUniqueSort(Abc_TtStore_t *p)
Definition abcNpn.c:129
void Abc_TtStoreWrite(char *pFileName, Abc_TtStore_t *p, int fBinary)
Definition abcDec.c:359
void Abc_TtStoreFree(Abc_TtStore_t *p, int nVarNum)
Definition abcDec.c:176
Abc_TtStore_t * Abc_TtStoreLoad(char *pFileName, int nVarNum)
Definition abcDec.c:396
void Abc_TruthNpnPerform(Abc_TtStore_t *p, int NpnType, int fVerbose)
Definition abcNpn.c:177
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void freePermInfoPtr(permInfo *x)
void simpleMinimal(word *x, word *pAux, word *minimal, permInfo *pi, int nVars)
void resetPCanonPermArray(char *x, int nVars)
Definition luckyFast6.c:30
unsigned luckyCanonicizer_final_fast1(word *pInOut, int nVars, char *pCanonPerm)
permInfo * setPermInfoPtr(int var)
unsigned luckyCanonicizer_final_fast(word *pInOut, int nVars, char *pCanonPerm)
unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int fCA)
Definition dauCanon.c:2637
struct Abc_TtHieMan_t_ Abc_TtHieMan_t
Definition dau.h:62
unsigned Abc_TtCanonicizePhase(word *pTruth, int nVars)
Definition dauCanon.c:1187
unsigned(* TtCanonicizeFunc)(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)
Definition dau.h:63
unsigned Abc_TtCanonicizePerm(word *pTruth, int nVars, char *pCanonPerm)
Definition dauCanon.c:1085
unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int iThres)
Definition dauCanon.c:2573
unsigned Abc_TtCanonicizeHie(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int fExact)
Definition dauCanon.c:1318
Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
Definition dauCanon.c:1255
void Abc_TtHieManStop(Abc_TtHieMan_t *p)
Definition dauCanon.c:1273
unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)
Definition dauCanon.c:1530
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition dauCanon.c:1036
Cube * p
Definition exorList.c:222
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
unsigned Kit_TruthSemiCanonicize(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
Definition kitTruth.c:1657
word ** pFuncs
Definition abcDec.c:51
#define assert(ex)
Definition util_old.h:213
int memcmp()