diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-01-18 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-01-18 08:01:00 -0800 |
commit | f936cc0680c98ffe51b3a1716c996072d5dbf76c (patch) | |
tree | 784a2a809fb6b972ec6a8e2758ab758ca590d01a /src/aig/saig/saigAbs.c | |
parent | c9ad5880cc61787dec6d018111b63023407ce0e6 (diff) | |
download | abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.gz abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.bz2 abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.zip |
Version abc90118
Diffstat (limited to 'src/aig/saig/saigAbs.c')
-rw-r--r-- | src/aig/saig/saigAbs.c | 259 |
1 files changed, 213 insertions, 46 deletions
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 8498f59a..d2a45b4e 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -23,6 +23,7 @@ #include "cnf.h" #include "satSolver.h" #include "satStore.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -105,7 +106,11 @@ int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * if ( Saig_ObjIsPi( p, pObj ) ) return 1; if ( Saig_ObjIsLo( p, pObj ) ) + { + if ( i == 0 ) + return 1; return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 ); + } if ( Aig_ObjIsPo( pObj ) ) return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); @@ -130,8 +135,8 @@ Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax ) Aig_Obj_t * pObj; int i, f; vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax ); - Saig_ManForEachLo( p, pObj, i ) - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); +// Saig_ManForEachLo( p, pObj, i ) +// Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); for ( f = 0; f < nFramesMax; f++ ) { Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f ); @@ -193,18 +198,19 @@ Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) Vec_PtrClear( vLoObjs ); Vec_PtrClear( vLiObjs ); Aig_ManForEachPi( p, pObj, i ) - { + { if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) { pObj->pData = Aig_ObjCreatePi(pFrame); if ( i >= Saig_ManPiNum(p) ) Vec_PtrPush( vLoObjs, pObj ); - } + } } // remember the number of (implicit) registers in this frame pFrame->nAsserts = Vec_PtrSize(vLoObjs); // create POs Aig_ManForEachPo( p, pObj, i ) + { if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) { Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); @@ -212,8 +218,10 @@ Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) if ( i >= Saig_ManPoNum(p) ) Vec_PtrPush( vLiObjs, pObj ); } - Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) ); - // set the new PIs to point to the recorresponding registers + } +// Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) ); + Vec_PtrPush( vFrames, Cnf_DeriveSimple(pFrame, Aig_ManPoNum(pFrame)) ); + // set the new PIs to point to the corresponding registers Aig_ManCleanData( pFrame ); Vec_PtrForEachEntry( vLoObjs, pObj, i ) ((Aig_Obj_t *)pObj->pData)->pData = pObj; @@ -290,7 +298,10 @@ sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames ) // add auxiliary clauses (output, connectors, initial) // add output clause if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) + { + printf( "SAT solver is not created correctly.\n" ); assert( 0 ); + } Vec_IntFree( vPoLits ); // add connecting clauses @@ -627,7 +638,7 @@ void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) /**Function************************************************************* - Synopsis [Performs proof-based abstraction using BMC of the given depth.] + Synopsis [Derive a new counter-example.] Description [] @@ -636,63 +647,194 @@ void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose ) +Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCexAbs ) { - Aig_Man_t * pResult; - Cnf_Dat_t * pCnf; - Vec_Ptr_t * vFrames; - sat_solver * pSat; - Vec_Int_t * vCore; - Vec_Int_t * vFlops; - int clk = clock(), clk2 = clock(); - assert( Aig_ManRegNum(p) > 0 ); - Aig_ManSetPioNumbers( p ); - if ( fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); - if ( fDynamic ) + Ssw_Cex_t * pCex; + Aig_Obj_t * pObj; + int i, f; + // start the counter-example + pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex->iFrame = pCexAbs->iFrame; + pCex->iPo = pCexAbs->iPo; + // copy the bit data + for ( f = 0; f <= pCexAbs->iFrame; f++ ) + { + Saig_ManForEachPi( pAbs, pObj, i ) + { + if ( i == Saig_ManPiNum(p) ) + break; + if ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); + } + } + // verify the counter example + if ( !Ssw_SmlRunCounterExample( p, pCex ) ) { - // create CNF for the frames - vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose ); - // create dynamic solver - pSat = Saig_AbsCreateSolverDyn( p, vFrames ); + printf( "Saig_ManCexShrink(): Counter-example is invalid.\n" ); + Ssw_SmlFreeCounterExample( pCex ); + pCex = NULL; } else { - // create CNF for the AIG - pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); - // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, 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 ); + if ( pAbs->pSeqModel == NULL ) + return NULL; +// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); + if ( Vec_IntSize(vFlopsNew) == 0 ) + { + printf( "Discovered a true counter-example!\n" ); + p->pSeqModel = Saig_ManCexShrink( p, pAbs, pAbs->pSeqModel ); + Vec_IntFree( vFlopsNew ); + return NULL; } if ( fVerbose ) + printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); + // vFlopsNew contains PI number that should be kept in pAbs + + // for each additional PI, collect the number of a register it stands for + Vec_IntForEachEntry( vFlops, Entry, i ) { - printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); - PRT( "Time", clock() - clk2 ); + pObj = Saig_ManLo( p, Entry ); + pObj->fMarkA = 1; } - // compute UNSAT core - vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); - sat_solver_delete( pSat ); - if ( vCore == NULL ) + vPiToReg = Vec_IntAlloc( 1000 ); + Aig_ManForEachPi( p, pObj, i ) { - Saig_AbsFreeCnfs( vFrames ); - return NULL; + if ( pObj->fMarkA ) + { + pObj->fMarkA = 0; + continue; + } + if ( i < Saig_ManPiNum(p) ) + Vec_IntPush( vPiToReg, -1 ); + else + Vec_IntPush( vPiToReg, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); } // collect registers - if ( fDynamic ) + Vec_IntForEachEntry( vFlopsNew, Entry, i ) { - vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); - Saig_AbsFreeCnfs( vFrames ); + iFlop = Vec_IntEntry( vPiToReg, Entry ); + assert( iFlop >= 0 ); + assert( iFlop < Aig_ManRegNum(p) ); + Vec_IntPush( vFlops, iFlop ); } - else + Vec_IntFree( vPiToReg ); + Vec_IntFree( vFlopsNew ); + + Vec_IntSort( vFlops, 0 ); + Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) + assert( Vec_IntEntry(vFlops, i-1) != Entry ); + + return Saig_ManAbstraction( p, vFlops ); +} + +/**Function************************************************************* + + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + 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 * pResult, * pTemp; + Cnf_Dat_t * pCnf; + Vec_Ptr_t * vFrames; + sat_solver * pSat; + Vec_Int_t * vCore; + Vec_Int_t * vFlops; + int Iter, clk = clock(), clk2 = clock(); + assert( Aig_ManRegNum(p) > 0 ); + Aig_ManSetPioNumbers( p ); + + if ( fSkipProof ) { - vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); - Cnf_DataFree( pCnf ); + assert( 0 ); + if ( fVerbose ) + printf( "Performing counter-example-based refinement.\n" ); +// vFlops = Vec_IntStartNatural( 100 ); +// Vec_IntPush( vFlops, 0 ); } - Vec_IntFree( vCore ); - if ( fVerbose ) + else { - printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); - PRT( "Time", clock() - clk ); + if ( fVerbose ) + printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); + if ( fDynamic ) + { + // create CNF for the frames + vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose ); + // create dynamic solver + pSat = Saig_AbsCreateSolverDyn( p, vFrames ); + } + else + { + // create CNF for the AIG + pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); + // create SAT solver for the unrolled AIG + pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + } + if ( fVerbose ) + { + printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); + PRT( "Time", clock() - clk2 ); + } + // compute UNSAT core + vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); + sat_solver_delete( pSat ); + if ( vCore == NULL ) + { + Saig_AbsFreeCnfs( vFrames ); + return NULL; + } + // collect registers + if ( fDynamic ) + { + vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); + Saig_AbsFreeCnfs( vFrames ); + } + else + { + vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); + Cnf_DataFree( pCnf ); + } + Vec_IntFree( vCore ); + if ( fVerbose ) + { + printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); + PRT( "Time", clock() - clk ); + } } +/* // extend the abstraction if ( fExtend ) { @@ -702,8 +844,33 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, if ( fVerbose ) printf( " %d flops.\n", Vec_IntSize(vFlops) ); } +*/ // create the resulting AIG pResult = Saig_ManAbstraction( p, vFlops ); + + if ( fExtend ) + { + if ( !fVerbose ) + { + printf( "Init : " ); + Aig_ManPrintStats( pResult ); + } + printf( "Refining abstraction...\n" ); + for ( Iter = 0; ; Iter++ ) + { + pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose ); + if ( pTemp == NULL ) + break; + Aig_ManStop( pResult ); + pResult = pTemp; + printf( "%4d : ", Iter ); + if ( !fVerbose ) + Aig_ManPrintStats( pResult ); + else + printf( " -----------------------------------------------------\n" ); + } + } + Vec_IntFree( vFlops ); return pResult; } |