diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/pdr/module.make | 8 | ||||
-rw-r--r-- | src/sat/pdr/pdr.c | 53 | ||||
-rw-r--r-- | src/sat/pdr/pdr.h | 77 | ||||
-rw-r--r-- | src/sat/pdr/pdrClass.c | 223 | ||||
-rw-r--r-- | src/sat/pdr/pdrCnf.c | 354 | ||||
-rw-r--r-- | src/sat/pdr/pdrCore.c | 692 | ||||
-rw-r--r-- | src/sat/pdr/pdrInt.h | 187 | ||||
-rw-r--r-- | src/sat/pdr/pdrInv.c | 351 | ||||
-rw-r--r-- | src/sat/pdr/pdrMan.c | 190 | ||||
-rw-r--r-- | src/sat/pdr/pdrSat.c | 351 | ||||
-rw-r--r-- | src/sat/pdr/pdrTsim.c | 450 | ||||
-rw-r--r-- | src/sat/pdr/pdrUtil.c | 547 |
12 files changed, 3483 insertions, 0 deletions
diff --git a/src/sat/pdr/module.make b/src/sat/pdr/module.make new file mode 100644 index 00000000..5cf4491c --- /dev/null +++ b/src/sat/pdr/module.make @@ -0,0 +1,8 @@ +SRC += src/sat/pdr/pdr.c \ + src/sat/pdr/pdrCnf.c \ + src/sat/pdr/pdrCore.c \ + src/sat/pdr/pdrInv.c \ + src/sat/pdr/pdrMan.c \ + src/sat/pdr/pdrSat.c \ + src/sat/pdr/pdrTsim.c \ + src/sat/pdr/pdrUtil.c diff --git a/src/sat/pdr/pdr.c b/src/sat/pdr/pdr.c new file mode 100644 index 00000000..6bdf75b5 --- /dev/null +++ b/src/sat/pdr/pdr.c @@ -0,0 +1,53 @@ +/**CFile**************************************************************** + + FileName [pdr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h new file mode 100644 index 00000000..1099c621 --- /dev/null +++ b/src/sat/pdr/pdr.h @@ -0,0 +1,77 @@ +/**CFile**************************************************************** + + FileName [pdr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __PDR_H__ +#define __PDR_H__ + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Pdr_Par_t_ Pdr_Par_t; +struct Pdr_Par_t_ +{ + int iOutput; // zero-based number of primary output to solve + int nRecycle; // limit on vars for recycling + int nFrameMax; // limit on frame count + int nConfLimit; // limit on SAT solver conflicts + int nTimeOut; // timeout in seconds + int fTwoRounds; // use two rounds for generalization + int fMonoCnf; // monolythic CNF + int fDumpInv; // dump inductive invariant + int fShortest; // forces bug traces to be shortest + int fVerbose; // verbose output + int fVeryVerbose; // very verbose output +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== pdrCore.c ==========================================================*/ +extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); +extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); + + +ABC_NAMESPACE_HEADER_END + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c new file mode 100644 index 00000000..31449735 --- /dev/null +++ b/src/sat/pdr/pdrClass.c @@ -0,0 +1,223 @@ +/**CFile**************************************************************** + + FileName [pdrClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Equivalence classes of register outputs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs duplication with the variable map.] + + Description [Var map contains -1 if const0 and <reg_num> otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj; + int i, iReg; + assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) ); + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + // create CI mapping + Aig_ManCleanData( pAig ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pFrames); + Saig_ManForEachLo( pAig, pObj, i ) + { + iReg = Vec_IntEntry(vMap, i); + if ( iReg == -1 ) + pObj->pData = Aig_ManConst0(pFrames); + else + pObj->pData = Saig_ManLo(pAig, iReg)->pData; + } + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add output nodes + Aig_ManForEachPo( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + // finish off + Aig_ManCleanup( pFrames ); + Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Creates mapping of registers.] + + Description [Var map contains -1 if const0 and <reg_num> otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + Vec_Int_t * vMap; + int * pLit2Id, Lit, i; + pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 ); + for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ ) + pLit2Id[i] = -1; + vMap = Vec_IntAlloc( Aig_ManRegNum(p) ); + Saig_ManForEachLi( p, pObj, i ) + { + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) ) + { + Vec_IntPush( vMap, -1 ); + continue; + } + Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj); + if ( pLit2Id[Lit] < 0 ) // the first time + pLit2Id[Lit] = i; + Vec_IntPush( vMap, pLit2Id[Lit] ); + } + ABC_FREE( pLit2Id ); + return vMap; +} + +/**Function************************************************************* + + Synopsis [Counts reduced registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCountMap( Vec_Int_t * vMap ) +{ + int i, Entry, Counter = 0; + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry != i ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts reduced registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManPrintMap( Vec_Int_t * vMap ) +{ + Vec_Int_t * vMarks; + int f, i, iClass, Entry, Counter = 0; + printf( " Consts: " ); + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry == -1 ) + printf( "%d ", i ); + printf( "\n" ); + vMarks = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vMap, iClass, f ) + { + if ( iClass == -1 ) + continue; + if ( iClass == f ) + continue; + // check previous classes + if ( Vec_IntFind( vMarks, iClass ) >= 0 ) + continue; + Vec_IntPush( vMarks, iClass ); + // print class + printf( " Class %d : ", iClass ); + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry == iClass ) + printf( "%d ", i ); + printf( "\n" ); + } + Vec_IntFree( vMarks ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManEquivClasses( Aig_Man_t * pAig ) +{ + Vec_Int_t * vMap; + Aig_Man_t * pTemp; + int f, nFrames = 100; + assert( Saig_ManRegNum(pAig) > 0 ); + // start the map + vMap = Vec_IntAlloc( 0 ); + Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 ); + // iterate and print changes + for ( f = 0; f < nFrames; f++ ) + { + // implement variable map + pTemp = Pdr_ManRehashWithMap( pAig, vMap ); + // report the result + printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n", + f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap), + Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" ); + // recreate the map + Pdr_ManPrintMap( vMap ); + Vec_IntFree( vMap ); + vMap = Pdr_ManCreateMap( pTemp ); + Aig_ManStop( pTemp ); + if ( Pdr_ManCountMap(vMap) == 0 ) + break; + } + Vec_IntFree( vMap ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c new file mode 100644 index 00000000..b40ed6d9 --- /dev/null +++ b/src/sat/pdr/pdrCnf.c @@ -0,0 +1,354 @@ +/**CFile**************************************************************** + + FileName [pdrCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [CNF computation on demand.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrCnf.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + The CNF (p->pCnf2) is expressed in terms of object IDs. + Each node in the CNF is marked if it has clauses (p->pCnf2->pObj2Count[Id] > 0). + Each node in the CNF has the first clause (p->pCnf2->pObj2Clause) + and the number of clauses (p->pCnf2->pObj2Count). + Each node used in a CNF of any timeframe has its SAT var recorded. + Each frame has a reserve mapping of SAT variables into ObjIds. +*/ + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns SAT variable of the given object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) +{ + return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ]; +} + +/**Function************************************************************* + + Synopsis [Returns SAT variable of the given object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) +{ + assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 ); + if ( p->pvId2Vars[Aig_ObjId(pObj)] == NULL ) + p->pvId2Vars[Aig_ObjId(pObj)] = Vec_IntStart( 16 ); + if ( Vec_IntGetEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ) == 0 ) + { + sat_solver * pSat = Pdr_ManSolver(p, k); + Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k); + int iVarNew = Vec_IntSize( vVar2Ids ); + assert( iVarNew > 0 ); + Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) ); + Vec_IntWriteEntry( p->pvId2Vars[Aig_ObjId(pObj)], k, iVarNew ); + sat_solver_setnvars( pSat, iVarNew + 1 ); + if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output + { + int Lit = toLitCond( iVarNew, 1 ); + int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue == 1 ); + sat_solver_compress( pSat ); + } + } + return Vec_IntEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ); +} + +/**Function************************************************************* + + Synopsis [Recursively adds CNF for the given object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k); + int nVarCount = Vec_IntSize(vVar2Ids); + int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj ); + int * pLit, i, iVar, nClauses, iFirstClause, RetValue; + if ( nVarCount == Vec_IntSize(vVar2Ids) ) + return iVarThis; + assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) ); + if ( Aig_ObjIsPi(pObj) ) + return iVarThis; + nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; + iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; + assert( nClauses > 0 ); + pSat = Pdr_ManSolver(p, k); + vLits = Vec_IntAlloc( 16 ); + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + { + Vec_IntClear( vLits ); + for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) + { + iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)) ); + Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); + } + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + assert( RetValue ); + } + Vec_IntFree( vLits ); + return iVarThis; +} + +/**Function************************************************************* + + Synopsis [Returns SAT variable of the given object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) +{ + if ( p->pPars->fMonoCnf ) + return Pdr_ObjSatVar1( p, k, pObj ); + else + return Pdr_ObjSatVar2( p, k, pObj ); +} + + +/**Function************************************************************* + + Synopsis [Returns register number for the given SAT variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjRegNum1( Pdr_Man_t * p, int k, int iSatVar ) +{ + int RegId; + assert( iSatVar >= 0 ); + // consider the case of auxiliary variable + if ( iSatVar >= p->pCnf1->nVars ) + return -1; + // consider the case of register output + RegId = Vec_IntEntry( p->vVar2Reg, iSatVar ); + assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) ); + return RegId; +} + +/**Function************************************************************* + + Synopsis [Returns register number for the given SAT variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar ) +{ + Aig_Obj_t * pObj; + int ObjId; + Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k); + assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) ); + ObjId = Vec_IntEntry( vVar2Ids, iSatVar ); + if ( ObjId == -1 ) // activation variable + return -1; + pObj = Aig_ManObj( p->pAig, ObjId ); + if ( Saig_ObjIsLi( p->pAig, pObj ) ) + return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig); + assert( 0 ); // should be called for register inputs only + return -1; +} + +/**Function************************************************************* + + Synopsis [Returns register number for the given SAT variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ) +{ + if ( p->pPars->fMonoCnf ) + return Pdr_ObjRegNum1( p, k, iSatVar ); + else + return Pdr_ObjRegNum2( p, k, iSatVar ); +} + + +/**Function************************************************************* + + Synopsis [Returns the index of unused SAT variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManFreeVar( Pdr_Man_t * p, int k ) +{ + if ( p->pPars->fMonoCnf ) + return sat_solver_nvars( Pdr_ManSolver(p, k) ); + else + { + Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( p->vVar2Ids, k ); + Vec_IntPush( vVar2Ids, -1 ); + return Vec_IntSize( vVar2Ids ) - 1; + } +} + +/**Function************************************************************* + + Synopsis [Creates SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit ) +{ + sat_solver * pSat; + Aig_Obj_t * pObj; + int i; + if ( p->pCnf1 == NULL ) + { + int nRegs = p->pAig->nRegs; + p->pAig->nRegs = Aig_ManPoNum(p->pAig); + p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) ); + p->pAig->nRegs = nRegs; + assert( p->vVar2Reg == NULL ); + p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars ); + Saig_ManForEachLi( p->pAig, pObj, i ) + Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i ); + } + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf1, 1, fInit ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Creates SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit ) +{ + sat_solver * pSat; + Vec_Int_t * vVar2Ids; + int i, Entry; + if ( p->pCnf2 == NULL ) + { + p->pCnf2 = Cnf_DeriveOther( p->pAig ); + p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) ); + p->vVar2Ids = Vec_PtrAlloc( 256 ); + } + // update the variable mapping + vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( p->vVar2Ids, k ); + if ( vVar2Ids == NULL ) + { + vVar2Ids = Vec_IntAlloc( 500 ); + Vec_PtrWriteEntry( p->vVar2Ids, k, vVar2Ids ); + } + Vec_IntForEachEntry( vVar2Ids, Entry, i ) + { + if ( Entry == -1 ) + continue; + assert( Vec_IntEntry( p->pvId2Vars[Entry], k ) > 0 ); + Vec_IntWriteEntry( p->pvId2Vars[Entry], k, 0 ); + } + Vec_IntClear( vVar2Ids ); + Vec_IntPush( vVar2Ids, -1 ); + // start the SAT solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, 500 ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Creates SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit ) +{ + if ( p->pPars->fMonoCnf ) + return Pdr_ManNewSolver1( p, k, fInit ); + else + return Pdr_ManNewSolver2( p, k, fInit ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c new file mode 100644 index 00000000..f1c10443 --- /dev/null +++ b/src/sat/pdr/pdrCore.c @@ -0,0 +1,692 @@ +/**CFile**************************************************************** + + FileName [pdrCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the state could be blocked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) +{ + memset( pPars, 0, sizeof(Pdr_Par_t) ); + pPars->iOutput = -1; // zero-based output number + pPars->nRecycle = 300; // limit on vars for recycling + pPars->nFrameMax = 5000; // limit on number of timeframes + pPars->nTimeOut = 0; // timeout in seconds + pPars->nConfLimit = 100000; // limit on SAT solver conflicts + pPars->fTwoRounds = 0; // use two rounds for generalization + pPars->fMonoCnf = 0; // monolythic CNF + pPars->fDumpInv = 0; // dump inductive invariant + pPars->fShortest = 0; // forces bug traces to be shortest + pPars->fVerbose = 0; // verbose output + pPars->fVeryVerbose = 0; // very verbose output +} + +/**Function************************************************************* + + Synopsis [Reduces clause using analyzeFinal.] + + Description [Assumes that the SAT solver just terminated an UNSAT call.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + Pdr_Set_t * pCubeMin; + Vec_Int_t * vLits; + int i, Entry, nCoreLits, * pCoreLits; + // get relevant SAT literals + nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits); + // translate them into register literals and remove auxiliary + vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits ); + // skip if there is no improvement + if ( Vec_IntSize(vLits) == pCube->nLits ) + return NULL; + assert( Vec_IntSize(vLits) < pCube->nLits ); + // if the cube overlaps with init, add any literal + Vec_IntForEachEntry( vLits, Entry, i ) + if ( lit_sign(Entry) == 0 ) // positive literal + break; + if ( i == Vec_IntSize(vLits) ) // only negative literals + { + // add the first positive literal + for ( i = 0; i < pCube->nLits; i++ ) + if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal + { + Vec_IntPush( vLits, pCube->Lits[i] ); + break; + } + assert( i < pCube->nLits ); + } + // generate a starting cube + pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) ); + assert( !Pdr_SetIsInit(pCubeMin, -1) ); +/* + // make sure the cube works + { + int RetValue; + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); + assert( RetValue ); + } +*/ + return pCubeMin; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the state could be blocked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManPushClauses( Pdr_Man_t * p ) +{ + Pdr_Set_t * pTemp, * pCubeK, * pCubeK1; + Vec_Ptr_t * vArrayK, * vArrayK1; + int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1; + int Counter = 0; + int clk = clock(); + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax-1 ) + { + Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); + vArrayK1 = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, k+1 ); + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + Counter++; + + // remove cubes in the same frame that are contained by pCubeK + Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) + { + if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp + continue; + Pdr_SetDeref( pTemp ); + Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) ); + Vec_PtrPop(vArrayK); + m--; + } + + // check if the clause can be moved to the next frame + if ( !Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ) ) + continue; + + { + Pdr_Set_t * pCubeMin; + pCubeMin = Pdr_ManReduceClause( p, k, pCubeK ); + if ( pCubeMin != NULL ) + { +// printf( "%d ", pCubeK->nLits - pCubeMin->nLits ); + Pdr_SetDeref( pCubeK ); + pCubeK = pCubeMin; + } + } + + // if it can be moved, add it to the next frame + Pdr_ManSolverAddClause( p, k+1, pCubeK ); + // check if the clause subsumes others + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i ) + { + if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1 + continue; + Pdr_SetDeref( pCubeK1 ); + Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) ); + Vec_PtrPop(vArrayK1); + i--; + } + // add the last clause + Vec_PtrPush( vArrayK1, pCubeK ); + Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); + Vec_PtrPop(vArrayK); + j--; + } + if ( Vec_PtrSize(vArrayK) == 0 ) + RetValue = 1; + } + + // clean up the last one + vArrayK = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, kMax ); + Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + // remove cubes in the same frame that are contained by pCubeK + Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) + { + if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp + continue; +/* + printf( "===\n" ); + Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL ); + printf( "\n" ); + Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL ); + printf( "\n" ); +*/ + Pdr_SetDeref( pTemp ); + Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) ); + Vec_PtrPop(vArrayK); + m--; + } + } + p->tPush += clock() - clk; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the clause is contained in higher clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet ) +{ + Pdr_Set_t * pThis; + Vec_Ptr_t * vArrayK; + int i, j, kMax = Vec_PtrSize(p->vSolvers)-1; + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax ) + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j ) + if ( Pdr_SetContains( pSet, pThis ) ) + return 1; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Sorts literals by priority.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) +{ + int * pPrios = Vec_IntArray(p->vPrio); + int * pArray = p->pOrder; + int temp, i, j, best_i, nSize = pCube->nLits; + // initialize variable order + for ( i = 0; i < nSize; i++ ) + pArray[i] = i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) +// if ( pArray[j] < pArray[best_i] ) + if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) + best_i = j; + temp = pArray[i]; + pArray[i] = pArray[best_i]; + pArray[best_i] = temp; + } +/* + for ( i = 0; i < pCube->nLits; i++ ) + printf( "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] ); + printf( "\n" ); +*/ + return pArray; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if the state could be blocked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin ) +{ + Pdr_Set_t * pCubeMin, * pCubeTmp = NULL; + int i, j, n, Lit, RetValue, clk = clock(); + int * pOrder; + // if there is no induction, return + *ppCubeMin = NULL; + RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit ); + if ( RetValue == -1 ) + return -1; + if ( RetValue == 0 ) + { + p->tGeneral += clock() - clk; + return 0; + } + // reduce clause using assumptions +// pCubeMin = Pdr_SetDup( pCube ); + pCubeMin = Pdr_ManReduceClause( p, k, pCube ); + if ( pCubeMin == NULL ) + pCubeMin = Pdr_SetDup( pCube ); + + // sort literals by their occurences + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + + // try removing literals + for ( j = 0; j < pCubeMin->nLits; j++ ) + { + // use ordering +// i = j; + i = pOrder[j]; + + // check init state + assert( pCubeMin->Lits[i] != -1 ); + if ( Pdr_SetIsInit(pCubeMin, i) ) + continue; + // try removing this literal + Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + if ( RetValue == -1 ) + { + Pdr_SetDeref( pCubeMin ); + return -1; + } + pCubeMin->Lits[i] = Lit; + if ( RetValue == 0 ) + continue; + + // remove j-th entry + for ( n = j; n < pCubeMin->nLits-1; n++ ) + pOrder[n] = pOrder[n+1]; + j--; + + // success - update the cube + pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); + Pdr_SetDeref( pCubeTmp ); + assert( pCubeMin->nLits > 0 ); + i--; + + // get the ordering by decreasing priorit + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + } + + if ( p->pPars->fTwoRounds ) + for ( j = 0; j < pCubeMin->nLits; j++ ) + { + // use ordering +// i = j; + i = pOrder[j]; + + // check init state + assert( pCubeMin->Lits[i] != -1 ); + if ( Pdr_SetIsInit(pCubeMin, i) ) + continue; + // try removing this literal + Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + if ( RetValue == -1 ) + { + Pdr_SetDeref( pCubeMin ); + return -1; + } + pCubeMin->Lits[i] = Lit; + if ( RetValue == 0 ) + continue; + + // remove j-th entry + for ( n = j; n < pCubeMin->nLits-1; n++ ) + pOrder[n] = pOrder[n+1]; + j--; + + // success - update the cube + pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); + Pdr_SetDeref( pCubeTmp ); + assert( pCubeMin->nLits > 0 ); + i--; + + // get the ordering by decreasing priorit + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + } + + assert( ppCubeMin != NULL ); + *ppCubeMin = pCubeMin; + p->tGeneral += clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the state could be blocked.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) +{ + Pdr_Obl_t * pThis; + Pdr_Set_t * pPred, * pCubeMin; + int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0; + int kMax = Vec_PtrSize(p->vSolvers)-1, clk; + p->nBlocks++; + // create first proof obligation + assert( p->pQueue == NULL ); + pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref + Pdr_QueuePush( p, pThis ); + // try to solve it recursively + while ( !Pdr_QueueIsEmpty(p) ) + { + Counter++; + pThis = Pdr_QueueHead( p ); + if ( pThis->iFrame == 0 ) + return 0; // SAT + pThis = Pdr_QueuePop( p ); + assert( pThis->iFrame > 0 ); + assert( !Pdr_SetIsInit(pThis->pState, -1) ); + + clk = clock(); + if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) ) + { + p->tContain += clock() - clk; + Pdr_OblDeref( pThis ); + continue; + } + p->tContain += clock() - clk; + + // check if the cube is already contained + if ( Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState ) ) // cube is blocked by clauses in this frame + { + Pdr_OblDeref( pThis ); + continue; + } + + // check if the cube holds with relative induction + pCubeMin = NULL; + RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin ); + if ( RetValue == -1 ) + { + Pdr_OblDeref( pThis ); + return -1; + } + if ( RetValue ) // cube is blocked inductively in this frame + { + assert( pCubeMin != NULL ); + + // k is the last frame where pCubeMin holds + k = pThis->iFrame; + + // check other frames + assert( pPred == NULL ); + for ( k = pThis->iFrame; k < kMax; k++ ) + if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) ) + break; + + // add new clause + if ( p->pPars->fVeryVerbose ) + { + printf( "Adding cube " ); + Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL ); + printf( " to frame %d.\n", k ); + } + // set priority flops + for ( i = 0; i < pCubeMin->nLits; i++ ) + { + assert( pCubeMin->Lits[i] >= 0 ); + assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); + } + + Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref + p->nCubes++; + // add clause + for ( i = 1; i <= k; i++ ) + Pdr_ManSolverAddClause( p, i, pCubeMin ); + // schedule proof obligation + if ( k < kMax && !p->pPars->fShortest ) + { + pThis->iFrame = k+1; + pThis->prio = Prio--; + Pdr_QueuePush( p, pThis ); + } + else + { + Pdr_OblDeref( pThis ); + } + } + else + { + assert( pCubeMin == NULL ); + assert( pPred != NULL ); + pThis->prio = Prio--; + Pdr_QueuePush( p, pThis ); + + pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) ); + Pdr_QueuePush( p, pThis ); + } + + // check the timeout + if ( p->timeToStop && clock() >= p->timeToStop ) + return -1; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManSolveInt( Pdr_Man_t * p ) +{ + int fPrintClauses = 0; + Pdr_Set_t * pCube; + int k, RetValue = -1; + int clkTotal = clock(); + int clkStart = clock(); + p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut); + assert( Vec_PtrSize(p->vSolvers) == 0 ); + // create the first timeframe + Pdr_ManCreateSolver( p, (k = 0) ); + while ( 1 ) + { + p->nFrames = k; + assert( k == Vec_PtrSize(p->vSolvers)-1 ); + RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + return -1; + } + if ( RetValue == 0 ) + { + RetValue = Pdr_ManBlockCube( p, pCube ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + return -1; + } + if ( RetValue == 0 ) + { + if ( fPrintClauses ) + { + printf( "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + return 0; // SAT + } + } + else + { + // open a new timeframe + assert( pCube == NULL ); + Pdr_ManSetPropertyOutput( p, k ); + Pdr_ManCreateSolver( p, ++k ); + if ( fPrintClauses ) + { + printf( "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 0, clock() - clkStart ); + // push clauses into this timeframe + if ( Pdr_ManPushClauses( p ) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + Pdr_ManReportInvariant( p ); + Pdr_ManVerifyInvariant( p ); + if ( p->pPars->fDumpInv ) + Pdr_ManDumpClauses( p, (char *)"inv.pla" ); + return 1; // UNSAT + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + clkStart = clock(); + } + + // check the timeout + if ( p->timeToStop && clock() >= p->timeToStop ) + { + if ( fPrintClauses ) + { + printf( "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + return -1; + } + if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); + return -1; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex ) +{ + Pdr_Man_t * p; + int RetValue; + int clk = clock(); + p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL ); + RetValue = Pdr_ManSolveInt( p ); + *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); +// if ( *ppCex && pPars->fVerbose ) +// printf( "Found counter-example in frame %d after exploring %d frames.\n", +// (*ppCex)->iFrame, p->nFrames ); + p->tTotal += clock() - clk; + if ( pvPrioInit ) + { + *pvPrioInit = p->vPrio; + p->vPrio = NULL; + } + Pdr_ManStop( p ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) +{ +/* + Vec_Int_t * vPrioInit = NULL; + int RetValue, nTimeOut; + if ( pPars->nTimeOut > 0 ) + return Pdr_ManSolve_( pAig, pPars, NULL, ppCex ); + nTimeOut = pPars->nTimeOut; + pPars->nTimeOut = 10; + RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex ); + pPars->nTimeOut = nTimeOut; + if ( RetValue == -1 ) + RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex ); + Vec_IntFree( vPrioInit ); + return RetValue; +*/ + return Pdr_ManSolve_( pAig, pPars, NULL, ppCex ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h new file mode 100644 index 00000000..d0211278 --- /dev/null +++ b/src/sat/pdr/pdrInt.h @@ -0,0 +1,187 @@ +/**CFile**************************************************************** + + FileName [pdrInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __PDR_INT_H__ +#define __PDR_INT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "saig.h" +#include "cnf.h" +#include "satSolver.h" +#include "pdr.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Pdr_Set_t_ Pdr_Set_t; +struct Pdr_Set_t_ +{ + word Sign; // signature + int nRefs; // ref counter + short nTotal; // total literals + short nLits; // num flop literals + int Lits[0]; +}; + +typedef struct Pdr_Obl_t_ Pdr_Obl_t; +struct Pdr_Obl_t_ +{ + int iFrame; // time frame + int prio; // priority + int nRefs; // reference counter + Pdr_Set_t * pState; // state cube + Pdr_Obl_t * pNext; // next one + Pdr_Obl_t * pLink; // queue link +}; + +typedef struct Pdr_Man_t_ Pdr_Man_t; +struct Pdr_Man_t_ +{ + // input problem + Pdr_Par_t * pPars; // parameters + Aig_Man_t * pAig; // user's AIG + // static CNF representation + Cnf_Dat_t * pCnf1; // CNF for this AIG + Vec_Int_t * vVar2Reg; // mapping of SAT var into registers + // dynamic CNF representation + Cnf_Dat_t * pCnf2; // CNF for this AIG + Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var + Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId + // data representation + Vec_Ptr_t * vSolvers; // SAT solvers + Vec_Vec_t * vClauses; // clauses by timeframe + Pdr_Obl_t * pQueue; // proof obligations + int * pOrder; // ordering of the lits + Vec_Int_t * vActVars; // the counter of activation variables + // internal use + Vec_Int_t * vPrio; // priority flops + Vec_Int_t * vLits; // array of literals + Vec_Int_t * vCiObjs; // cone leaves + Vec_Int_t * vCoObjs; // cone roots + Vec_Int_t * vCiVals; // cone leaf values + Vec_Int_t * vCoVals; // cone root values + Vec_Int_t * vNodes; // cone nodes + Vec_Int_t * vUndo; // cone undos + Vec_Int_t * vVisits; // intermediate + Vec_Int_t * vCi2Rem; // CIs to be removed + Vec_Int_t * vRes; // final result + // statistics + int nBlocks; // the number of times blockState was called + int nObligs; // the number of proof obligations derived + int nCubes; // the number of cubes derived + int nCalls; // the number of SAT calls + int nCallsS; // the number of SAT calls (sat) + int nCallsU; // the number of SAT calls (unsat) + int nStarts; // the number of SAT solver restarts + int nFrames; // frames explored + // runtime + int timeStart; + int timeToStop; + // time stats + int tSat; + int tSatSat; + int tSatUnsat; + int tGeneral; + int tPush; + int tTsim; + int tContain; + int tCnf; + int tTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== pdrCex.c ==========================================================*/ +extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); +/*=== pdrCnf.c ==========================================================*/ +extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ); +extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); +extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k ); +extern sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit ); +/*=== pdrInv.c ==========================================================*/ +extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time ); +extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); +extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName ); +extern void Pdr_ManReportInvariant( Pdr_Man_t * p ); +extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p ); +/*=== pdrMan.c ==========================================================*/ +extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); +extern void Pdr_ManStop( Pdr_Man_t * p ); +extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); +/*=== pdrSat.c ==========================================================*/ +extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ); +extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ); +extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ); +extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext ); +extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray ); +extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); +extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues ); +extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); +extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ); +/*=== pdrTsim.c ==========================================================*/ +extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); +/*=== pdrUtil.c ==========================================================*/ +extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ); +extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ); +extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ); +extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ); +extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ); +extern void Pdr_SetDeref( Pdr_Set_t * p ); +extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); +extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove ); +extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); +extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); +extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); +extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); +extern void Pdr_OblDeref( Pdr_Obl_t * p ); +extern int Pdr_QueueIsEmpty( Pdr_Man_t * p ); +extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p ); +extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ); +extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ); +extern void Pdr_QueuePrint( Pdr_Man_t * p ); +extern void Pdr_QueueStop( Pdr_Man_t * p ); + +ABC_NAMESPACE_HEADER_END + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c new file mode 100644 index 00000000..184b6c4f --- /dev/null +++ b/src/sat/pdr/pdrInv.c @@ -0,0 +1,351 @@ +/**CFile**************************************************************** + + FileName [pdrInv.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Invariant computation, printing, verification.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time ) +{ + extern int Extra_Base10Log( unsigned int Num ); + static int PastSize; + Vec_Ptr_t * vVec; + int i, ThisSize, Length, LengthStart; + if ( Vec_PtrSize(p->vSolvers) < 2 ) + return; + // count the total length of the printout + Length = 0; + Vec_VecForEachLevel( p->vClauses, vVec, i ) + Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1); + // determine the starting point + LengthStart = ABC_MAX( 0, Length - 70 ); + printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 ); + ThisSize = 6; + if ( LengthStart > 0 ) + { + printf( " ..." ); + ThisSize += 4; + } + Length = 0; + Vec_VecForEachLevel( p->vClauses, vVec, i ) + { + if ( Length < LengthStart ) + { + Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1); + continue; + } + printf( " %d", Vec_PtrSize(vVec) ); + Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1); + ThisSize += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1); + } + if ( fClose ) + { + for ( i = 0; i < PastSize - ThisSize; i++ ) + printf( " " ); + printf( "\n" ); + } + else + { + printf( "\r" ); + PastSize = ThisSize; + } +// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC)); +} + +/**Function************************************************************* + + Synopsis [Counts how many times each flop appears in the set of cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) +{ + Vec_Int_t * vFlopCount; + Pdr_Set_t * pCube; + int i, n; + vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + for ( n = 0; n < pCube->nLits; n++ ) + { + assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) ); + Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 ); + } + return vFlopCount; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManFindInvariantStart( Pdr_Man_t * p ) +{ + Vec_Ptr_t * vArrayK; + int k, kMax = Vec_PtrSize(p->vSolvers)-1; + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax ) + if ( Vec_PtrSize(vArrayK) == 0 ) + return k; + return -1; +} + +/**Function************************************************************* + + Synopsis [Counts the number of variables used in the clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart ) +{ + Vec_Ptr_t * vResult; + Vec_Ptr_t * vArrayK; + Pdr_Set_t * pSet; + int i, j; + vResult = Vec_PtrAlloc( 100 ); + Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart ) + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j ) + Vec_PtrPush( vResult, pSet ); + return vResult; +} + +/**Function************************************************************* + + Synopsis [Counts the number of variables used in the clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart ) +{ + Vec_Int_t * vFlopCounts; + Vec_Ptr_t * vCubes; + int i, Entry, Counter = 0; + vCubes = Pdr_ManCollectCubes( p, kStart ); + vFlopCounts = Pdr_ManCountFlops( p, vCubes ); + Vec_IntForEachEntry( vFlopCounts, Entry, i ) + Counter += (Entry > 0); + Vec_IntFreeP( &vFlopCounts ); + Vec_PtrFree( vCubes ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ) +{ + Vec_Ptr_t * vArrayK; + Pdr_Set_t * pCube; + int i, k, Counter = 0; + Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart ) + { + Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i ) + { + printf( "C=%4d. F=%4d ", Counter++, k ); + Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL ); + printf( "\n" ); + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName ) +{ + int fUseSupp = 1; + FILE * pFile; + Vec_Int_t * vFlopCounts; + Vec_Ptr_t * vCubes; + Pdr_Set_t * pCube; + int i, kStart; + // create file + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing invariant.\n", pFileName ); + return; + } + // collect cubes + kStart = Pdr_ManFindInvariantStart( p ); + vCubes = Pdr_ManCollectCubes( p, kStart ); + Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); + // collect variable appearances + vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; + // output the header + fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName ); + fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() ); + fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) ); + fprintf( pFile, ".o 1\n" ); + fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) ); + // output cubes + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); + fprintf( pFile, " 1\n" ); + } + fprintf( pFile, ".e\n\n" ); + fclose( pFile ); + Vec_IntFreeP( &vFlopCounts ); + Vec_PtrFree( vCubes ); + printf( "Inductive invariant was written into file \"%s\".\n", pFileName ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManReportInvariant( Pdr_Man_t * p ) +{ + Vec_Ptr_t * vCubes; + int kStart = Pdr_ManFindInvariantStart( p ); + vCubes = Pdr_ManCollectCubes( p, kStart ); + printf( "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", + kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); + Vec_PtrFree( vCubes ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManVerifyInvariant( Pdr_Man_t * p ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + Vec_Ptr_t * vCubes; + Pdr_Set_t * pCube; + int i, kStart, kThis, RetValue, Counter = 0, clk = clock(); + // collect cubes used in the inductive invariant + kStart = Pdr_ManFindInvariantStart( p ); + vCubes = Pdr_ManCollectCubes( p, kStart ); + // create solver with the cubes + kThis = Vec_PtrSize(p->vSolvers); + pSat = Pdr_ManCreateSolver( p, kThis ); + // add the property output + Pdr_ManSetPropertyOutput( p, kThis ); + // add the clauses + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + assert( RetValue ); + sat_solver_compress( pSat ); + } + // check each clause + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + if ( RetValue != l_False ) + { + printf( "Verification of clause %d failed.\n", i ); + Counter++; + } + } + if ( Counter ) + printf( "Verification of %d clauses has failed.\n", Counter ); + else + { + printf( "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } +// sat_solver_delete( pSat ); + Vec_PtrFree( vCubes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c new file mode 100644 index 00000000..f33f6586 --- /dev/null +++ b/src/sat/pdr/pdrMan.c @@ -0,0 +1,190 @@ +/**CFile**************************************************************** + + FileName [pdr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Manager procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ) +{ + Pdr_Man_t * p; + p = ABC_CALLOC( Pdr_Man_t, 1 ); + p->pPars = pPars; + p->pAig = pAig; + p->vSolvers = Vec_PtrAlloc( 0 ); + p->vClauses = Vec_VecAlloc( 0 ); + p->pQueue = NULL; + p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) ); + p->vActVars = Vec_IntAlloc( 256 ); + // internal use + p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops + p->vLits = Vec_IntAlloc( 100 ); // array of literals + p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves + p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots + p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values + p->vCoVals = Vec_IntAlloc( 100 ); // cone root values + p->vNodes = Vec_IntAlloc( 100 ); // cone nodes + p->vUndo = Vec_IntAlloc( 100 ); // cone undos + p->vVisits = Vec_IntAlloc( 100 ); // intermediate + p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed + p->vRes = Vec_IntAlloc( 100 ); // final result + // additional AIG data-members + if ( pAig->pFanData == NULL ) + Aig_ManFanoutStart( pAig ); + if ( pAig->pTerSimData == NULL ) + pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) ); + p->timeStart = clock(); + return p; +} + +/**Function************************************************************* + + Synopsis [Frees manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManStop( Pdr_Man_t * p ) +{ + Pdr_Set_t * pCla; + sat_solver * pSat; + int i, k; + if ( p->pPars->fVerbose ) + { + printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n", + p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts ); + ABC_PRTP( "SAT solving", p->tSat, p->tTotal ); + ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal ); + ABC_PRTP( " sat ", p->tSatSat, p->tTotal ); + ABC_PRTP( "Generalize ", p->tGeneral, p->tTotal ); + ABC_PRTP( "Push clause", p->tPush, p->tTotal ); + ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal ); + ABC_PRTP( "Containment", p->tContain, p->tTotal ); + ABC_PRTP( "CNF compute", p->tCnf, p->tTotal ); + ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal ); + } + + Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i ) + sat_solver_delete( pSat ); + Vec_PtrFree( p->vSolvers ); + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k ) + Pdr_SetDeref( pCla ); + Vec_VecFree( p->vClauses ); + Pdr_QueueStop( p ); + ABC_FREE( p->pOrder ); + Vec_IntFree( p->vActVars ); + // static CNF + Cnf_DataFree( p->pCnf1 ); + Vec_IntFreeP( &p->vVar2Reg ); + // dynamic CNF + Cnf_DataFree( p->pCnf2 ); + if ( p->pvId2Vars ) + for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) + Vec_IntFreeP( &p->pvId2Vars[i] ); + ABC_FREE( p->pvId2Vars ); + Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids ); + // internal use + Vec_IntFreeP( &p->vPrio ); // priority flops + Vec_IntFree( p->vLits ); // array of literals + Vec_IntFree( p->vCiObjs ); // cone leaves + Vec_IntFree( p->vCoObjs ); // cone roots + Vec_IntFree( p->vCiVals ); // cone leaf values + Vec_IntFree( p->vCoVals ); // cone root values + Vec_IntFree( p->vNodes ); // cone nodes + Vec_IntFree( p->vUndo ); // cone undos + Vec_IntFree( p->vVisits ); // intermediate + Vec_IntFree( p->vCi2Rem ); // CIs to be removed + Vec_IntFree( p->vRes ); // final result + // additional AIG data-members + if ( p->pAig->pFanData != NULL ) + Aig_ManFanoutStop( p->pAig ); + if ( p->pAig->pTerSimData != NULL ) + ABC_FREE( p->pAig->pTerSimData ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Derives counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) +{ + extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); + Abc_Cex_t * pCex; + Pdr_Obl_t * pObl; + int i, f, Lit, nFrames = 0; + // count the number of frames + for ( pObl = p->pQueue; pObl; pObl = pObl->pNext ) + nFrames++; + // create the counter-example + pCex = Gia_ManAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); + pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; + pCex->iFrame = nFrames-1; + for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) + for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) + { + Lit = pObl->pState->Lits[i]; + if ( lit_sign(Lit) ) + continue; + assert( lit_var(Lit) < pCex->nPis ); + Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); + } + assert( f == nFrames ); + return pCex; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c new file mode 100644 index 00000000..45ada5c0 --- /dev/null +++ b/src/sat/pdr/pdrSat.c @@ -0,0 +1,351 @@ +/**CFile**************************************************************** + + FileName [pdrSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [SAT solver procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates new SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) +{ + sat_solver * pSat; + assert( Vec_PtrSize(p->vSolvers) == k ); + assert( Vec_VecSize(p->vClauses) == k ); + assert( Vec_IntSize(p->vActVars) == k ); + // create new solver + pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) ); + Vec_PtrPush( p->vSolvers, pSat ); + Vec_VecExpand( p->vClauses, k ); + Vec_IntPush( p->vActVars, 0 ); + // add property cone + Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Returns old or restarted solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ) +{ + sat_solver * pSat; + Vec_Ptr_t * vArrayK; + Pdr_Set_t * pCube; + int i, j; + pSat = Pdr_ManSolver(p, k); + if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle ) + return pSat; + assert( k < Vec_PtrSize(p->vSolvers) - 1 ); + p->nStarts++; + sat_solver_delete( pSat ); + // create new SAT solver + pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) ); + // write new SAT solver + Vec_PtrWriteEntry( p->vSolvers, k, pSat ); + Vec_IntWriteEntry( p->vActVars, k, 0 ); + // set the property output + Pdr_ManSetPropertyOutput( p, k ); + // add the clauses + Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) + Pdr_ManSolverAddClause( p, k, pCube ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Converts SAT variables into register IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray ) +{ + int i, RegId; + Vec_IntClear( p->vLits ); + for ( i = 0; i < nArray; i++ ) + { + RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) ); + if ( RegId == -1 ) + continue; + assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) ); + Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) ); + } + assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray ); + return p->vLits; +} + +/**Function************************************************************* + + Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext ) +{ + Aig_Obj_t * pObj; + int i, iVar, iVarMax = 0; + int clk = clock(); + Vec_IntClear( p->vLits ); + for ( i = 0; i < pCube->nLits; i++ ) + { + if ( pCube->Lits[i] == -1 ) + continue; + if ( fNext ) + pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) ); + else + pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) ); + iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + iVarMax = ABC_MAX( iVarMax, iVar ); + Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) ); + } +// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 ); + p->tCnf += clock() - clk; + return p->vLits; +} + +/**Function************************************************************* + + Synopsis [Sets the property output to 0 (sat) forever.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) +{ + sat_solver * pSat; + int Lit, RetValue; + pSat = Pdr_ManSolver(p, k); + Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal + RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue == 1 ); + sat_solver_compress( pSat ); +} + +/**Function************************************************************* + + Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + int RetValue; + pSat = Pdr_ManSolver(p, k); + vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + assert( RetValue == 1 ); + sat_solver_compress( pSat ); +} + +/**Function************************************************************* + + Synopsis [Collects values of the RO/RI variables in k-th SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues ) +{ + sat_solver * pSat; + Aig_Obj_t * pObj; + int iVar, i; + Vec_IntClear( vValues ); + pSat = Pdr_ManSolver(p, k); + Aig_ManForEachNodeVec( p->pAig, vObjIds, pObj, i ) + { + iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.] + + Description [Return 1/0 if cube or property are proved to hold/fail + in k-th timeframe. Returns the predecessor bad state in ppPred.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + int RetValue; + pSat = Pdr_ManFetchSolver( p, k ); + vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 ); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + assert( RetValue != l_Undef ); + return (RetValue == l_False); +} + +/**Function************************************************************* + + Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.] + + Description [Return 1/0 if cube or property are proved to hold/fail + in k-th timeframe. Returns the predecessor bad state in ppPred.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ) +{ + int fUseLit = 1; + int fLitUsed = 0; + sat_solver * pSat; + Vec_Int_t * vLits; + int Lit, RetValue, clk; + p->nCalls++; + pSat = Pdr_ManFetchSolver( p, k ); + if ( pCube == NULL ) // solve the property + { + clk = clock(); + Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails) + RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); + if ( RetValue == l_Undef ) + return -1; + } + else // check relative containment in terms of next states + { + if ( fUseLit ) + { + fLitUsed = 1; + Vec_IntAddToEntry( p->vActVars, k, 1 ); + // add the cube in terms of current state variables + vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 ); + // add activation literal + Lit = toLit( Pdr_ManFreeVar(p, k) ); + // add activation literal + Vec_IntPush( vLits, Lit ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + assert( RetValue == 1 ); + sat_solver_compress( pSat ); + // create assumptions + vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 ); + // add activation literal + Vec_IntPush( vLits, lit_neg(Lit) ); + } + else + vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 ); + + // solve + clk = clock(); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); + if ( RetValue == l_Undef ) + return -1; + } + clk = clock() - clk; + p->tSat += clk; + assert( RetValue != l_Undef ); + if ( RetValue == l_False ) + { + p->tSatUnsat += clk; + p->nCallsU++; + if ( ppPred ) + *ppPred = NULL; + RetValue = 1; + } + else // if ( RetValue == l_True ) + { + p->tSatSat += clk; + p->nCallsS++; + if ( ppPred ) + *ppPred = Pdr_ManTernarySim( p, k, pCube ); + RetValue = 0; + } + +/* // for some reason, it does not work... + if ( fLitUsed ) + { + int RetValue; + Lit = lit_neg(Lit); + RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue == 1 ); + sat_solver_compress( pSat ); + } +*/ + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c new file mode 100644 index 00000000..01b54e3f --- /dev/null +++ b/src/sat/pdr/pdrTsim.c @@ -0,0 +1,450 @@ +/**CFile**************************************************************** + + FileName [pdrTsim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Ternary simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define PDR_ZER 1 +#define PDR_ONE 2 +#define PDR_UND 3 + +static inline int Pdr_ManSimInfoNot( int Value ) +{ + if ( Value == PDR_ZER ) + return PDR_ONE; + if ( Value == PDR_ONE ) + return PDR_ZER; + return PDR_UND; +} + +static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 ) +{ + if ( Value0 == PDR_ZER || Value1 == PDR_ZER ) + return PDR_ZER; + if ( Value0 == PDR_ONE && Value1 == PDR_ONE ) + return PDR_ONE; + return PDR_UND; +} + +static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1)); +} + +static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value ) +{ + assert( Value >= PDR_ZER && Value <= PDR_UND ); + Value ^= Pdr_ManSimInfoGet( p, pObj ); + p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1)); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Marks the TFI cone and collects CIs and nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + Vec_IntPush( vCiObjs, Aig_ObjId(pObj) ); + return; + } + Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes ); + if ( Aig_ObjIsPo(pObj) ) + return; + Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes ); + Vec_IntPush( vNodes, Aig_ObjId(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Marks the TFI cone and collects CIs and nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes ) +{ + Aig_Obj_t * pObj; + int i; + Vec_IntClear( vCiObjs ); + Vec_IntClear( vNodes ); + Aig_ManIncrementTravId( pAig ); + Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); + Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i ) + Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes ); +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + int Value0, Value1, Value; + Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) ); + if ( Aig_ObjFaninC0(pObj) ) + Value0 = Pdr_ManSimInfoNot( Value0 ); + if ( Aig_ObjIsPo(pObj) ) + { + Pdr_ManSimInfoSet( pAig, pObj, Value0 ); + return Value0; + } + assert( Aig_ObjIsNode(pObj) ); + Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) ); + if ( Aig_ObjFaninC1(pObj) ) + Value1 = Pdr_ManSimInfoNot( Value1 ); + Value = Pdr_ManSimInfoAnd( Value0, Value1 ); + Pdr_ManSimInfoSet( pAig, pObj, Value ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one design.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManSimDataInit( Aig_Man_t * pAig, + Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes, + Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem ) +{ + Aig_Obj_t * pObj; + int i; + // set the CI values + Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE ); + Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i ) + Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) ); + // set the FOs to remove + if ( vCi2Rem != NULL ) + Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i ) + Pdr_ManSimInfoSet( pAig, pObj, PDR_UND ); + // perform ternary simulation + Aig_ManForEachNodeVec( pAig, vNodes, pObj, i ) + Pdr_ManExtendOneEval( pAig, pObj ); + // transfer results to the output + Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i ) + Pdr_ManExtendOneEval( pAig, pObj ); + // check the results + Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i ) + if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Tries to assign ternary value to one of the CIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis ) +{ + Aig_Obj_t * pFanout; + int i, k, iFanout, Value, Value2; + assert( Saig_ObjIsLo(pAig, pObj) ); + assert( Aig_ObjIsTravIdCurrent(pAig, pObj) ); + // save original value + Value = Pdr_ManSimInfoGet( pAig, pObj ); + assert( Value == PDR_ZER || Value == PDR_ONE ); + Vec_IntPush( vUndo, Aig_ObjId(pObj) ); + Vec_IntPush( vUndo, Value ); + // update original value + Pdr_ManSimInfoSet( pAig, pObj, PDR_UND ); + // traverse + Vec_IntClear( vVis ); + Vec_IntPush( vVis, Aig_ObjId(pObj) ); + Aig_ManForEachNodeVec( pAig, vVis, pObj, i ) + { + Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k ) + { + if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) ) + continue; + assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) ); + Value = Pdr_ManSimInfoGet( pAig, pFanout ); + if ( Value == PDR_UND ) + continue; + Value2 = Pdr_ManExtendOneEval( pAig, pFanout ); + if ( Value2 == Value ) + continue; + assert( Value2 == PDR_UND ); + Vec_IntPush( vUndo, Aig_ObjId(pFanout) ); + Vec_IntPush( vUndo, Value ); + if ( Aig_ObjIsPo(pFanout) ) + return 0; + assert( Aig_ObjIsNode(pFanout) ); + Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Undoes the partial results of ternary simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo ) +{ + Aig_Obj_t * pObj; + int i, Value; + Aig_ManForEachNodeVec( pAig, vUndo, pObj, i ) + { + Value = Vec_IntEntry(vUndo, ++i); + assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND ); + Pdr_ManSimInfoSet( pAig, pObj, Value ); + } +} + +/**Function************************************************************* + + Synopsis [Derives the resulting cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits ) +{ + Aig_Obj_t * pObj; + int i, Lit; + // mark removed flop outputs + Aig_ManIncrementTravId( pAig ); + Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i ) + { + assert( Saig_ObjIsLo( pAig, pObj ) ); + Aig_ObjSetTravIdCurrent(pAig, pObj); + } + // collect flop outputs that are not marked + Vec_IntClear( vRes ); + Vec_IntClear( vPiLits ); + Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i ) + { + if ( Saig_ObjIsPi(pAig, pObj) ) + { + Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); + Vec_IntPush( vPiLits, Lit ); + continue; + } + assert( Saig_ObjIsLo(pAig, pObj) ); + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + continue; + Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); + Vec_IntPush( vRes, Lit ); + } + if ( Vec_IntSize(vRes) == 0 ) + Vec_IntPush(vRes, 0); +} + +/**Function************************************************************* + + Synopsis [Derives the resulting cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem ) +{ + Aig_Obj_t * pObj; + int i; + char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 ); + for ( i = 0; i < Aig_ManPiNum(pAig); i++ ) + pBuff[i] = '-'; + pBuff[i] = 0; + Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i ) + pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); + if ( vCi2Rem ) + Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i ) + pBuff[Aig_ObjPioNum(pObj)] = 'x'; + printf( "%s\n", pBuff ); + ABC_FREE( pBuff ); +} + +/**Function************************************************************* + + Synopsis [Shrinks values using ternary simulation.] + + Description [The cube contains the set of flop index literals which, + when converted into a clause and applied to the combinational outputs, + led to a satisfiable SAT run in frame k (values stored in the SAT solver). + If the cube is NULL, it is assumed that the first property output was + asserted and failed. + The resulting array is a set of flop index literals that asserts the COs. + Priority contains 0 for i-th entry if the i-th FF is desirable to remove.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + Vec_Int_t * vPrio = p->vPrio; // priority flops (flop indices) + Vec_Int_t * vPiLits = p->vLits; // array of literals (0/1 PI values) + Vec_Int_t * vCiObjs = p->vCiObjs; // cone leaves (CI obj IDs) + Vec_Int_t * vCoObjs = p->vCoObjs; // cone roots (CO obj IDs) + Vec_Int_t * vCiVals = p->vCiVals; // cone leaf values (0/1 CI values) + Vec_Int_t * vCoVals = p->vCoVals; // cone root values (0/1 CO values) + Vec_Int_t * vNodes = p->vNodes; // cone nodes (node obj IDs) + Vec_Int_t * vUndo = p->vUndo; // cone undos (node obj IDs) + Vec_Int_t * vVisits = p->vVisits; // intermediate (obj IDs) + Vec_Int_t * vCi2Rem = p->vCi2Rem; // CIs to be removed (CI obj IDs) + Vec_Int_t * vRes = p->vRes; // final result (flop literals) + Aig_Obj_t * pObj; + int i, Entry, RetValue; + int clk = clock(); + + // collect CO objects + Vec_IntClear( vCoObjs ); + if ( pCube == NULL ) // the target is the property output + Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); + else // the target is the cube + { + for ( i = 0; i < pCube->nLits; i++ ) + { + if ( pCube->Lits[i] == -1 ) + continue; + pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1)); + Vec_IntPush( vCoObjs, Aig_ObjId(pObj) ); + } + } +if ( p->pPars->fVeryVerbose ) +{ +printf( "Trying to justify cube " ); +if ( pCube ) + Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL ); +else + printf( "<prop=fail>" ); +printf( " in frame %d.\n", k ); +} + + // collect CI objects + Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes ); + // collect values + Pdr_ManCollectValues( p, k, vCiObjs, vCiVals ); + Pdr_ManCollectValues( p, k, vCoObjs, vCoVals ); + // simulate for the first time +if ( p->pPars->fVeryVerbose ) +Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); + RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL ); + assert( RetValue ); + + // try removing high-priority flops + Vec_IntClear( vCi2Rem ); + Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } + // try removing low-priority flops + Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } +if ( p->pPars->fVeryVerbose ) +Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); + RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem ); + assert( RetValue ); + + // derive the set of resulting registers + Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits ); + assert( Vec_IntSize(vRes) > 0 ); + p->tTsim += clock() - clk; + return Pdr_SetCreate( vRes, vPiLits ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c new file mode 100644 index 00000000..7e83102b --- /dev/null +++ b/src/sat/pdr/pdrUtil.c @@ -0,0 +1,547 @@ +/**CFile**************************************************************** + + FileName [pdrUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 20, 2010.] + + Revision [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pdrInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntSelectSort( int * pArray, int nSize ) +{ + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( pArray[j] < pArray[best_i] ) + best_i = j; + temp = pArray[i]; + pArray[i] = pArray[best_i]; + pArray[best_i] = temp; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ) +{ + Pdr_Set_t * p; + int i; + assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<15) ); + p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) ); + p->nLits = Vec_IntSize(vLits); + p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits); + p->nRefs = 1; + p->Sign = 0; + for ( i = 0; i < p->nLits; i++ ) + { + p->Lits[i] = Vec_IntEntry(vLits, i); + p->Sign |= ((word)1 << (p->Lits[i] % 63)); + } + Vec_IntSelectSort( p->Lits, p->nLits ); +/* + for ( i = 0; i < p->nLits; i++ ) + printf( "%d ", p->Lits[i] ); + printf( "\n" ); +*/ + // remember PI literals + for ( i = p->nLits; i < p->nTotal; i++ ) + p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ) +{ + Pdr_Set_t * p; + int i, k = 0; + assert( iRemove >= 0 && iRemove < pSet->nLits ); + p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) ); + p->nLits = pSet->nLits - 1; + p->nTotal = pSet->nTotal - 1; + p->nRefs = 1; + p->Sign = 0; + for ( i = 0; i < pSet->nTotal; i++ ) + { + if ( i == iRemove ) + continue; + p->Lits[k++] = pSet->Lits[i]; + if ( i >= pSet->nLits ) + continue; + p->Sign |= ((word)1 << (pSet->Lits[i] % 63)); + } + assert( k == p->nTotal ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ) +{ + Pdr_Set_t * p; + int i, k = 0; + assert( nLits >= 0 && nLits <= pSet->nLits ); + p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) ); + p->nLits = nLits; + p->nTotal = nLits + pSet->nTotal - pSet->nLits; + p->nRefs = 1; + p->Sign = 0; + for ( i = 0; i < nLits; i++ ) + { + assert( pLits[i] >= 0 ); + p->Lits[k++] = pLits[i]; + p->Sign |= ((word)1 << (pLits[i] % 63)); + } + Vec_IntSelectSort( p->Lits, p->nLits ); + for ( i = pSet->nLits; i < pSet->nTotal; i++ ) + p->Lits[k++] = pSet->Lits[i]; + assert( k == p->nTotal ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ) +{ + Pdr_Set_t * p; + int i; + p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) ); + p->nLits = pSet->nLits; + p->nTotal = pSet->nTotal; + p->nRefs = 1; + p->Sign = pSet->Sign; + for ( i = 0; i < pSet->nTotal; i++ ) + p->Lits[i] = pSet->Lits[i]; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ) +{ + p->nRefs++; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_SetDeref( Pdr_Set_t * p ) +{ + if ( --p->nRefs == 0 ) + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ) +{ + char * pBuff; + int i, k, Entry; + pBuff = ABC_ALLOC( char, nRegs + 1 ); + for ( i = 0; i < nRegs; i++ ) + pBuff[i] = '-'; + pBuff[i] = 0; + for ( i = 0; i < p->nLits; i++ ) + { + if ( p->Lits[i] == -1 ) + continue; + pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); + } + if ( vFlopCounts ) + { + // skip some literals + k = 0; + Vec_IntForEachEntry( vFlopCounts, Entry, i ) + if ( Entry ) + pBuff[k++] = pBuff[i]; + pBuff[k] = 0; + } + fprintf( pFile, "%s", pBuff ); + ABC_FREE( pBuff ); +} + +/**Function************************************************************* + + Synopsis [Return 1 if pOld set-theoretically contains pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) +{ + int * pOldInt, * pNewInt; + assert( pOld->nLits > 0 ); + assert( pNew->nLits > 0 ); + if ( pOld->nLits < pNew->nLits ) + return 0; + if ( (pOld->Sign & pNew->Sign) != pNew->Sign ) + return 0; + pOldInt = pOld->Lits + pOld->nLits - 1; + pNewInt = pNew->Lits + pNew->nLits - 1; + while ( pNew->Lits <= pNewInt ) + { + if ( pOld->Lits > pOldInt ) + return 0; + assert( *pNewInt != -1 ); + assert( *pOldInt != -1 ); + if ( *pNewInt == *pOldInt ) + pNewInt--, pOldInt--; + else if ( *pNewInt < *pOldInt ) + pOldInt--; + else + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Return 1 if the state cube contains init state (000...0).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove ) +{ + int i; + for ( i = 0; i < pCube->nLits; i++ ) + { + assert( pCube->Lits[i] != -1 ); + if ( i == iRemove ) + continue; + if ( lit_sign( pCube->Lits[i] ) == 0 ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) +{ + Pdr_Set_t * p1 = *pp1; + Pdr_Set_t * p2 = *pp2; + int i; + for ( i = 0; i < p1->nLits && i < p2->nLits; i++ ) + { + if ( p1->Lits[i] > p2->Lits[i] ) + return -1; + if ( p1->Lits[i] < p2->Lits[i] ) + return 1; + } + if ( i == p1->nLits && i < p2->nLits ) + return -1; + if ( i < p1->nLits && i == p2->nLits ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ) +{ + Pdr_Obl_t * p; + p = ABC_ALLOC( Pdr_Obl_t, 1 ); + p->iFrame = k; + p->prio = prio; + p->nRefs = 1; + p->pState = pState; + p->pNext = pNext; + p->pLink = NULL; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ) +{ + p->nRefs++; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_OblDeref( Pdr_Obl_t * p ) +{ + if ( --p->nRefs == 0 ) + { + if ( p->pNext ) + Pdr_OblDeref( p->pNext ); + Pdr_SetDeref( p->pState ); + ABC_FREE( p ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_QueueIsEmpty( Pdr_Man_t * p ) +{ + return p->pQueue == NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p ) +{ + return p->pQueue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ) +{ + Pdr_Obl_t * pRes = p->pQueue; + if ( p->pQueue == NULL ) + return NULL; + p->pQueue = p->pQueue->pLink; + Pdr_OblDeref( pRes ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ) +{ + Pdr_Obl_t * pTemp, ** ppPrev; + p->nObligs++; + Pdr_OblRef( pObl ); + if ( p->pQueue == NULL ) + { + p->pQueue = pObl; + return; + } + for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink ) + if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) ) + break; + *ppPrev = pObl; + pObl->pLink = pTemp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_QueuePrint( Pdr_Man_t * p ) +{ + Pdr_Obl_t * pObl; + for ( pObl = p->pQueue; pObl; pObl = pObl->pLink ) + printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_QueueStop( Pdr_Man_t * p ) +{ + Pdr_Obl_t * pObl; + while ( !Pdr_QueueIsEmpty(p) ) + { + pObl = Pdr_QueuePop(p); + Pdr_OblDeref( pObl ); + } + p->pQueue = NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |