/**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