ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
fsim.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Fsim_ParSim_t_
 
struct  Fsim_ParSwitch_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t
 INCLUDES ///.
 
typedef struct Fsim_ParSim_t_ Fsim_ParSim_t
 
typedef struct Fsim_ParSwitch_t_ Fsim_ParSwitch_t
 

Functions

void Fsim_ManSetDefaultParamsSim (Fsim_ParSim_t *p)
 MACRO DEFINITIONS ///.
 
void Fsim_ManSetDefaultParamsSwitch (Fsim_ParSwitch_t *p)
 
int Fsim_ManSimulate (Aig_Man_t *pAig, Fsim_ParSim_t *pPars)
 
Vec_Int_t * Fsim_ManSwitchSimulate (Aig_Man_t *pAig, Fsim_ParSwitch_t *pPars)
 
Vec_Ptr_t * Fsim_ManTerSimulate (Aig_Man_t *pAig, int fVerbose)
 

Typedef Documentation

◆ Fsim_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t

INCLUDES ///.

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

FileName [fsim.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast sequential AIG simulator.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
fsim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 42 of file fsim.h.

◆ Fsim_ParSim_t

typedef struct Fsim_ParSim_t_ Fsim_ParSim_t

Definition at line 45 of file fsim.h.

◆ Fsim_ParSwitch_t

typedef struct Fsim_ParSwitch_t_ Fsim_ParSwitch_t

Definition at line 59 of file fsim.h.

Function Documentation

◆ Fsim_ManSetDefaultParamsSim()

void Fsim_ManSetDefaultParamsSim ( Fsim_ParSim_t * p)
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [fsimCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast sequential AIG simulator.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fsimCore.c.

46{
47 memset( p, 0, sizeof(Fsim_ParSim_t) );
48 // user-controlled parameters
49 p->nWords = 8; // the number of machine words
50 p->nIters = 32; // the number of timeframes
51 p->TimeLimit = 60; // time limit in seconds
52 p->fCheckMiter = 0; // check if miter outputs are non-zero
53 p->fVerbose = 1; // enables verbose output
54 // internal parameters
55 p->fCompressAig = 0; // compresses internal data
56}
p
Cube * p
Definition exorList.c:222
Fsim_ParSim_t
struct Fsim_ParSim_t_ Fsim_ParSim_t
Definition fsim.h:45
memset
char * memset()
Here is the call graph for this function:

◆ Fsim_ManSetDefaultParamsSwitch()

void Fsim_ManSetDefaultParamsSwitch ( Fsim_ParSwitch_t * p)
extern

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file fsimCore.c.

70{
71 memset( p, 0, sizeof(Fsim_ParSwitch_t) );
72 // user-controlled parameters
73 p->nWords = 1; // the number of machine words
74 p->nIters = 48; // the number of timeframes
75 p->nPref = 16; // the number of first timeframes to skip
76 p->nRandPiNum = 0; // PI trans prob (0=1/2; 1=1/4; 2=1/8, etc)
77 p->fProbOne = 1; // collect probability of one
78 p->fProbTrans = 1; // collect probatility of switching
79 p->fVerbose = 1; // enables verbose output
80}
Fsim_ParSwitch_t
struct Fsim_ParSwitch_t_ Fsim_ParSwitch_t
Definition fsim.h:59
Here is the call graph for this function:

◆ Fsim_ManSimulate()

int Fsim_ManSimulate ( Aig_Man_t * pAig,
Fsim_ParSim_t * pPars )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file fsimSim.c.

472{
473 Fsim_Man_t * p;
474 Sec_MtrStatus_t Status;
475 int i, iOut, iPat;
476 clock_t clk, clkTotal = clock(), clk2, clk2Total = 0;
477 assert( Aig_ManRegNum(pAig) > 0 );
478 if ( pPars->fCheckMiter )
479 {
480 Status = Sec_MiterStatus( pAig );
481 if ( Status.nSat > 0 )
482 {
483 printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
484 return 1;
485 }
486 if ( Status.nUndec == 0 )
487 {
488 printf( "Miter is trivially unsatisfiable.\n" );
489 return 0;
490 }
491 }
492 // create manager
493 clk = clock();
494 p = Fsim_ManCreate( pAig );
495 p->nWords = pPars->nWords;
496 if ( pPars->fVerbose )
497 {
498 printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d. FrtMem = %7.2f MB. ",
499 p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront,
500 4.0*p->nWords*(p->nFront)/(1<<20) );
501 ABC_PRT( "Time", clock() - clk );
502 }
503 // create simulation frontier
504 clk = clock();
505 Fsim_ManFront( p, pPars->fCompressAig );
506 if ( pPars->fVerbose )
507 {
508 printf( "Max ID = %8d. Log max ID = %2d. AigMem = %7.2f MB (%5.2f byte/obj). ",
509 p->iNumber, Aig_Base2Log(p->iNumber),
510 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
511 1.0*(p->pDataCur-p->pDataAig)/p->nObjs );
512 ABC_PRT( "Time", clock() - clk );
513 }
514 // perform simulation
515 Aig_ManRandom( 1 );
516 assert( p->pDataSim == NULL );
517 p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->nFront );
518 p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * p->nCis );
519 p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * p->nCos );
520 Fsim_ManSimInfoInit( p );
521 for ( i = 0; i < pPars->nIters; i++ )
522 {
523 Fsim_ManSimulateRound( p );
524 if ( pPars->fVerbose )
525 {
526 printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
527 printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
528 }
529 if ( pPars->fCheckMiter && Fsim_ManCheckPos( p, &iOut, &iPat ) )
530 {
531 assert( pAig->pSeqModel == NULL );
532 pAig->pSeqModel = Fsim_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
533 if ( pPars->fVerbose )
534 printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
535 break;
536 }
537 if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
538 break;
539 clk2 = clock();
540 if ( i < pPars->nIters - 1 )
541 Fsim_ManSimInfoTransfer( p );
542 clk2Total += clock() - clk2;
543 }
544 if ( pAig->pSeqModel == NULL )
545 printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
546 if ( pPars->fVerbose )
547 {
548 printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
549 p->nCrossCutMax,
550 p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
551 4.0*p->nWords*(p->nFront+p->nCis+p->nCos)/(1<<20) );
552 ABC_PRT( "Sim time", clock() - clkTotal );
553
554// ABC_PRT( "Additional time", clk2Total );
555// Fsim_ManSimulateRoundTest( p );
556// Fsim_ManSimulateRoundTest2( p );
557 }
558 Fsim_ManDelete( p );
559 return pAig->pSeqModel != NULL;
560
561}
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Fsim_ManFront
void Fsim_ManFront(Fsim_Man_t *p, int fCompressAig)
FUNCTION DECLARATIONS ///.
Definition fsimFront.c:245
Fsim_ManDelete
void Fsim_ManDelete(Fsim_Man_t *p)
Definition fsimMan.c:169
Fsim_ManCreate
Fsim_Man_t * Fsim_ManCreate(Aig_Man_t *pAig)
Definition fsimMan.c:102
Fsim_ManGenerateCounter
Abc_Cex_t * Fsim_ManGenerateCounter(Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
Definition fsimSim.c:433
Fsim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t
INCLUDES ///.
Definition fsim.h:42
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
Fsim_ParSim_t_::nIters
int nIters
Definition fsim.h:50
Fsim_ParSim_t_::fCheckMiter
int fCheckMiter
Definition fsim.h:52
Fsim_ParSim_t_::fCompressAig
int fCompressAig
Definition fsim.h:55
Fsim_ParSim_t_::fVerbose
int fVerbose
Definition fsim.h:53
Fsim_ParSim_t_::TimeLimit
int TimeLimit
Definition fsim.h:51
Fsim_ParSim_t_::nWords
int nWords
Definition fsim.h:49
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Fsim_ManSwitchSimulate()

Vec_Int_t * Fsim_ManSwitchSimulate ( Aig_Man_t * pAig,
Fsim_ParSwitch_t * pPars )
extern

◆ Fsim_ManTerSimulate()

Vec_Ptr_t * Fsim_ManTerSimulate ( Aig_Man_t * pAig,
int fVerbose )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 339 of file fsimTsim.c.

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}
nWords
int nWords
Definition abcNpn.c:127
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Fsim_ManTerStateInsert
void Fsim_ManTerStateInsert(unsigned *pState, int nWords, unsigned **pBins, int nBins)
Definition fsimTsim.c:236
Fsim_ManTerStateCreate
unsigned * Fsim_ManTerStateCreate(unsigned *pInfo, int nPis, int nCis, int nWords)
Definition fsimTsim.c:255
Fsim_ManTerStateLookup
int Fsim_ManTerStateLookup(unsigned *pState, int nWords, unsigned **pBins, int nBins)
Definition fsimTsim.c:214
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function: