ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fsimTsim.c
Go to the documentation of this file.
1
20
21#include "fsimInt.h"
22
24
25
29
30#define FSIM_ZER 1
31#define FSIM_ONE 2
32#define FSIM_UND 3
33
34static inline int Aig_XsimNotCond( int Value, int fCompl )
35{
36 if ( Value == FSIM_UND )
37 return FSIM_UND;
38 if ( Value == FSIM_ZER + fCompl )
39 return FSIM_ZER;
40 return FSIM_ONE;
41}
42static inline int Aig_XsimAndCond( int Value0, int fCompl0, int Value1, int fCompl1 )
43{
44 if ( Value0 == FSIM_UND || Value1 == FSIM_UND )
45 return FSIM_UND;
46 if ( Value0 == FSIM_ZER + fCompl0 || Value1 == FSIM_ZER + fCompl1 )
47 return FSIM_ZER;
48 return FSIM_ONE;
49}
50
51static inline int Fsim_ManTerSimInfoGet( unsigned * pInfo, int i )
52{
53 return 3 & (pInfo[i >> 4] >> ((i & 15) << 1));
54}
55static inline void Fsim_ManTerSimInfoSet( unsigned * pInfo, int i, int Value )
56{
57 assert( Value >= FSIM_ZER && Value <= FSIM_UND );
58 Value ^= Fsim_ManTerSimInfoGet( pInfo, i );
59 pInfo[i >> 4] ^= (Value << ((i & 15) << 1));
60}
61
62static inline unsigned * Fsim_ManTerStateNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
63static inline void Fsim_ManTerStateSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
64
68
80static inline void Fsim_ManTerSimulateCi( Fsim_Man_t * p, int iNode, int iCi )
81{
82 Fsim_ManTerSimInfoSet( p->pDataSim, iNode, Fsim_ManTerSimInfoGet(p->pDataSimCis, iCi) );
83}
84
96static inline void Fsim_ManTerSimulateCo( Fsim_Man_t * p, int iCo, int iFan0 )
97{
98 int Value = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan0) );
99 Fsim_ManTerSimInfoSet( p->pDataSimCos, iCo, Aig_XsimNotCond( Value, Fsim_LitIsCompl(iFan0) ) );
100}
101
113static inline void Fsim_ManTerSimulateNode( Fsim_Man_t * p, int iNode, int iFan0, int iFan1 )
114{
115 int Value0 = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan0) );
116 int Value1 = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan1) );
117 Fsim_ManTerSimInfoSet( p->pDataSim, iNode, Aig_XsimAndCond( Value0, Fsim_LitIsCompl(iFan0), Value1, Fsim_LitIsCompl(iFan1) ) );
118}
119
131static inline void Fsim_ManTerSimInfoInit( Fsim_Man_t * p )
132{
133 int iPioNum, i;
134 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
135 {
136 if ( iPioNum < p->nPis )
137 Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_UND );
138 else
139 Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_ZER );
140 }
141}
142
154static inline void Fsim_ManTerSimInfoTransfer( Fsim_Man_t * p )
155{
156 int iPioNum, i;
157 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
158 {
159 if ( iPioNum < p->nPis )
160 Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_UND );
161 else
162 Fsim_ManTerSimInfoSet( p->pDataSimCis, i, Fsim_ManTerSimInfoGet( p->pDataSimCos, p->nPos+iPioNum-p->nPis ) );
163 }
164}
165
166
178int Fsim_ManTerStateHash( unsigned * pState, int nWords, int nTableSize )
179{
180 static int s_FPrimes[128] = {
181 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
182 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
183 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
184 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
185 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
186 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
187 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
188 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
189 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
190 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
191 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
192 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
193 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
194 };
195 unsigned uHash;
196 int i;
197 uHash = 0;
198 for ( i = 0; i < nWords; i++ )
199 uHash ^= pState[i] * s_FPrimes[i & 0x7F];
200 return uHash % nTableSize;
201}
202
214int Fsim_ManTerStateLookup( unsigned * pState, int nWords, unsigned ** pBins, int nBins )
215{
216 unsigned * pEntry;
217 int Hash;
218 Hash = Fsim_ManTerStateHash( pState, nWords, nBins );
219 for ( pEntry = pBins[Hash]; pEntry; pEntry = Fsim_ManTerStateNext(pEntry, nWords) )
220 if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
221 return 1;
222 return 0;
223}
224
236void Fsim_ManTerStateInsert( unsigned * pState, int nWords, unsigned ** pBins, int nBins )
237{
238 int Hash = Fsim_ManTerStateHash( pState, nWords, nBins );
239 assert( !Fsim_ManTerStateLookup( pState, nWords, pBins, nBins ) );
240 Fsim_ManTerStateSetNext( pState, nWords, pBins[Hash] );
241 pBins[Hash] = pState;
242}
243
255unsigned * Fsim_ManTerStateCreate( unsigned * pInfo, int nPis, int nCis, int nWords )
256{
257 unsigned * pRes;
258 int i;
259 pRes = (unsigned *)ABC_CALLOC( char, sizeof(unsigned) * nWords + sizeof(unsigned *) );
260 for ( i = nPis; i < nCis; i++ )
261 Fsim_ManTerSimInfoSet( pRes, i-nPis, Fsim_ManTerSimInfoGet(pInfo, i) );
262 return pRes;
263}
264
276void Fsim_ManTerStatePrint( unsigned * pState, int nRegs )
277{
278 int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
279 for ( i = 0; i < nRegs; i++ )
280 {
281 Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
282 if ( Value == 1 )
283 printf( "0" ), nZeros++;
284 else if ( Value == 2 )
285 printf( "1" ), nOnes++;
286 else if ( Value == 3 )
287 printf( "x" ), nDcs++;
288 else
289 assert( 0 );
290 }
291 printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
292}
293
294
306static inline void Fsim_ManTerSimulateRound( Fsim_Man_t * p )
307{
308 int * pCur, * pEnd;
309 int iCis = 0, iCos = 0;
310 if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
311 Fsim_ManTerSimInfoSet( p->pDataSimCis, 1, FSIM_ONE );
312 pCur = p->pDataAig2 + 6;
313 pEnd = p->pDataAig2 + 3 * p->nObjs;
314 while ( pCur < pEnd )
315 {
316 if ( pCur[1] == 0 )
317 Fsim_ManTerSimulateCi( p, pCur[0], iCis++ );
318 else if ( pCur[2] == 0 )
319 Fsim_ManTerSimulateCo( p, iCos++, pCur[1] );
320 else
321 Fsim_ManTerSimulateNode( p, pCur[0], pCur[1], pCur[2] );
322 pCur += 3;
323 }
324 assert( iCis == p->nCis );
325 assert( iCos == p->nCos );
326}
327
339Vec_Ptr_t * Fsim_ManTerSimulate( Aig_Man_t * pAig, int fVerbose )
340{
341 Fsim_Man_t * p;
342 Vec_Ptr_t * vStates;
343 unsigned ** pBins, * pState;
344 int i, nWords, nBins;
345 clock_t clk, clkTotal = clock();
346 assert( Aig_ManRegNum(pAig) > 0 );
347 // create manager
348 clk = clock();
349 p = Fsim_ManCreate( pAig );
350 if ( fVerbose )
351 {
352 printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d. FrtMem = %7.2f MB. ",
353 p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront,
354 4.0*Aig_BitWordNum(2 * p->nFront)/(1<<20) );
355 ABC_PRT( "Time", clock() - clk );
356 }
357 // create simulation frontier
358 clk = clock();
359 Fsim_ManFront( p, 0 );
360 if ( fVerbose )
361 {
362 printf( "Max ID = %8d. Log max ID = %2d. AigMem = %7.2f MB (%5.2f byte/obj). ",
363 p->iNumber, Aig_Base2Log(p->iNumber),
364 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
365 1.0*(p->pDataCur-p->pDataAig)/p->nObjs );
366 ABC_PRT( "Time", clock() - clk );
367 }
368 // allocate storage for terminary states
369 nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
370 vStates = Vec_PtrAlloc( 1000 );
371 nBins = Abc_PrimeCudd( 500 );
372 pBins = ABC_ALLOC( unsigned *, nBins );
373 memset( pBins, 0, sizeof(unsigned *) * nBins );
374 // perform simulation
375 assert( p->pDataSim == NULL );
376 p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nFront) * sizeof(unsigned) );
377 p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCis) * sizeof(unsigned) );
378 p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCos) * sizeof(unsigned) );
379 Fsim_ManTerSimInfoInit( p );
380 // hash the first state
381 pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
382 Vec_PtrPush( vStates, pState );
383 Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
384 // perform simuluation till convergence
385 for ( i = 0; ; i++ )
386 {
387 Fsim_ManTerSimulateRound( p );
388 Fsim_ManTerSimInfoTransfer( p );
389 // hash the first state
390 pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
391 Vec_PtrPush( vStates, pState );
392 if ( Fsim_ManTerStateLookup(pState, nWords, pBins, nBins) )
393 break;
394 Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
395 }
396 if ( fVerbose )
397 {
398 printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
399 p->nCrossCutMax,
400 p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
401 4.0*(Aig_BitWordNum(2 * p->nFront)+Aig_BitWordNum(2 * p->nCis)+Aig_BitWordNum(2 * p->nCos))/(1<<20) );
402 ABC_PRT( "Sim time", clock() - clkTotal );
403 }
404 ABC_FREE( pBins );
405 Fsim_ManDelete( p );
406 return vStates;
407
408}
409
413
414
416
int nWords
Definition abcNpn.c:127
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#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
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Cube * p
Definition exorList.c:222
void Fsim_ManFront(Fsim_Man_t *p, int fCompressAig)
FUNCTION DECLARATIONS ///.
Definition fsimFront.c:245
void Fsim_ManDelete(Fsim_Man_t *p)
Definition fsimMan.c:169
Fsim_Man_t * Fsim_ManCreate(Aig_Man_t *pAig)
Definition fsimMan.c:102
Vec_Ptr_t * Fsim_ManTerSimulate(Aig_Man_t *pAig, int fVerbose)
Definition fsimTsim.c:339
void Fsim_ManTerStateInsert(unsigned *pState, int nWords, unsigned **pBins, int nBins)
Definition fsimTsim.c:236
int Fsim_ManTerStateHash(unsigned *pState, int nWords, int nTableSize)
Definition fsimTsim.c:178
#define FSIM_ONE
Definition fsimTsim.c:31
void Fsim_ManTerStatePrint(unsigned *pState, int nRegs)
Definition fsimTsim.c:276
unsigned * Fsim_ManTerStateCreate(unsigned *pInfo, int nPis, int nCis, int nWords)
Definition fsimTsim.c:255
#define FSIM_UND
Definition fsimTsim.c:32
#define FSIM_ZER
DECLARATIONS ///.
Definition fsimTsim.c:30
int Fsim_ManTerStateLookup(unsigned *pState, int nWords, unsigned **pBins, int nBins)
Definition fsimTsim.c:214
typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t
INCLUDES ///.
Definition fsim.h:42
#define assert(ex)
Definition util_old.h:213
char * memset()
int memcmp()
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42