diff options
Diffstat (limited to 'src/aig/saig/saigAbsPba.c')
| -rw-r--r-- | src/aig/saig/saigAbsPba.c | 374 |
1 files changed, 0 insertions, 374 deletions
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c deleted file mode 100644 index 34e1decf..00000000 --- a/src/aig/saig/saigAbsPba.c +++ /dev/null @@ -1,374 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigAbsPba.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Proof-based abstraction.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigAbsPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "sat/cnf/cnf.h" -#include "sat/bsat/satSolver.h" -#include "aig/gia/giaAig.h" - -ABC_NAMESPACE_IMPL_START - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Collect nodes in the unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots ) -{ - if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsCo(pObj) ) - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); - else if ( Aig_ObjIsNode(pObj) ) - { - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots ); - } - if ( vRoots && Saig_ObjIsLo( pAig, pObj ) ) - Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) ); - Vec_IntPush( vObjs, Aig_ObjId(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Derives unrolled timeframes for PBA.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap ) -{ - Aig_Man_t * pFrames; // unrolled timeframes - Vec_Vec_t * vFrameCos; // the list of COs per frame - Vec_Vec_t * vFrameObjs; // the list of objects per frame - Vec_Int_t * vRoots, * vObjs; - Aig_Obj_t * pObj, * pObjNew; - int i, f; - assert( nStart <= nFrames ); - // collect COs and Objs visited in each frame - vFrameCos = Vec_VecStart( nFrames ); - vFrameObjs = Vec_VecStart( nFrames ); - for ( f = nFrames-1; f >= 0; f-- ) - { - // add POs of this frame - vRoots = Vec_VecEntryInt( vFrameCos, f ); - Saig_ManForEachPo( pAig, pObj, i ) - Vec_IntPush( vRoots, Aig_ObjId(pObj) ); - // collect nodes starting from the roots - Aig_ManIncrementTravId( pAig ); - Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) - Saig_ManUnrollForPba_rec( pAig, pObj, - Vec_VecEntryInt( vFrameObjs, f ), - (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); - } - // derive unrolled timeframes - pFrames = Aig_ManStart( 10000 ); - pFrames->pName = Abc_UtilStrsav( pAig->pName ); - pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); - // create activation variables - Saig_ManForEachLo( pAig, pObj, i ) - Aig_ObjCreateCi( pFrames ); - // initialize the flops - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,i), Aig_ObjCreateCi(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++ ) - { - // construct - vObjs = Vec_VecEntryInt( vFrameObjs, f ); - Aig_ManForEachObjVec( vObjs, pAig, pObj, i ) - { - if ( Aig_ObjIsNode(pObj) ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else if ( Aig_ObjIsCo(pObj) ) - pObj->pData = Aig_ObjChild0Copy(pObj); - else if ( Saig_ObjIsPi(pAig, pObj) ) - { - Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjCioId(pObj), Aig_ManCiNum(pFrames) ); - pObj->pData = Aig_ObjCreateCi( pFrames ); - } - else if ( Aig_ObjIsConst1(pObj) ) - pObj->pData = Aig_ManConst1(pFrames); - else if ( !Saig_ObjIsLo(pAig, pObj) ) - assert( 0 ); - } - // create output - if ( f >= nStart ) - { - Saig_ManForEachPo( pAig, pObj, i ) - pObjNew = Aig_Or( pFrames, pObjNew, (Aig_Obj_t *)pObj->pData ); - } - // transfer - if ( f == nFrames - 1 ) - break; - vRoots = Vec_VecEntryInt( vFrameCos, f ); - Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) - { - if ( Saig_ObjIsLi(pAig, pObj) ) - { - int iFlopNum = Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig); - assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); - Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); - } - } - } - // cleanup - Vec_VecFree( vFrameCos ); - Vec_VecFree( vFrameObjs ); - // create output - Aig_ObjCreateCo( pFrames, pObjNew ); - Aig_ManSetRegNum( pFrames, 0 ); - // finallize - Aig_ManCleanup( pFrames ); - 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; - Aig_Obj_t * pObj, * pObjRi, * pObjRo; - int i, f, Entry, iBit = 0; - pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); - pCex->iPo = -1; - pCex->iFrame = -1; - Vec_IntForEachEntry( vPiVarMap, Entry, i ) - { - if ( Entry >= 0 ) - { - int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManCi(pCnf->pMan, Entry)) ]; - if ( sat_solver_var_value( pSat, iSatVar ) ) - Abc_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); - } - } - // check what frame has failed - Aig_ManCleanMarkB(pAig); - Aig_ManConst1(pAig)->fMarkB = 1; - Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); - for ( f = 0; f < nFrames; f++ ) - { - // compute new state - Saig_ManForEachPi( pAig, pObj, i ) - pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); - Aig_ManForEachNode( pAig, pObj, i ) - pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & - (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachCo( pAig, pObj, i ) - pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); - Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i ) - pObjRo->fMarkB = pObjRi->fMarkB; - // check the outputs - Saig_ManForEachPo( pAig, pObj, i ) - { - if ( pObj->fMarkB ) - { - pCex->iPo = i; - pCex->iFrame = f; - pCex->nBits = pCex->nRegs + pCex->nPis * (f+1); - break; - } - } - if ( i < Saig_ManPoNum(pAig) ) - break; - } - Aig_ManCleanMarkB(pAig); - if ( f == nFrames ) - { - Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - if ( !Saig_ManVerifyCex( pAig, pCex ) ) - { - Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - return pCex; -} - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int TimeLimit, int fVerbose, int * piFrame ) -{ - Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap; - Aig_Man_t * pFrames; - sat_solver * pSat; - Cnf_Dat_t * pCnf; - Aig_Obj_t * pObj; - int nCoreLits, * pCoreLits; - int i, iVar, RetValue; - clock_t clk; -if ( fVerbose ) -{ -if ( TimeLimit ) - printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFrames, TimeLimit ); -else - printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFrames ); -} - // create SAT solver -clk = clock(); - pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap ); -if ( fVerbose ) -Aig_ManPrintStats( pFrames ); -// pCnf = Cnf_DeriveSimple( pFrames, 0 ); -// pCnf = Cnf_Derive( pFrames, 0 ); - pCnf = Cnf_DeriveFast( pFrames, 0 ); - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - if ( pSat == NULL ) - { - Aig_ManStop( pFrames ); - Cnf_DataFree( pCnf ); - return NULL; - } -if ( fVerbose ) -Abc_PrintTime( 1, "Preparing", clock() - clk ); - - // map activation variables into flop numbers - vAssumps = Vec_IntAlloc( Aig_ManRegNum(pAig) ); - vMapVar2FF = Vec_IntStartFull( pCnf->nVars ); - Aig_ManForEachCi( pFrames, pObj, i ) - { - if ( i >= Aig_ManRegNum(pAig) ) - break; - iVar = pCnf->pVarNums[Aig_ObjId(pObj)]; - Vec_IntPush( vAssumps, toLitCond(iVar, 1) ); - Vec_IntWriteEntry( vMapVar2FF, iVar, i ); - } - - // set runtime limit - if ( TimeLimit ) - sat_solver_set_runtime_limit( pSat, TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0 ); - - // run SAT solver -clk = clock(); - RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), - (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); -if ( fVerbose ) -Abc_PrintTime( 1, "Solving", clock() - clk ); - if ( RetValue != l_False ) - { - if ( RetValue == l_True ) - { - Vec_Int_t * vAbsFfsToAdd; - ABC_FREE( pAig->pSeqModel ); - pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap ); - printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame ); - *piFrame = pAig->pSeqModel->iFrame; - // CEX is detected - refine the flops - vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose ); - if ( Vec_IntSize(vAbsFfsToAdd) == 0 ) - { - Vec_IntFree( vAbsFfsToAdd ); - goto finish; - } - if ( fVerbose ) - { - printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) ); - Abc_PrintTime( 1, "Time", clock() - clk ); - } - vFlops = vAbsFfsToAdd; - } - else - { - printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" ); - } - goto finish; - } - assert( RetValue == l_False ); // UNSAT - *piFrame = nFrames; - - // get relevant SAT literals - nCoreLits = sat_solver_final( pSat, &pCoreLits ); - assert( nCoreLits > 0 ); - if ( fVerbose ) - printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n", - nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts ); - - // collect flops - vFlops = Vec_IntAlloc( nCoreLits ); - for ( i = 0; i < nCoreLits; i++ ) - { - iVar = Vec_IntEntry( vMapVar2FF, lit_var(pCoreLits[i]) ); - assert( iVar >= 0 && iVar < Aig_ManRegNum(pAig) ); - Vec_IntPush( vFlops, iVar ); - } - Vec_IntSort( vFlops, 0 ); - - // cleanup -finish: - Vec_IntFree( vPiVarMap ); - Vec_IntFree( vAssumps ); - Vec_IntFree( vMapVar2FF ); - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - Aig_ManStop( pFrames ); - return vFlops; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |