ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
saigSimSeq.c File Reference
#include "saig.h"
#include "proof/ssw/ssw.h"
Include dependency graph for saigSimSeq.c:

Go to the source code of this file.

Classes

struct  Raig_Man_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_ Raig_Man_t
 DECLARATIONS ///.
 

Functions

int Raig_ManFindPo (Aig_Man_t *pAig, int iNode)
 FUNCTION DEFINITIONS ///.
 
int Raig_ManCreate_rec (Raig_Man_t *p, Aig_Obj_t *pObj)
 
Raig_Man_t * Raig_ManCreate (Aig_Man_t *pAig)
 
void Raig_ManDelete (Raig_Man_t *p)
 
unsigned * Raig_ManSimRef (Raig_Man_t *p, int i)
 
unsigned * Raig_ManSimDeref (Raig_Man_t *p, int i)
 
int Raig_ManSimulateRound (Raig_Man_t *p, int fMiter, int fFirst, int *piPat)
 
Abc_Cex_t * Raig_ManGenerateCounter (Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
 
int Raig_ManSimulate (Aig_Man_t *pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose)
 

Typedef Documentation

◆ Raig_Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_ Raig_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [saigSimSeq.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Fast sequential AIG simulator.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
saigSimSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 32 of file saigSimSeq.c.

Function Documentation

◆ Raig_ManCreate()

Raig_Man_t * Raig_ManCreate ( Aig_Man_t * pAig)

Function*************************************************************

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file saigSimSeq.c.

147{
148 Raig_Man_t * p;
149 Aig_Obj_t * pObj;
150 int i, nObjs;
151 Aig_ManCleanData( pAig );
152 p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 );
153 memset( p, 0, sizeof(Raig_Man_t) );
154 p->pAig = pAig;
155 p->nPis = Saig_ManPiNum(pAig);
156 p->nPos = Saig_ManPoNum(pAig);
157 p->nCis = Aig_ManCiNum(pAig);
158 p->nCos = Aig_ManCoNum(pAig);
159 p->nNodes = Aig_ManNodeNum(pAig);
160 nObjs = p->nCis + p->nCos + p->nNodes + 2;
161 p->pFans0 = ABC_ALLOC( int, nObjs );
162 p->pFans1 = ABC_ALLOC( int, nObjs );
163 p->pRefs = ABC_ALLOC( int, nObjs );
164 p->pSims = ABC_CALLOC( unsigned, nObjs );
165 p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) );
166 // add objects (0=unused; 1=const1)
167 p->nObjs = 2;
168 pObj = Aig_ManConst1( pAig );
169 pObj->iData = 1;
170 Aig_ManForEachCi( pAig, pObj, i )
171 if ( Aig_ObjRefs(pObj) == 0 )
172 Raig_ManCreate_rec( p, pObj );
173 Aig_ManForEachCo( pAig, pObj, i )
174 Raig_ManCreate_rec( p, pObj );
175 assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) );
176 assert( p->nObjs == nObjs );
177 // collect flop outputs
178 p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
179 Saig_ManForEachLo( pAig, pObj, i )
180 Vec_IntPush( p->vLos, pObj->iData );
181 // collect flop inputs
182 p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
183 Saig_ManForEachLi( pAig, pObj, i )
184 {
185 Vec_IntPush( p->vLis, pObj->iData );
186 assert( p->pRefs[ pObj->iData ] == 0 );
187 p->pRefs[ pObj->iData ]++;
188 }
189 return p;
190}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
p
Cube * p
Definition exorList.c:222
Raig_Man_t
typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_ Raig_Man_t
DECLARATIONS ///.
Definition saigSimSeq.c:32
Raig_ManCreate_rec
int Raig_ManCreate_rec(Raig_Man_t *p, Aig_Obj_t *pObj)
Definition saigSimSeq.c:104
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Aig_Obj_t_::iData
int iData
Definition aig.h:88
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Raig_ManCreate_rec()

int Raig_ManCreate_rec ( Raig_Man_t * p,
Aig_Obj_t * pObj )

Function*************************************************************

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file saigSimSeq.c.

105{
106 int iFan0, iFan1;
107 assert( !Aig_IsComplement(pObj) );
108 if ( pObj->iData )
109 return pObj->iData;
110 assert( !Aig_ObjIsConst1(pObj) );
111 if ( Aig_ObjIsNode(pObj) )
112 {
113 iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
114 iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
115 iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
116 iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
117 }
118 else if ( Aig_ObjIsCo(pObj) )
119 {
120 iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
121 iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
122 iFan1 = 0;
123 }
124 else
125 {
126 iFan0 = iFan1 = 0;
127 Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) );
128 }
129 p->pFans0[p->nObjs] = iFan0;
130 p->pFans1[p->nObjs] = iFan1;
131 p->pRefs[p->nObjs] = Aig_ObjRefs(pObj);
132 return pObj->iData = p->nObjs++;
133}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Raig_ManDelete()

void Raig_ManDelete ( Raig_Man_t * p)

Function*************************************************************

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file saigSimSeq.c.

204{
205 Vec_IntFree( p->vCis2Ids );
206 Vec_IntFree( p->vLos );
207 Vec_IntFree( p->vLis );
208 ABC_FREE( p->pFans0 );
209 ABC_FREE( p->pFans1 );
210 ABC_FREE( p->pRefs );
211 ABC_FREE( p->pSims );
212 ABC_FREE( p->pMems );
213 ABC_FREE( p );
214}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Raig_ManFindPo()

int Raig_ManFindPo ( Aig_Man_t * pAig,
int iNode )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Find the PO corresponding to the PO driver.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file saigSimSeq.c.

84{
85 Aig_Obj_t * pObj;
86 int i;
87 Saig_ManForEachPo( pAig, pObj, i )
88 if ( pObj->iData == iNode )
89 return i;
90 return -1;
91}
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Here is the caller graph for this function:

◆ Raig_ManGenerateCounter()

Abc_Cex_t * Raig_ManGenerateCounter ( Aig_Man_t * pAig,
int iFrame,
int iOut,
int nWords,
int iPat,
Vec_Int_t * vCis2Ids )

Function*************************************************************

Synopsis [Returns the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 416 of file saigSimSeq.c.

417{
418 Abc_Cex_t * p;
419 unsigned * pData;
420 int f, i, w, iPioId, Counter;
421 p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
422 p->iFrame = iFrame;
423 p->iPo = iOut;
424 // fill in the binary data
425 Aig_ManRandom( 1 );
426 Counter = p->nRegs;
427 pData = ABC_ALLOC( unsigned, nWords );
428 for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
429 for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
430 {
431 iPioId = Vec_IntEntry( vCis2Ids, i );
432 if ( iPioId >= p->nPis )
433 continue;
434 for ( w = 0; w < nWords; w++ )
435 pData[w] = Aig_ManRandom( 0 );
436 if ( Abc_InfoHasBit( pData, iPat ) )
437 Abc_InfoSetBit( p->pData, Counter + iPioId );
438 }
439 ABC_FREE( pData );
440 return p;
441}
nWords
int nWords
Definition abcNpn.c:127
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Raig_ManSimDeref()

unsigned * Raig_ManSimDeref ( Raig_Man_t * p,
int i )

Function*************************************************************

Synopsis [Dereference simulaton info.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file saigSimSeq.c.

276{
277 unsigned * pSim;
278 assert( i );
279 if ( i == 1 ) // const 1
280 return p->pMems;
281 assert( p->pSims[i] > 0 );
282 pSim = p->pMems + p->pSims[i];
283 if ( --pSim[0] == 0 )
284 {
285 pSim[0] = p->MemFree;
286 p->MemFree = p->pSims[i];
287 p->pSims[i] = 0;
288 p->nMems--;
289 }
290 return pSim;
291}
Here is the caller graph for this function:

◆ Raig_ManSimRef()

unsigned * Raig_ManSimRef ( Raig_Man_t * p,
int i )

Function*************************************************************

Synopsis [References simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file saigSimSeq.c.

228{
229 unsigned * pSim;
230 assert( i > 1 );
231 assert( p->pSims[i] == 0 );
232 if ( p->MemFree == 0 )
233 {
234 unsigned * pPlace, Ent;
235 if ( p->nWordsAlloc == 0 )
236 {
237 assert( p->pMems == NULL );
238 p->nWordsAlloc = (1<<17); // -> 1Mb
239 p->nMems = 1;
240 }
241 p->nWordsAlloc *= 2;
242 p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
243 memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
244 pPlace = (unsigned *)&p->MemFree;
245 for ( Ent = p->nMems * (p->nWords + 1);
246 Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
247 Ent += p->nWords + 1 )
248 {
249 *pPlace = Ent;
250 pPlace = p->pMems + Ent;
251 }
252 *pPlace = 0;
253 }
254 p->pSims[i] = p->MemFree;
255 pSim = p->pMems + p->MemFree;
256 p->MemFree = pSim[0];
257 pSim[0] = p->pRefs[i];
258 p->nMems++;
259 if ( p->nMemsMax < p->nMems )
260 p->nMemsMax = p->nMems;
261 return pSim;
262}
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Raig_ManSimulate()

int Raig_ManSimulate ( Aig_Man_t * pAig,
int nWords,
int nIters,
int TimeLimit,
int fMiter,
int fVerbose )

Function*************************************************************

Synopsis [Returns 1 if the bug is detected, 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file saigSimSeq.c.

455{
456 Raig_Man_t * p;
457 Sec_MtrStatus_t Status;
458 int i, iPat, RetValue = 0;
459 abctime clk, clkTotal = Abc_Clock();
460 assert( Aig_ManRegNum(pAig) > 0 );
461 Status = Sec_MiterStatus( pAig );
462 if ( Status.nSat > 0 )
463 {
464 printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
465 return 1;
466 }
467 if ( Status.nUndec == 0 )
468 {
469 printf( "Miter is trivially unsatisfiable.\n" );
470 return 0;
471 }
472 Aig_ManRandom( 1 );
473 p = Raig_ManCreate( pAig );
474 p->nWords = nWords;
475 // iterate through objects
476 for ( i = 0; i < nIters; i++ )
477 {
478 clk = Abc_Clock();
479 RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
480 if ( fVerbose )
481 {
482 printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
483 printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC);
484 }
485 if ( RetValue > 0 )
486 {
487 int iOut = Raig_ManFindPo(p->pAig, RetValue);
488 assert( pAig->pSeqModel == NULL );
489 pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids );
490 if ( fVerbose )
491 printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
492 break;
493 }
494 if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
495 {
496 printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
497 break;
498 }
499 }
500 if ( fVerbose )
501 {
502 printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
503 p->nMemsMax,
504 1.0*(p->nObjs * 16)/(1<<20),
505 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
506 ABC_PRT( "Total time", Abc_Clock() - clkTotal );
507 }
508 Raig_ManDelete( p );
509 return RetValue > 0;
510}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Raig_ManGenerateCounter
Abc_Cex_t * Raig_ManGenerateCounter(Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
Definition saigSimSeq.c:416
Raig_ManDelete
void Raig_ManDelete(Raig_Man_t *p)
Definition saigSimSeq.c:203
Raig_ManCreate
Raig_Man_t * Raig_ManCreate(Aig_Man_t *pAig)
Definition saigSimSeq.c:146
Raig_ManFindPo
int Raig_ManFindPo(Aig_Man_t *pAig, int iNode)
FUNCTION DEFINITIONS ///.
Definition saigSimSeq.c:83
Raig_ManSimulateRound
int Raig_ManSimulateRound(Raig_Man_t *p, int fMiter, int fFirst, int *piPat)
Definition saigSimSeq.c:304
Sec_MiterStatus
Sec_MtrStatus_t Sec_MiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition saigMiter.c:46
Sec_MtrStatus_t
typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
INCLUDES ///.
Definition saig.h:41
Here is the call graph for this function:

◆ Raig_ManSimulateRound()

int Raig_ManSimulateRound ( Raig_Man_t * p,
int fMiter,
int fFirst,
int * piPat )

Function*************************************************************

Synopsis [Simulates one round.]

Description [Returns the number of PO entry if failed; 0 otherwise.]

SideEffects []

SeeAlso []

Definition at line 304 of file saigSimSeq.c.

305{
306 unsigned * pRes0, * pRes1, * pRes;
307 int i, w, nCis, nCos, iFan0, iFan1, iPioNum;
308 // nove the values to the register outputs
309 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
310 {
311 if ( iPioNum < p->nPis )
312 continue;
313 pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
314 if ( fFirst )
315 memset( pRes + 1, 0, sizeof(unsigned) * p->nWords );
316 else
317 {
318 pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) );
319 for ( w = 1; w <= p->nWords; w++ )
320 pRes[w] = pRes0[w];
321 }
322 // handle unused PIs
323 if ( pRes[0] == 0 )
324 {
325 pRes[0] = 1;
326 Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
327 }
328 }
329 // simulate the logic
330 nCis = nCos = 0;
331 for ( i = 2; i < p->nObjs; i++ )
332 {
333 if ( p->pFans0[i] == 0 ) // ci always has zero first fanin
334 {
335 iPioNum = Vec_IntEntry( p->vCis2Ids, nCis );
336 if ( iPioNum < p->nPis )
337 {
338 pRes = Raig_ManSimRef( p, i );
339 for ( w = 1; w <= p->nWords; w++ )
340 pRes[w] = Aig_ManRandom( 0 );
341 // handle unused PIs
342 if ( pRes[0] == 0 )
343 {
344 pRes[0] = 1;
345 Raig_ManSimDeref( p, i );
346 }
347 }
348 else
349 assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i );
350 nCis++;
351 continue;
352 }
353 if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin
354 {
355 pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
356 if ( nCos < p->nPos && fMiter )
357 {
358 unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0;
359 for ( w = 1; w <= p->nWords; w++ )
360 if ( pRes0[w] != Const )
361 {
362 *piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const );
363 return i;
364 }
365 }
366 else
367 {
368 pRes = Raig_ManSimRef( p, i );
369 assert( pRes[0] == 1 );
370 if ( Raig_LitIsCompl(p->pFans0[i]) )
371 for ( w = 1; w <= p->nWords; w++ )
372 pRes[w] = ~pRes0[w];
373 else
374 for ( w = 1; w <= p->nWords; w++ )
375 pRes[w] = pRes0[w];
376 }
377 nCos++;
378 continue;
379 }
380 pRes = Raig_ManSimRef( p, i );
381 assert( pRes[0] > 0 );
382 iFan0 = p->pFans0[i];
383 iFan1 = p->pFans1[i];
384 pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
385 pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) );
386 if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
387 for ( w = 1; w <= p->nWords; w++ )
388 pRes[w] = ~(pRes0[w] | pRes1[w]);
389 else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
390 for ( w = 1; w <= p->nWords; w++ )
391 pRes[w] = ~pRes0[w] & pRes1[w];
392 else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
393 for ( w = 1; w <= p->nWords; w++ )
394 pRes[w] = pRes0[w] & ~pRes1[w];
395 else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
396 for ( w = 1; w <= p->nWords; w++ )
397 pRes[w] = pRes0[w] & pRes1[w];
398 }
399 assert( nCis == p->nCis );
400 assert( nCos == p->nCos );
401 assert( p->nMems == 1 + Vec_IntSize(p->vLis) );
402 return 0;
403}
Raig_ManSimRef
unsigned * Raig_ManSimRef(Raig_Man_t *p, int i)
Definition saigSimSeq.c:227
Raig_ManSimDeref
unsigned * Raig_ManSimDeref(Raig_Man_t *p, int i)
Definition saigSimSeq.c:275
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function: