From 49df91f071d6828113ded55f371e15d192304222 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 2 Aug 2011 12:58:37 +0700 Subject: Several bug fixes. --- src/aig/gia/giaAbs.c | 111 +++++++++++++++++++++++++++------------------- src/aig/saig/saig.h | 2 +- src/aig/saig/saigAbsPba.c | 68 +++++++++++++++++++++++++--- src/aig/ssw/sswRarity.c | 4 +- src/base/abci/abcDar.c | 18 ++++++-- src/misc/vec/vecPtr.h | 19 ++++++++ 6 files changed, 163 insertions(+), 59 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index fca680a5..8c89859c 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -225,52 +225,6 @@ Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew ) return vSelected; } -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose ) -{ - Gia_Man_t * pAbs; - Aig_Man_t * pAig; - Vec_Int_t * vFlops, * vFlopsNew, * vSelected; - if ( pGia->vFlopClasses == NULL ) - { - printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" ); - return 0; - } - // derive abstraction - pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); - // refine abstraction using PBA - pAig = Gia_ManToAigSimple( pAbs ); - Gia_ManStop( pAbs ); - vFlopsNew = Saig_ManPbaDerive( pAig, nFrames, nConfLimit, fVerbose ); - Aig_ManStop( pAig ); - // derive new classes - if ( vFlopsNew != NULL ) - { - vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); - vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); - Vec_IntFree( pGia->vFlopClasses ); - pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); - Vec_IntFree( vSelected ); - - Vec_IntFree( vFlopsNew ); - Vec_IntFree( vFlops ); - return 1; - } - // found counter-eample for the abstracted model - // or exceeded conflict limit - return 0; -} - /**Function************************************************************* Synopsis [Adds flops that should be present in the abstraction.] @@ -350,6 +304,71 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p ) return -1; } +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose ) +{ + Gia_Man_t * pAbs; + Aig_Man_t * pAig, * pOrig; + Vec_Int_t * vFlops, * vFlopsNew, * vSelected; + if ( pGia->vFlopClasses == NULL ) + { + printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" ); + return 0; + } + // derive abstraction + pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); + // refine abstraction using PBA + pAig = Gia_ManToAigSimple( pAbs ); + Gia_ManStop( pAbs ); + vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose ); + Aig_ManStop( pAig ); + // derive new classes + if ( pAig->pSeqModel == NULL ) + { + // the problem is UNSAT + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); + vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); + Vec_IntFree( pGia->vFlopClasses ); + pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); + Vec_IntFree( vSelected ); + + Vec_IntFree( vFlopsNew ); + Vec_IntFree( vFlops ); + return -1; + } + else if ( vFlopsNew == NULL ) + { + // found real counter-example + assert( pAig->pSeqModel != NULL ); + printf( "Refinement did not happen. Discovered a true counter-example.\n" ); + printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAig), Gia_ManPiNum(pGia) ); + // derive new counter-example + pOrig = Gia_ManToAigSimple( pGia ); + pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel ); + Aig_ManStop( pOrig ); + Aig_ManStop( pAig ); + return 0; + } + else + { + // found counter-eample for the abstracted model + // update flop classes + Vec_Int_t * vAbsFfsToAdd = vFlopsNew; + Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); + Vec_IntFree( vAbsFfsToAdd ); + return -1; + } +} //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 4437413f..f20641a5 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars ); /*=== sswAbsPba.c ==========================================================*/ -extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ); +extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose ); /*=== sswAbsStart.c ==========================================================*/ extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index a22871b7..3f8fb222 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -72,7 +72,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) +Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap ) { Aig_Man_t * pFrames; // unrolled timeframes Vec_Vec_t * vFrameCos; // the list of COs per frame @@ -107,6 +107,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) Saig_ManForEachLo( pAig, pObj, i ) pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreatePi(pFrames), Aig_ManConst0(pFrames) ); // iterate through the frames + *pvPiVarMap = Vec_IntStartFull( nFrames * Saig_ManPiNum(pAig) ); pObjNew = Aig_ManConst0(pFrames); for ( f = 0; f < nFrames; f++ ) { @@ -119,7 +120,10 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) else if ( Aig_ObjIsPo(pObj) ) pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Saig_ObjIsPi(pAig, pObj) ) + { + Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManPiNum(pFrames) ); pObj->pData = Aig_ObjCreatePi( pFrames ); + } else if ( Aig_ObjIsConst1(pObj) ) pObj->pData = Aig_ManConst1(pFrames); else if ( !Saig_ObjIsLo(pAig, pObj) ) @@ -153,6 +157,37 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) return pFrames; } +/**Function************************************************************* + + Synopsis [Derives the counter-example from the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap ) +{ + Abc_Cex_t * pCex; + int i, f, Entry; + pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); + Vec_IntForEachEntry( vPiVarMap, Entry, i ) + if ( Entry >= 0 ) + { + int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ]; + if ( sat_solver_var_value( pSat, iSatVar ) ) + Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); + } + // check what frame has failed + for ( f = 0; f < nFrames; f++ ) + { +// Aig_ManForEach + } + return pCex; +} + /**Function************************************************************* Synopsis [Derive unrolled timeframes.] @@ -164,9 +199,9 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ) +Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose ) { - Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps; + Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps, * vPiVarMap; Aig_Man_t * pFrames; sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -176,7 +211,7 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, in // create SAT solver clk = clock(); - pFrames = Saig_ManUnrollForPba( pAig, nFrames ); + pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap ); if ( fVerbose ) Aig_ManPrintStats( pFrames ); // pCnf = Cnf_DeriveSimple( pFrames, 0 ); @@ -212,9 +247,29 @@ Abc_PrintTime( 1, "Solving", clock() - clk ); if ( RetValue != l_False ) { if ( RetValue == l_True ) - printf( "Saig_ManPerformPba(): Internal Error!!! The resulting problem is SAT.\n" ); + { + Vec_Int_t * vAbsFfsToAdd; + ABC_FREE( pAig->pSeqModel ); + pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap ); + // CEX is detected - refine the flops + vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose ); + if ( Vec_IntSize(vAbsFfsToAdd) == 0 ) + { + Vec_IntFree( vAbsFfsToAdd ); + return NULL; + } + if ( fVerbose ) + { + printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) ); + Abc_PrintTime( 0, "Time", clock() - clk ); + } + return vAbsFfsToAdd; + } else - printf( "Saig_ManPerformPba(): SAT solver timed out.\n" ); + { + printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" ); + } + Vec_IntFree( vPiVarMap ); Vec_IntFree( vAssumps ); Vec_IntFree( vMapVar2FF ); sat_solver_delete( pSat ); @@ -242,6 +297,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk ); Vec_IntSort( vFlops, 0 ); // cleanup + Vec_IntFree( vPiVarMap ); Vec_IntFree( vAssumps ); Vec_IntFree( vMapVar2FF ); sat_solver_delete( pSat ); diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index 24cfe65d..037dfe55 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -899,7 +899,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in if ( Aig_ManNodeNum(pAig) == 0 ) return -1; // check trivially SAT miters - if ( Ssw_RarCheckTrivial( pAig, fVerbose ) ) + if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) return 0; if ( fVerbose ) printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", @@ -1006,7 +1006,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize if ( Aig_ManNodeNum(pAig) == 0 ) return -1; // check trivially SAT miters - if ( Ssw_RarCheckTrivial( pAig, 1 ) ) + if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) ) return 0; if ( fVerbose ) printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ebeafa86..3b0cbb06 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) printf( "(timeout %d sec). ", pPars->nTimeOut ); else printf( "(conf limit %d). ", pPars->nConfLimit ); - if ( pNtk->vSeqModelVec ) - Vec_PtrFreeFree( pNtk->vSeqModelVec ); - pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; +// if ( pNtk->vSeqModelVec ) +// Vec_PtrFreeFree( pNtk->vSeqModelVec ); +// pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } } else // if ( RetValue == 0 ) @@ -1838,7 +1838,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) } else { - printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs ); + int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); + if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) + printf( "All %d outputs are found to be SAT. ", nOutputs ); + else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) + printf( "None of the %d outputs is found to be SAT. ", nOutputs ); + else + printf( "Some outputs (%d out of %d) are proved SAT. ", + nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } } ABC_PRT( "Time", clock() - clk ); diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 9915f2d6..fe4b00b2 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -287,6 +287,25 @@ static inline int Vec_PtrSize( Vec_Ptr_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_PtrCountZero( Vec_Ptr_t * p ) +{ + int i, Counter = 0; + for ( i = 0; i < p->nSize; i++ ) + Counter += (p->pArray[i] == NULL); + return Counter; +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3