From a28fe0d324b0c096d1f6f2d27f956f4f1625ed9e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Apr 2011 13:49:03 -0700 Subject: Unsuccessful attempt to improve PDR and a few minor changes. --- src/sat/pdr/pdr.h | 2 +- src/sat/pdr/pdrClass.c | 2 +- src/sat/pdr/pdrCnf.c | 2 +- src/sat/pdr/pdrCore.c | 2 +- src/sat/pdr/pdrInt.h | 13 +++- src/sat/pdr/pdrInv.c | 2 +- src/sat/pdr/pdrMan.c | 35 +++++---- src/sat/pdr/pdrSat.c | 20 ++++- src/sat/pdr/pdrTsim.c | 2 +- src/sat/pdr/pdrUtil.c | 200 +++++++++++++++++++++++++++++++++++++++++++++---- 10 files changed, 243 insertions(+), 37 deletions(-) (limited to 'src/sat/pdr') diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h index 27e76b6e..740eb46f 100644 --- a/src/sat/pdr/pdr.h +++ b/src/sat/pdr/pdr.h @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [External declarations.] diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c index 31449735..3e990958 100644 --- a/src/sat/pdr/pdrClass.c +++ b/src/sat/pdr/pdrClass.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Equivalence classes of register outputs.] diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c index b40ed6d9..2c5218d8 100644 --- a/src/sat/pdr/pdrCnf.c +++ b/src/sat/pdr/pdrCnf.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [CNF computation on demand.] diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index 742ce381..6289889b 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Core procedures.] diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h index d0211278..1eadcf93 100644 --- a/src/sat/pdr/pdrInt.h +++ b/src/sat/pdr/pdrInt.h @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Internal declarations.] @@ -92,6 +92,8 @@ struct Pdr_Man_t_ Vec_Int_t * vVisits; // intermediate Vec_Int_t * vCi2Rem; // CIs to be removed Vec_Int_t * vRes; // final result + Vec_Int_t * vSuppLits; // support literals + Pdr_Set_t * pCubeJust; // justification // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -101,6 +103,10 @@ struct Pdr_Man_t_ int nCallsU; // the number of SAT calls (unsat) int nStarts; // the number of SAT solver restarts int nFrames; // frames explored + int nCasesSS; + int nCasesSU; + int nCasesUS; + int nCasesUU; // runtime int timeStart; int timeToStop; @@ -133,6 +139,8 @@ 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 ); +/*=== pdrCore.c ==========================================================*/ +extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet ); /*=== pdrInv.c ==========================================================*/ extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); @@ -156,6 +164,7 @@ extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube /*=== 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_SetAlloc( int nSize ); 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 ); @@ -163,6 +172,7 @@ 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_SetContainsSimple( 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 ); @@ -175,6 +185,7 @@ 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 ); +extern int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c index daf542e9..a60732cb 100644 --- a/src/sat/pdr/pdrInv.c +++ b/src/sat/pdr/pdrInv.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Invariant computation, printing, verification.] diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c index 97f0992b..95a38efb 100644 --- a/src/sat/pdr/pdrMan.c +++ b/src/sat/pdr/pdrMan.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [pdr.c] + FileName [pdrMan.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Manager procedures.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - November 20, 2010.] - Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] + Revision [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -65,6 +65,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vVisits = Vec_IntAlloc( 100 ); // intermediate p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result + p->vSuppLits= Vec_IntAlloc( 100 ); // support literals + p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) ); // additional AIG data-members if ( pAig->pFanData == NULL ) Aig_ManFanoutStart( pAig ); @@ -90,6 +92,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Pdr_Set_t * pCla; sat_solver * pSat; int i, k; + Aig_ManCleanMarkAB( p->pAig ); if ( p->pPars->fVerbose ) { printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n", @@ -104,7 +107,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) ABC_PRTP( "CNF compute", p->tCnf, p->tTotal ); ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal ); } - +// printf( "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU ); Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i ) sat_solver_delete( pSat ); Vec_PtrFree( p->vSolvers ); @@ -125,17 +128,19 @@ void Pdr_ManStop( Pdr_Man_t * p ) 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 + 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 + Vec_IntFree( p->vSuppLits ); // support literals + ABC_FREE( p->pCubeJust ); // additional AIG data-members if ( p->pAig->pFanData != NULL ) Aig_ManFanoutStop( p->pAig ); diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c index 45ada5c0..4ba22e84 100644 --- a/src/sat/pdr/pdrSat.c +++ b/src/sat/pdr/pdrSat.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [SAT solver procedures.] @@ -307,6 +307,24 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); if ( RetValue == l_Undef ) return -1; +/* + if ( RetValue == l_True ) + { + int RetValue2 = Pdr_ManCubeJust( p, k, pCube ); + if ( RetValue2 ) + p->nCasesSS++; + else + p->nCasesSU++; + } + else + { + int RetValue2 = Pdr_ManCubeJust( p, k, pCube ); + if ( RetValue2 ) + p->nCasesUS++; + else + p->nCasesUU++; + } +*/ } clk = clock() - clk; p->tSat += clk; diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c index 01b54e3f..ae457352 100644 --- a/src/sat/pdr/pdrTsim.c +++ b/src/sat/pdr/pdrTsim.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Ternary simulation.] diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c index 7e83102b..a568a2d5 100644 --- a/src/sat/pdr/pdrUtil.c +++ b/src/sat/pdr/pdrUtil.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Netlist representation.] + PackageName [Property driven reachability.] Synopsis [Various utilities.] @@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [Performs fast mapping for one node.] + Synopsis [] Description [] @@ -43,19 +43,12 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -static inline void Vec_IntSelectSort( int * pArray, int nSize ) +Pdr_Set_t * Pdr_SetAlloc( 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; - } + Pdr_Set_t * p; + assert( nSize < (1<<15) ); + p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) ); + return p; } /**Function************************************************************* @@ -299,6 +292,46 @@ int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) return 1; } +/**Function************************************************************* + + Synopsis [Return 1 if pOld set-theoretically contains pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ) +{ + int * pOldInt, * pNewInt; + assert( pOld->nLits > 0 ); + assert( pNew->nLits > 0 ); + pOldInt = pOld->Lits + pOld->nLits - 1; + pNewInt = pNew->Lits + pNew->nLits - 1; + while ( pNew->Lits <= pNewInt ) + { + assert( *pOldInt != -1 ); + if ( *pNewInt == -1 ) + { + pNewInt--; + continue; + } + 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).] @@ -538,6 +571,145 @@ void Pdr_QueueStop( Pdr_Man_t * p ) p->pQueue = NULL; } + +#define PDR_VAL0 1 +#define PDR_VAL1 2 +#define PDR_VALX 3 + +/**Function************************************************************* + + Synopsis [Returns value (0 or 1) or X if unassigned.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0; + return PDR_VALX; +} + +/**Function************************************************************* + + Synopsis [Recursively searched for a satisfying assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur ) +{ + int Value0, Value1; + if ( Aig_ObjIsConst1(pNode) ) + return 1; + if ( Aig_ObjIsTravIdCurrent(pAig, pNode) ) + return ((int)pNode->fMarkA == Value); + Aig_ObjSetTravIdCurrent(pAig, pNode); + pNode->fMarkA = Value; + if ( Aig_ObjIsPi(pNode) ) + { +// if ( vSuppLits ) +// Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); + if ( Saig_ObjIsLo(pAig, pNode) ) + { +// pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); + pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); + pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); + } + return 1; + } + assert( Aig_ObjIsNode(pNode) ); + // propagation + if ( Value ) + { + if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) ) + return 0; + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur); + } + // justification + Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) ); + if ( Value0 == PDR_VAL0 ) + return 1; + Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) ); + if ( Value1 == PDR_VAL0 ) + return 1; + if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 ) + return 0; + if ( Value0 == PDR_VAL1 ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); + if ( Value1 == PDR_VAL1 ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); + assert( Value0 == PDR_VALX && Value1 == PDR_VALX ); + // decision making +// if ( rand() % 10 == Heur ) + if ( Aig_ObjId(pNode) % 4 == Heur ) + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur); + else + return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) +{ + Aig_Obj_t * pNode; + int i, v, fCompl; +// return 0; + for ( i = 0; i < 4; i++ ) + { + // derive new assignment + p->pCubeJust->nLits = 0; + p->pCubeJust->Sign = 0; + Aig_ManIncrementTravId( p->pAig ); + for ( v = 0; v < pCube->nLits; v++ ) + { + if ( pCube->Lits[v] == -1 ) + continue; + pNode = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) ); + fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode); + if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) ) + break; + } + if ( v < pCube->nLits ) + continue; + // figure this out!!! + if ( p->pCubeJust->nLits == 0 ) + continue; + // successfully derived new assignment + Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits ); + // check assignment against this cube + if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) ) + continue; +//printf( "\n" ); +//Pdr_SetPrint( stdout, pCube, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); +//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" ); + // check assignment against the clauses + if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) ) + continue; + // find good assignment + return 1; + } + return 0; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3