From d2b735f794575ce0f10f01bba1255cf1dc3b8aaf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Oct 2008 08:01:00 -0700 Subject: Version abc81025 --- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 1 + src/aig/saig/saigBmc.c | 550 +++++++++++++++++++++++++++++------------------ src/aig/saig/saigBmc2.c | 314 +++++++++++++++++++++++++++ src/aig/saig/saigMiter.c | 159 +++++++++++++- src/aig/saig/saigSynch.c | 1 + 6 files changed, 809 insertions(+), 217 deletions(-) create mode 100644 src/aig/saig/saigBmc2.c (limited to 'src/aig/saig') diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 48d91438..7063bd2a 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,5 +1,6 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigBmc.c \ + src/aig/saig/saigBmc2.c \ src/aig/saig/saigCone.c \ src/aig/saig/saigDup.c \ src/aig/saig/saigHaig.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f0c8fb54..a6f5631b 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -99,6 +99,7 @@ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, in extern Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames ); extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ); +extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 5776cd4a..0bbf63f9 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -26,62 +26,172 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define AIG_VISITED ((Aig_Obj_t *)(PORT_PTRUINT_T)1) + +typedef struct Saig_Bmc_t_ Saig_Bmc_t; +struct Saig_Bmc_t_ +{ + // parameters + int nFramesMax; // the max number of timeframes to consider + int nConfMaxOne; // the max number of conflicts at a target + int nConfMaxAll; // the max number of conflicts for all targets + int nNodesMax; // the max number of nodes to add + int fVerbose; // enables verbose output + // AIG managers + Aig_Man_t * pAig; // the user's AIG manager + Aig_Man_t * pFrm; // Frames manager + Vec_Ptr_t * vVisited; // nodes visited in Frames + // node mapping + int nObjs; // the largest number of an AIG object + Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes + // SAT solver + sat_solver * pSat; // SAT solver + Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables + int nSatVars; // the number of used SAT variables + Vec_Ptr_t * vTargets; // targets to be solved in this interval + int iFramelast; // last frame + int iOutputLast; // last output +}; + +static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); } +static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); } + +static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } +static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } + +static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Create timeframes of the manager for BMC.] + Synopsis [Create manager.] - Description [The resulting manager is combinational. POs correspond to \ - the property outputs in each time-frame.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) { - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f; - assert( Saig_ManRegNum(pAig) > 0 ); - pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs + Saig_Bmc_t * p; + Aig_Obj_t * pObj; + int i, Lit; + assert( Aig_ManRegNum(pAig) > 0 ); + p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) ); + memset( p, 0, sizeof(Saig_Bmc_t) ); + // set parameters + p->nFramesMax = 1000000; + p->nConfMaxOne = nConfMaxOne; + p->nConfMaxAll = nConfMaxAll; + p->nNodesMax = nNodesMax; + p->fVerbose = fVerbose; + p->pAig = pAig; + p->nObjs = Aig_ManObjNumMax(pAig); + // create node and variable mappings + p->vAig2Frm = Vec_PtrAlloc( 0 ); + Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL ); + p->vObj2Var = Vec_IntAlloc( 0 ); + Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 ); + // start the AIG manager and map primary inputs + p->pFrm = Aig_ManStart( 5 * p->nObjs ); Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ManConst0( pFrames ); - // add timeframes - for ( f = 0; f < nFrames; f++ ) + Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); + // create SAT solver + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 2000 ); + p->nSatVars = 1; + Lit = toLit( p->nSatVars ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ ); + // other data structures + p->vTargets = Vec_PtrAlloc( 0 ); + p->vVisited = Vec_PtrAlloc( 0 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Delete manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcManStop( Saig_Bmc_t * p ) +{ + Aig_ManStop( p->pFrm ); + Vec_PtrFree( p->vAig2Frm ); + Vec_IntFree( p->vObj2Var ); + sat_solver_delete( p->pSat ); + Vec_PtrFree( p->vTargets ); + Vec_PtrFree( p->vVisited ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Explores the possibility of constructing the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) +{ + Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig); + pRes = Saig_BmcObjFrame( p, pObj, i ); + if ( pRes != NULL ) + return pRes; + if ( Saig_ObjIsPi( p->pAig, pObj ) ) + pRes = AIG_VISITED; + else if ( Saig_ObjIsLo( p->pAig, pObj ) ) + pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); + else if ( Aig_ObjIsPo( pObj ) ) { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create POs for this frame - Saig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; + pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i ); + if ( pRes != AIG_VISITED ) + pRes = Saig_BmcObjChild0( p, pObj, i ); + } + else + { + p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i ); + if ( p0 != AIG_VISITED ) + p0 = Saig_BmcObjChild0( p, pObj, i ); + p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i ); + if ( p1 != AIG_VISITED ) + p1 = Saig_BmcObjChild1( p, pObj, i ); + + if ( p0 == Aig_Not(p1) ) + pRes = Aig_Not(pConst1); + else if ( Aig_Regular(p0) == pConst1 ) + pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1); + else if ( Aig_Regular(p1) == pConst1 ) + pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1); + else + pRes = AIG_VISITED; + + if ( pRes != pConst1 && pRes != Aig_Not(pConst1) ) + pRes = AIG_VISITED; } - Aig_ManCleanup( pFrames ); - return pFrames; + Saig_BmcObjSetFrame( p, pObj, i, pRes ); + return pRes; } /**Function************************************************************* - Synopsis [Returns the number of internal nodes that are not counted yet.] + Synopsis [Performs the actual construction of the output.] Description [] @@ -90,81 +200,70 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { - if ( !Aig_ObjIsNode(pObj) ) - return 0; - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - return 0; - Aig_ObjSetTravIdCurrent(p, pObj); - return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + - Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); + Aig_Obj_t * pRes; + pRes = Saig_BmcObjFrame( p, pObj, i ); + assert( pRes != NULL ); + if ( pRes != AIG_VISITED ) + return pRes; + if ( Saig_ObjIsPi( p->pAig, pObj ) ) + pRes = Aig_ObjCreatePi(p->pFrm); + else if ( Saig_ObjIsLo( p->pAig, pObj ) ) + pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); + else if ( Aig_ObjIsPo( pObj ) ) + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i ); + pRes = Saig_BmcObjChild0( p, pObj, i ); + } + else + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i ); + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i ); + pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + } + Saig_BmcObjSetFrame( p, pObj, i, pRes ); + return pRes; } /**Function************************************************************* - Synopsis [Create timeframes of the manager for BMC.] + Synopsis [Adds new AIG nodes to the frames.] - Description [The resulting manager is combinational. POs correspond to - the property outputs in each time-frame. - The unrolling is stopped as soon as the number of nodes in the frames - exceeds the given maximum size.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +void Saig_BmcInterval( Saig_Bmc_t * p ) { - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; - int i, f, Counter = 0; - assert( Saig_ManRegNum(pAig) > 0 ); - pFrames = Aig_ManStart( nSizeMax ); - Aig_ManIncrementTravId( pFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ManConst0( pFrames ); - // add timeframes - Counter = 0; - for ( f = 0; f < nFrames; f++ ) + Aig_Obj_t * pTarget, * pObj; + int i, nNodes = Aig_ManNodeNum( p->pFrm ); + Vec_PtrClear( p->vTargets ); + for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 ) { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create POs for this frame - Saig_ManForEachPo( pAig, pObj, i ) + if ( p->iOutputLast == 0 ) { - pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); } - if ( Counter >= nSizeMax ) + for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ ) { - Aig_ManCleanup( pFrames ); - return pFrames; + if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax ) + return; + Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); + pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); + Vec_PtrPush( p->vTargets, pTarget ); } - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; } - Aig_ManCleanup( pFrames ); - return pFrames; } /**Function************************************************************* - Synopsis [Performs BMC for the given AIG.] + Synopsis [Performs the actual construction of the output.] Description [] @@ -173,140 +272,179 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj ) { - sat_solver * pSat; - Cnf_Dat_t * pCnf; - Aig_Man_t * pFrames, * pAigTemp; - Aig_Obj_t * pObj; - int status, clk, Lit, i, RetValue = 1; - // derive the timeframes - clk = clock(); - if ( nSizeMax > 0 ) - { - pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); - nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); - } - else - pFrames = Saig_ManFramesBmc( pAig, nFrames ); - if ( piFrame ) - *piFrame = nFrames; - if ( fVerbose ) + if ( pObj->pData ) + return pObj->pData; + Vec_PtrPush( p->vVisited, pObj ); + if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) ) + return pObj->pData = Aig_ObjCreatePi(pNew); + Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) ); + Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Creates AIG of the newly added nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i; + pNew = Aig_ManStart( p->nNodesMax ); + Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew); + Vec_PtrClear( p->vVisited ); + Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) ); + Vec_PtrForEachEntry( p->vTargets, pObj, i ) { - printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", - Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), - Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); - printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", - nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), - Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) ); + Aig_ObjCreatePo( pNew, pObjNew ); } - // rewrite the timeframes - if ( fRewrite ) + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derives CNF for the newly added nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) +{ + Aig_Obj_t * pObj, * pObjNew; + int i, Lits[2], VarNumOld, VarNumNew; + Vec_PtrForEachEntry( p->vVisited, pObj, i ) { - clk = clock(); -// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 ); - pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 ); - Aig_ManStop( pAigTemp ); - if ( fVerbose ) + pObjNew = pObj->pData; + pObj->pData = NULL; + VarNumNew = pCnf->pVarNums[ pObjNew->Id ]; + if ( VarNumNew == -1 ) + continue; + VarNumOld = Saig_BmcSatNum( p, pObj ); + if ( VarNumOld == 0 ) { - printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", - Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + Saig_BmcSetSatNum( p, pObj, VarNumNew ); + continue; } - } - // create the SAT solver - clk = clock(); - pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); - pSat = sat_solver_new(); - sat_solver_setnvars( pSat, pCnf->nVars ); - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + // add clauses connecting existing variables + Lits[0] = toLitCond( VarNumOld, 0 ); + Lits[1] = toLitCond( VarNumNew, 1 ); + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( VarNumOld, 1 ); + Lits[1] = toLitCond( VarNumNew, 0 ); + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) assert( 0 ); } - if ( fVerbose ) + // add CNF to the SAT solver + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + break; + if ( i < pCnf->nClauses ) + printf( "SAT solver became UNSAT after adding clauses.\n" ); +} + +/**Function************************************************************* + + Synopsis [Solves targets with the given resource limit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_BmcSolveTargets( Saig_Bmc_t * p ) +{ + Aig_Obj_t * pObj; + int i, VarNum, Lit, RetValue; + assert( Vec_PtrSize(p->vTargets) > 0 ); + Vec_PtrForEachEntry( p->vTargets, pObj, i ) { - printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + return l_Undef; + VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); + Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); + RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_False ) // unsat + continue; + if ( RetValue == l_Undef ) // undecided + return l_Undef; + // generate counter-example + return l_True; } - status = sat_solver_simplify(pSat); - if ( status == 0 ) + return l_False; +} + +/**Function************************************************************* + + Synopsis [Performs BMC with the given parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) +{ + Saig_Bmc_t * p; + Aig_Man_t * pNew; + Cnf_Dat_t * pCnf; + int RetValue, clk = clock(); + p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose ); + while ( 1 ) { - if ( fVerbose ) - { - printf( "The BMC problem is trivially UNSAT\n" ); - fflush( stdout ); - } + // add new logic slice to frames + Saig_BmcInterval( p ); + if ( Vec_PtrSize(p->vTargets) == 0 ) + break; + // convert logic slice into new AIG + pNew = Saig_BmcIntervalToAig( p ); + // derive CNF for the new AIG + pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) ); + Cnf_DataLift( pCnf, p->nSatVars ); + p->nSatVars += pCnf->nVars; + // add this CNF to the solver + Saig_BmcLoadCnf( p, pCnf ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pNew ); + // solve the targets + RetValue = Saig_BmcSolveTargets( p ); + if ( RetValue != l_False ) + break; } + if ( RetValue == l_True ) + printf( "BMC failed for output %d in frame %d. ", p->iOutputLast, p->iFramelast ); + else // if ( RetValue == l_False || RetValue == l_Undef ) + printf( "BMC completed for %d timeframes. ", p->iFramelast ); + PRT( "Time", clock() - clk ); + if ( p->iFramelast >= p->nFramesMax ) + printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); + else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); else - { - int clkPart = clock(); - Aig_ManForEachPo( pFrames, pObj, i ) - { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( fVerbose ) - { - printf( "Solving output %2d of frame %3d ... \r", - i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - } - clk = clock(); - status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) - { - printf( "Solved %2d outputs of frame %3d. ", - Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); - PRT( "T", clock() - clkPart ); - clkPart = clock(); - fflush( stdout ); - } - if ( status == l_False ) - { -/* - Lit = lit_neg( Lit ); - RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); - assert( RetValue ); - if ( pSat->qtail != pSat->qhead ) - { - RetValue = sat_solver_simplify(pSat); - assert( RetValue ); - } -*/ - } - else if ( status == l_True ) - { - extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); - Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); - int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pModel[Aig_ManPiNum(pFrames)] = pObj->Id; - pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); - free( pModel ); - Vec_IntFree( vCiIds ); - -// if ( piFrame ) -// *piFrame = i / Saig_ManPoNum(pAig); - RetValue = 0; - break; - } - else - { - if ( piFrame ) - *piFrame = i / Saig_ManPoNum(pAig); - RetValue = -1; - break; - } - } - } - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - Aig_ManStop( pFrames ); - return RetValue; + printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + Saig_BmcManStop( p ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c new file mode 100644 index 00000000..5776cd4a --- /dev/null +++ b/src/aig/saig/saigBmc2.c @@ -0,0 +1,314 @@ +/**CFile**************************************************************** + + FileName [saigBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Simple BMC package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "cnf.h" +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. POs correspond to \ + the property outputs in each time-frame.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Returns the number of internal nodes that are not counted yet.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( !Aig_ObjIsNode(pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + + Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. POs correspond to + the property outputs in each time-frame. + The unrolling is stopped as soon as the number of nodes in the frames + exceeds the given maximum size.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; + int i, f, Counter = 0; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( nSizeMax ); + Aig_ManIncrementTravId( pFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + Counter = 0; + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + { + pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + } + if ( Counter >= nSizeMax ) + { + Aig_ManCleanup( pFrames ); + return pFrames; + } + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Performs BMC for the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Man_t * pFrames, * pAigTemp; + Aig_Obj_t * pObj; + int status, clk, Lit, i, RetValue = 1; + // derive the timeframes + clk = clock(); + if ( nSizeMax > 0 ) + { + pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); + nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); + } + else + pFrames = Saig_ManFramesBmc( pAig, nFrames ); + if ( piFrame ) + *piFrame = nFrames; + if ( fVerbose ) + { + printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", + nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + // rewrite the timeframes + if ( fRewrite ) + { + clk = clock(); +// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 ); + pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 ); + Aig_ManStop( pAigTemp ); + if ( fVerbose ) + { + printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + } + // create the SAT solver + clk = clock(); + pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + } + if ( fVerbose ) + { + printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + if ( fVerbose ) + { + printf( "The BMC problem is trivially UNSAT\n" ); + fflush( stdout ); + } + } + else + { + int clkPart = clock(); + Aig_ManForEachPo( pFrames, pObj, i ) + { + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( fVerbose ) + { + printf( "Solving output %2d of frame %3d ... \r", + i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + } + clk = clock(); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) + { + printf( "Solved %2d outputs of frame %3d. ", + Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); + PRT( "T", clock() - clkPart ); + clkPart = clock(); + fflush( stdout ); + } + if ( status == l_False ) + { +/* + Lit = lit_neg( Lit ); + RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue ); + if ( pSat->qtail != pSat->qhead ) + { + RetValue = sat_solver_simplify(pSat); + assert( RetValue ); + } +*/ + } + else if ( status == l_True ) + { + extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); + Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); + int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + pModel[Aig_ManPiNum(pFrames)] = pObj->Id; + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); + free( pModel ); + Vec_IntFree( vCiIds ); + +// if ( piFrame ) +// *piFrame = i / Saig_ManPoNum(pAig); + RetValue = 0; + break; + } + else + { + if ( piFrame ) + *piFrame = i / Saig_ManPoNum(pAig); + RetValue = -1; + break; + } + } + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 5efcd24d..cc71f371 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -49,6 +49,8 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); pNew->pName = Aig_UtilStrsav( "miter" ); + Aig_ManCleanData( p0 ); + Aig_ManCleanData( p1 ); // map constant nodes Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); @@ -85,7 +87,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); // cleanup Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) ); - Aig_ManCleanup( pNew ); +// Aig_ManCleanup( pNew ); return pNew; } @@ -184,6 +186,9 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); break; } + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); // save register inputs Saig_ManForEachLi( pAig, pObj, i ) pObj->pData = Aig_ObjChild0Copy(pObj); @@ -213,7 +218,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet ) +Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet ) { Aig_Man_t * pNew, * pCopy; Aig_Obj_t * pObj; @@ -250,7 +255,7 @@ Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) +Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) { Aig_Man_t * pNew, * pCopy; Aig_Obj_t * pObj; @@ -337,6 +342,79 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi Vec_PtrFree( vSet1 ); return 0; } + if ( Aig_ObjFaninC0(pObj) ) + pObj0 = Aig_Not(pObj0); + +// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); + if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) + { + Vec_PtrPush( vSet0, pObj0 ); + Vec_PtrPush( vSet1, pObj1 ); + } + else + { + Vec_PtrPush( vSet0, pObj1 ); + Vec_PtrPush( vSet1, pObj0 ); + } + } +// printf( "Miter has %d constant outputs.\n", Counter ); +// printf( "\n" ); + if ( ppAig0 ) + { + *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); + FREE( (*ppAig0)->pName ); + (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + } + if ( ppAig1 ) + { + *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); + FREE( (*ppAig1)->pName ); + (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + } + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG to have constant-0 initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) +{ + Vec_Ptr_t * vSet0, * vSet1; + Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1; + int i, Counter = 0; + assert( Saig_ManRegNum(p) % 2 == 0 ); + vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + Saig_ManForEachPo( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsConst1( pFanin ) ) + { + if ( !Aig_ObjFaninC0(pObj) ) + printf( "The output number %d of the miter is constant 1.\n", i ); + Counter++; + continue; + } + if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) + { + printf( "The miter cannot be demitered.\n" ); + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + return 0; + } + if ( Aig_ObjFaninC0(pObj) ) + pObj0 = Aig_Not(pObj0); + // printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) { @@ -353,13 +431,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi // printf( "\n" ); if ( ppAig0 ) { - *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); + *ppAig0 = Aig_ManDupNodesAll( p, vSet0 ); FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { - *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); + *ppAig1 = Aig_ManDupNodesAll( p, vSet1 ); FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } @@ -525,14 +603,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) if ( ppAig0 ) { assert( 0 ); - *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); // not ready + *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { assert( 0 ); - *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); // not ready + *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } @@ -566,6 +644,42 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra return pMiter; } + +/**Function************************************************************* + + Synopsis [Resimulates counter-example and returns the failed output number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ) +{ + Aig_Obj_t * pObj; + int i, RetValue = -1; + *pnOutputs = 0; + Aig_ManConst1(p)->fMarkA = 1; + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkA = pModel[i]; + Aig_ManForEachNode( p, pObj, i ) + pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & + ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) ); + Aig_ManForEachPo( p, pObj, i ) + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj); + Aig_ManForEachPo( p, pObj, i ) + if ( pObj->fMarkA ) + { + if ( RetValue == -1 ) + RetValue = i; + (*pnOutputs)++; + } + Aig_ManCleanMarkA(p); + return RetValue; +} + /**Function************************************************************* Synopsis [Reduces SEC to CEC for the special case of seq synthesis.] @@ -578,12 +692,16 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra SeeAlso [] ***********************************************************************/ -int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose ) +int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose ) { extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); - int nFrames = 2; // modify to enable comparison over any number of frames + int iOut, nOuts; Aig_Man_t * pMiterCec; int RetValue, clkTotal = clock(); + Aig_ManPrintStats( pPart0 ); + Aig_ManPrintStats( pPart1 ); +// Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); +// Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) { @@ -605,7 +723,6 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose ) // transfer model if given // if ( pNtk2 == NULL ) // pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL; - Aig_ManStop( pMiterCec ); // report the miter if ( RetValue == 1 ) { @@ -616,6 +733,24 @@ PRT( "Time", clock() - clkTotal ); { printf( "Networks are NOT EQUIVALENT. " ); PRT( "Time", clock() - clkTotal ); + if ( pMiterCec->pData == NULL ) + printf( "Counter-example is not available.\n" ); + else + { + iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts ); + if ( iOut == -1 ) + printf( "Counter-example verification has failed.\n" ); + else + { + if ( iOut < Saig_ManPoNum(pPart0) * nFrames ) + printf( "Primary output %d has failed in frame %d.\n", + iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) ); + else + printf( "Flop input %d has failed in the last frame.\n", + iOut - Saig_ManPoNum(pPart0) * nFrames ); + printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts ); + } + } } else { @@ -623,6 +758,7 @@ PRT( "Time", clock() - clkTotal ); PRT( "Time", clock() - clkTotal ); } fflush( stdout ); + Aig_ManStop( pMiterCec ); return RetValue; } @@ -639,6 +775,7 @@ PRT( "Time", clock() - clkTotal ); ***********************************************************************/ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ) { + int nFrames = 2; // modify to enable comparison over any number of frames Aig_Man_t * pPart0, * pPart1; int RetValue; if ( fVerbose ) @@ -657,7 +794,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ) // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); // printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); } - RetValue = Ssw_SecSpecial( pPart0, pPart1, fVerbose ); + RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose ); Aig_ManStop( pPart0 ); Aig_ManStop( pPart1 ); return RetValue; diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index eb0fefc9..c52f2f48 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -632,6 +632,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, pAig1z = Saig_ManDupInitZero( pAig1 ); pAig2z = Saig_ManDupInitZero( pAig2 ); pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 ); + Aig_ManCleanup( pMiter ); Aig_ManStop( pAig1z ); Aig_ManStop( pAig2z ); -- cgit v1.2.3