ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraUtilMaj.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
26#include "misc/vec/vec.h"
27#include "misc/vec/vecMem.h"
28#include "misc/extra/extra.h"
29#include "misc/util/utilTruth.h"
30#include "opt/dau/dau.h"
31
33
37
38typedef struct Gem_Man_t_ Gem_Man_t;
39typedef struct Gem_Obj_t_ Gem_Obj_t;
40
42{
43 int nVars; // max variable count
44 int nWords; // truth tabel word count
45 int nObjsAlloc; // allocated objects
46 int nObjs; // used objects
47 Gem_Obj_t * pObjs; // function objects
48 Vec_Mem_t * vTtMem; // truth table memory and hash table
49 word ** pTtElems; // elementary truth tables
51};
52
53struct Gem_Obj_t_ // 8 bytes
54{
55 unsigned nVars : 4; // variable count
56 unsigned nNodes : 4; // node count
57 unsigned History : 8; // (i < j) ? {vi, vj} : {vi, 0}
58 unsigned Groups : 16; // mask with last vars in each symmetric group
59 int Predec; // predecessor
60};
61
65
77void Gem_PrintNode( Gem_Man_t * p, int f, char * pLabel, int fUpdate )
78{
79 Gem_Obj_t * pObj = p->pObjs + f;
80 int GroupsMod = pObj->Groups;
81 if ( !p->fVerbose )
82 return;
83 printf( "Node %6d : %s Pred = %6d Vars = %d Nodes = %d History = %d%d Profile: ",
84 f, pLabel, pObj->Predec, pObj->nVars, pObj->nNodes, pObj->History & 0xF, pObj->History >> 4 );
85 Extra_PrintBinary2( stdout, (unsigned*)&GroupsMod, p->nVars ); printf("%s\n", fUpdate?" *":"");
86}
87Gem_Man_t * Gem_ManAlloc( int nVars, int fVerbose )
88{
89 Gem_Man_t * p;
90 assert( nVars <= 16 );
91 p = ABC_CALLOC( Gem_Man_t, 1 );
92 p->nVars = nVars;
93 p->nWords = Abc_TtWordNum( nVars );
94 p->nObjsAlloc = 10000000;
95 p->nObjs = 2;
96 p->pObjs = ABC_CALLOC( Gem_Obj_t, p->nObjsAlloc );
97 p->pObjs[1].nVars = p->pObjs[1].Groups = 1; // buffer
98 p->vTtMem = Vec_MemAllocForTT( nVars, 0 );
99 p->pTtElems = (word **)Extra_ArrayAlloc( nVars + 4, p->nWords, sizeof(word) );
100 p->fVerbose = fVerbose;
101 Abc_TtElemInit( p->pTtElems, nVars );
102 Gem_PrintNode( p, 1, "Original", 0 );
103 return p;
104}
106{
107 Vec_MemHashFree( p->vTtMem );
108 Vec_MemFree( p->vTtMem );
109 ABC_FREE( p->pTtElems );
110 ABC_FREE( p->pObjs );
111 ABC_FREE( p );
112 return 1;
113}
115{
116 int nObjNew = Abc_MinInt( 2 * p->nObjsAlloc, 0x7FFFFFFF );
117 assert( p->nObjs == p->nObjsAlloc );
118 if ( p->nObjs == 0x7FFFFFFF )
119 printf( "Hard limit on the number of nodes (0x7FFFFFFF) is reached. Quitting...\n" ), exit(1);
120 assert( p->nObjs < nObjNew );
121 printf("Extending object storage: %d -> %d.\n", p->nObjsAlloc, nObjNew );
122 p->pObjs = ABC_REALLOC( Gem_Obj_t, p->pObjs, nObjNew );
123 memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gem_Obj_t) * (nObjNew - p->nObjsAlloc) );
124 p->nObjsAlloc = nObjNew;
125}
126
138int Gem_GroupsDerive( word * pTruth, int nVars, word * pCof0, word * pCof1 )
139{
140 int v, Res = 1 << (nVars-1);
141 for ( v = 0; v < nVars-1; v++ )
142 if ( !Abc_TtVarsAreSymmetric(pTruth, nVars, v, v+1, pCof0, pCof1) )
143 Res |= (1 << v);
144 return Res;
145}
146
158int Gem_GroupVarRemove( int Groups, int i ) // remove i-th var
159{
160 int Mask = i ? Abc_InfoMask( i ) : 0;
161 assert( i >= 0 );
162 assert( (Groups >> i) & 1 );
163 return (Groups & Mask) | ((Groups & ~Mask) >> 1);
164}
165int Gem_GroupVarsInsert1( int Groups, int i, int fGroup ) // insert one bit after i
166{
167 int Mask = i+1 ? Abc_InfoMask( i+1 ) : 0;
168 assert( i+1 >= 0 );
169 assert( !fGroup || i == -1 || ((Groups >> i) & 1) );
170 assert( fGroup == 0 || fGroup == 1 );
171 return (Groups & Mask) | ((Groups & ~Mask) << 1) | (fGroup << (i+1));
172}
173int Gem_GroupVarsInsert3( int Groups, int i ) // insert group of 3 bits after i
174{
175 int Mask = i+1 ? Abc_InfoMask( i+1 ) : 0;
176 assert( i+1 >= 0 );
177 assert( i == -1 || (Groups >> i) & 1 );
178 return (Groups & Mask) | ((Groups & ~Mask) << 3) | (0x4 << (i+1));
179}
180int Gem_GroupUnpack( int Groups, int * pVars )
181{
182 int v, nGroups = 0;
183 for ( v = 0; Groups; v++, Groups >>= 1 )
184 if ( Groups & 1 )
185 pVars[nGroups++] = v;
186 return nGroups;
187}
188int Gem_FuncFindPlace( word * pTruth, int nWords, int Groups, word * pBest, int fOneVar )
189{
190 int pLast[16], nGroups = Gem_GroupUnpack( Groups, pLast );
191 int g, v, Value, BestPlace = nGroups ? pLast[nGroups - 1] : -1;
192 assert( nGroups >= 0 );
193 Abc_TtCopy( pBest, pTruth, nWords, 0 );
194 for ( g = nGroups - 1; g >= 0; g-- )
195 {
196 int Limit = g ? pLast[g-1] : -1;
197 for ( v = pLast[g]; v > Limit; v-- )
198 {
199 Abc_TtSwapAdjacent( pTruth, nWords, v+0 );
200 if ( fOneVar )
201 continue;
202 Abc_TtSwapAdjacent( pTruth, nWords, v+1 );
203 Abc_TtSwapAdjacent( pTruth, nWords, v+2 );
204 }
205 Value = memcmp(pBest, pTruth, sizeof(word)*nWords);
206 if ( Value < 0 )
207 {
208 Abc_TtCopy( pBest, pTruth, nWords, 0 );
209 BestPlace = Limit;
210 }
211 }
212 return BestPlace;
213}
214void Gem_FuncExpand( Gem_Man_t * p, int f, int i )
215{
216 Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
217 word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
218 word * pResult = p->pTtElems[p->nVars];
219 word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
220 int v, iFunc;
221 char pCanonPermC[16];
222 assert( i < (int)pObj->nVars );
223 assert( (int)pObj->nVars + 2 <= p->nVars );
224 Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
225 // move i variable to the end
226 for ( v = i; v < (int)pObj->nVars-1; v++ )
227 Abc_TtSwapAdjacent( pResult, p->nWords, v );
228 // create new symmetric group
229 assert( v == (int)pObj->nVars-1 );
230 Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v );
231 Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v );
232 Abc_TtMaj( pResult, p->pTtElems[v], p->pTtElems[v+1], p->pTtElems[v+2], p->nWords );
233 Abc_TtMux( pResult, pResult, pCofs[1], pCofs[0], p->nWords );
234 // canonicize
235 //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n");
236 Abc_TtCanonicizePerm( pResult, pObj->nVars + 2, pCanonPermC );
237 Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars+2), p->nVars );
238 //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n\n");
239 iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
240 if ( iFunc < p->nObjs )
241 return;
242 assert( iFunc == p->nObjs );
243 pNew->nVars = pObj->nVars + 2;
244 pNew->nNodes = pObj->nNodes + 1;
245 pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
246 pNew->Predec = f;
247 pNew->History = i;
248 Gem_PrintNode( p, iFunc, "Expand ", 0 );
249
250 assert( p->nObjs < p->nObjsAlloc );
251 if ( ++p->nObjs == p->nObjsAlloc )
252 Gem_ManRealloc( p );
253}
254
267{
268 Gem_Obj_t * pObj = p->pObjs + f;
269 word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
270 int Polar = Abc_TtIsFullySymmetric( pTruth, pObj->nVars );
271 if ( Polar != -1 )
272 {
273 int nHalfVars = (pObj->nVars+1) >> 1;
274 int Mask = Abc_Tt6Mask( nHalfVars );
275 printf( "Found symmetric %d-variable function: ", pObj->nVars );
276 Extra_PrintBinary2( stdout, (unsigned *)&Polar, pObj->nVars + 1 );
277 printf( " " );
278 if ( (pObj->nVars & 1) && Polar == (Mask << nHalfVars) )
279 {
280 printf( "This is majority-%d.\n", pObj->nVars );
281 return 0;
282 }
283 printf( "\n" );
284 }
285 return 0;
286}
287int Gem_FuncReduce( Gem_Man_t * p, int f, int i, int j )
288{
289 Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
290 word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
291 word * pResult = p->pTtElems[p->nVars];
292 word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
293 int v, iFunc;
294 char pCanonPermC[16];
295 assert( i < j && j < 16 );
296 Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
297 // move j variable to the end
298 for ( v = j; v < (int)pObj->nVars-1; v++ )
299 Abc_TtSwapAdjacent( pResult, p->nWords, v );
300 assert( v == (int)pObj->nVars-1 );
301 // move i variable to the end
302 for ( v = i; v < (int)pObj->nVars-2; v++ )
303 Abc_TtSwapAdjacent( pResult, p->nWords, v );
304 assert( v == (int)pObj->nVars-2 );
305 // create new variable
306 Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v+1 );
307 Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v+1 );
308 Abc_TtCofactor0( pCofs[0], p->nWords, v );
309 Abc_TtCofactor1( pCofs[1], p->nWords, v );
310 Abc_TtMux( pResult, p->pTtElems[v], pCofs[1], pCofs[0], p->nWords );
311 // canonicize
312 //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n");
313 Abc_TtCanonicizePerm( pResult, pObj->nVars - 1, pCanonPermC );
314 Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars-1), p->nVars );
315 //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n\n");
316 iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
317 if ( iFunc < p->nObjs )
318 return 0;
319 assert( iFunc == p->nObjs );
320 pNew->nVars = pObj->nVars - 1;
321 pNew->nNodes = pObj->nNodes;
322 pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
323 pNew->Predec = f;
324 pNew->History = (j << 4) | i;
325 Gem_PrintNode( p, iFunc, "Crossbar", 0 );
326 Gem_FuncCheckMajority( p, iFunc );
327
328 assert( p->nObjs < p->nObjsAlloc );
329 if ( ++p->nObjs == p->nObjsAlloc )
330 Gem_ManRealloc( p );
331 return 0;
332}
333
345int Gem_Enumerate( int nVars, int fDump, int fVerbose )
346{
347 abctime clk = Abc_Clock();
348 Gem_Man_t * p = Gem_ManAlloc( nVars, fVerbose );
349 int v, f, i, j, nObjsStop = 1;
350 for ( v = 1; v <= nVars-2; v++ )
351 {
352 // expand functions by adding a gate
353 int nObjsStopPrev = nObjsStop;
354 nObjsStop = p->nObjs;
355 printf( "Expanding var %2d (functions = %10d) ", v, p->nObjs );
356 Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
357 for ( f = 0; f < nObjsStop; f++ )
358 if ( v == (int)p->pObjs[f].nVars || (v > (int)p->pObjs[f].nVars && f >= nObjsStopPrev) )
359 for ( i = 0; i < v; i++ )
360 if ( (int)p->pObjs[f].Groups & (1 << i) )
361 Gem_FuncExpand( p, f, i );
362 // reduce functions by adding a crossbar
363 printf( "Connecting var %2d (functions = %10d) ", v, p->nObjs );
364 Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
365 for ( f = nObjsStop; f < p->nObjs; f++ )
366 for ( i = 0; i < (int)p->pObjs[f].nVars; i++ )
367 if ( (int)p->pObjs[f].Groups & (1 << i) )
368 for ( j = i+1; j < (int)p->pObjs[f].nVars; j++ )
369 if ( (int)p->pObjs[f].Groups & (1 << j) )
370 if ( Gem_FuncReduce( p, f, i, j ) )
371 return Gem_ManFree( p );
372 }
373 printf( "Finished (functions = %10d) ", p->nObjs );
374 Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
375 if ( fDump ) Vec_MemDumpTruthTables( p->vTtMem, "enum", nVars );
376 Gem_ManFree( p );
377 return 0;
378}
379
383
384
386
int nWords
Definition abcNpn.c:127
ABC_INT64_T abctime
Definition abc_global.h:332
#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_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
unsigned Abc_TtCanonicizePerm(word *pTruth, int nVars, char *pCanonPerm)
Definition dauCanon.c:1085
Cube * p
Definition exorList.c:222
Gem_Man_t * Gem_ManAlloc(int nVars, int fVerbose)
int Gem_GroupVarsInsert1(int Groups, int i, int fGroup)
struct Gem_Obj_t_ Gem_Obj_t
int Gem_FuncReduce(Gem_Man_t *p, int f, int i, int j)
int Gem_GroupVarRemove(int Groups, int i)
int Gem_Enumerate(int nVars, int fDump, int fVerbose)
void Gem_FuncExpand(Gem_Man_t *p, int f, int i)
int Gem_GroupsDerive(word *pTruth, int nVars, word *pCof0, word *pCof1)
void Gem_PrintNode(Gem_Man_t *p, int f, char *pLabel, int fUpdate)
FUNCTION DEFINITIONS ///.
int Gem_GroupUnpack(int Groups, int *pVars)
void Gem_ManRealloc(Gem_Man_t *p)
int Gem_ManFree(Gem_Man_t *p)
int Gem_GroupVarsInsert3(int Groups, int i)
int Gem_FuncCheckMajority(Gem_Man_t *p, int f)
typedefABC_NAMESPACE_IMPL_START struct Gem_Man_t_ Gem_Man_t
DECLARATIONS ///.
int Gem_FuncFindPlace(word *pTruth, int nWords, int Groups, word *pBest, int fOneVar)
void Extra_PrintBinary2(FILE *pFile, unsigned Sign[], int nBits)
void ** Extra_ArrayAlloc(int nCols, int nRows, int Size)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Vec_Mem_t * vTtMem
Gem_Obj_t * pObjs
word ** pTtElems
unsigned History
unsigned Groups
unsigned nNodes
unsigned nVars
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
#define assert(ex)
Definition util_old.h:213
char * memset()
int memcmp()
VOID_HACK exit()