diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/int/intCheck.c | 301 |
1 files changed, 301 insertions, 0 deletions
diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c new file mode 100644 index 00000000..564813f4 --- /dev/null +++ b/src/aig/int/intCheck.c @@ -0,0 +1,301 @@ +/**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_ObjCreatePi( 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) ); + // 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_ObjCreatePo( pFrames, 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_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) ); + assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) ); + // convert to CNF + p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(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 ) +{ + Aig_Obj_t * pObj, * pObj2; + int i, f, VarA, VarB, RetValue, Entry, status; + int nRegs = Aig_ManPiNum(pCnfInt->pMan); + assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs ); + assert( Aig_ManPoNum(pCnfInt->pMan) == 1 ); + + // 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_ManForEachPi( pCnfInt->pMan, pObj, i ) + { + pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(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_ManPo(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_ManPo(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_ManPo(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 + |