| /**CFile**************************************************************** |
| |
| FileName [intCheck.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Interpolation engine.] |
| |
| Synopsis [Procedures to perform incremental inductive check.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 24, 2008.] |
| |
| Revision [$Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "intInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // checking manager |
| struct Inter_Check_t_ |
| { |
| int nFramesK; // the number of timeframes (K=1 for simple induction) |
| int nVars; // the current number of variables in the solver |
| Aig_Man_t * pFrames; // unrolled timeframes |
| Cnf_Dat_t * pCnf; // CNF of unrolled timeframes |
| sat_solver * pSat; // SAT solver |
| Vec_Int_t * vOrLits; // OR vars in each time frame (total number is the number nFrames) |
| Vec_Int_t * vAndLits; // AND vars in the last timeframe (total number is the number of interpolants) |
| Vec_Int_t * vAssLits; // assumptions (the union of the two) |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Create timeframes of the manager for interpolation.] |
| |
| Description [The resulting manager is combinational. The primary inputs |
| corresponding to register outputs are ordered first.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Inter_ManUnrollFrames( 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_ObjCreateCi( pFrames ); |
| // add timeframes |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // create PI nodes for this frame |
| Saig_ManForEachPi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pFrames ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // 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_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData ); |
| } |
| } |
| Aig_ManCleanup( pFrames ); |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [This procedure sets default values of interpolation parameters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ) |
| { |
| Inter_Check_t * p; |
| // create solver |
| p = ABC_CALLOC( Inter_Check_t, 1 ); |
| p->vOrLits = Vec_IntAlloc( 100 ); |
| p->vAndLits = Vec_IntAlloc( 100 ); |
| p->vAssLits = Vec_IntAlloc( 100 ); |
| // generate the timeframes |
| p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK ); |
| assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) ); |
| assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) ); |
| // convert to CNF |
| p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); |
| p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); |
| // assign parameters |
| p->nFramesK = nFramesK; |
| p->nVars = p->pCnf->nVars; |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [This procedure sets default values of interpolation parameters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Inter_CheckStop( Inter_Check_t * p ) |
| { |
| if ( p == NULL ) |
| return; |
| Vec_IntFree( p->vOrLits ); |
| Vec_IntFree( p->vAndLits ); |
| Vec_IntFree( p->vAssLits ); |
| Cnf_DataFree( p->pCnf ); |
| Aig_ManStop( p->pFrames ); |
| sat_solver_delete( p->pSat ); |
| ABC_FREE( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates one OR-gate: A + B = C.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Inter_CheckAddOrGate( Inter_Check_t * p, int iVarA, int iVarB, int iVarC ) |
| { |
| int RetValue, pLits[3]; |
| // add A => C or !A + C |
| pLits[0] = toLitCond(iVarA, 1); |
| pLits[1] = toLitCond(iVarC, 0); |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); |
| assert( RetValue ); |
| // add B => C or !B + C |
| pLits[0] = toLitCond(iVarB, 1); |
| pLits[1] = toLitCond(iVarC, 0); |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); |
| assert( RetValue ); |
| // add !A & !B => !C or A + B + !C |
| pLits[0] = toLitCond(iVarA, 0); |
| pLits[1] = toLitCond(iVarB, 0); |
| pLits[2] = toLitCond(iVarC, 1); |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); |
| assert( RetValue ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates equality: A = B.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB ) |
| { |
| int RetValue, pLits[3]; |
| // add A => B or !A + B |
| pLits[0] = toLitCond(iVarA, 1); |
| pLits[1] = toLitCond(iVarB, 0); |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); |
| assert( RetValue ); |
| // add B => A or !B + A |
| pLits[0] = toLitCond(iVarB, 1); |
| pLits[1] = toLitCond(iVarA, 0); |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); |
| assert( RetValue ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform the checking.] |
| |
| Description [Returns 1 if the check has passed.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, abctime nTimeNewOut ) |
| { |
| Aig_Obj_t * pObj, * pObj2; |
| int i, f, VarA, VarB, RetValue, Entry, status; |
| int nRegs = Aig_ManCiNum(pCnfInt->pMan); |
| assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs ); |
| assert( Aig_ManCoNum(pCnfInt->pMan) == 1 ); |
| |
| // set runtime limit |
| if ( nTimeNewOut ) |
| sat_solver_set_runtime_limit( p->pSat, nTimeNewOut ); |
| |
| // add clauses to the SAT solver |
| Cnf_DataLift( pCnfInt, p->nVars ); |
| for ( f = 0; f <= p->nFramesK; f++ ) |
| { |
| // add clauses to the solver |
| for ( i = 0; i < pCnfInt->nClauses; i++ ) |
| { |
| RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] ); |
| assert( RetValue ); |
| } |
| // add equality clauses for the flop variables |
| Aig_ManForEachCi( pCnfInt->pMan, pObj, i ) |
| { |
| pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i); |
| Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] ); |
| } |
| // add final clauses |
| if ( f < p->nFramesK ) |
| { |
| if ( f == Vec_IntSize(p->vOrLits) ) // find time here |
| { |
| // add literal to this frame |
| VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; |
| Vec_IntPush( p->vOrLits, VarB ); |
| } |
| else |
| { |
| // add OR gate for this frame |
| VarA = Vec_IntEntry( p->vOrLits, f ); |
| VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; |
| Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars ); |
| Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID! |
| } |
| } |
| else |
| { |
| // add AND gate for this frame |
| VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; |
| Vec_IntPush( p->vAndLits, VarB ); |
| } |
| // update variable IDs |
| Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 ); |
| p->nVars += pCnfInt->nVars + 1; |
| } |
| Cnf_DataLift( pCnfInt, -p->nVars ); |
| assert( Vec_IntSize(p->vOrLits) == p->nFramesK ); |
| |
| // collect the assumption literals |
| Vec_IntClear( p->vAssLits ); |
| Vec_IntForEachEntry( p->vOrLits, Entry, i ) |
| Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) ); |
| Vec_IntForEachEntry( p->vAndLits, Entry, i ) |
| Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) ); |
| /* |
| if ( pCnfInt->nLiterals == 3635 ) |
| { |
| int s = 0; |
| } |
| */ |
| // call the SAT solver |
| status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits), |
| Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits), |
| (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| |
| return status == l_False; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| ABC_NAMESPACE_IMPL_END |
| |
