diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbs.c | 13 | ||||
-rw-r--r-- | src/aig/saig/saigMiter.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigSimMv.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigSynch.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigTrans.c | 2 |
6 files changed, 12 insertions, 11 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f11345eb..5ddef829 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index c9e76626..a2a915f7 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -693,15 +693,15 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose ) -{ +Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose ) +{ extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); Vec_Int_t * vFlopsNew, * vPiToReg; Aig_Obj_t * pObj; int i, Entry, iFlop; - Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose ); + Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose ); if ( pAbs->pSeqModel == NULL ) return NULL; // Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); @@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ) +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -779,11 +779,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, if ( fSkipProof ) { - assert( 0 ); +// assert( 0 ); if ( fVerbose ) printf( "Performing counter-example-based refinement.\n" ); // vFlops = Vec_IntStartNatural( 100 ); // Vec_IntPush( vFlops, 0 ); + vFlops = Vec_IntStartNatural( 1 ); } else { @@ -858,7 +859,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { - pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose ); + pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pTemp == NULL ) break; Aig_ManStop( pResult ); diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 71bdadf6..0a9f230b 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -327,7 +327,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) ); assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 ); // start timeframes - p = Aig_ManStart( nFrames * AIG_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); + p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); p->pName = Aig_UtilStrsav( "frames" ); // create variables for register outputs pAig = pBot; diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 9bc6416b..a3fdaf93 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -180,7 +180,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 ) pNode->iFan1 = iFan1; pNode->iNext = 0; if ( iFan0 || iFan1 ) - p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); + p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); else p->pLevels[p->nObjs] = 0, p->nPis++; return p->nObjs++; diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index ff46634e..b29fcb9b 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -616,7 +616,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, return NULL; } clk = clock(); - vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); + vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); // process Design 1 RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 ); diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index f50af285..a92d9369 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -398,7 +398,7 @@ ABC_PRT( "Fraiging", clock() - clk ); clk = clock(); pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); ABC_PRT( "Mapped", clock() - clk ); - // ABC_FREE mapping + // free mapping Saig_ManStopMap2( pAig ); clk = clock(); pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); |