summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/pdr/pdr.h2
-rw-r--r--src/sat/pdr/pdrClass.c2
-rw-r--r--src/sat/pdr/pdrCnf.c2
-rw-r--r--src/sat/pdr/pdrCore.c2
-rw-r--r--src/sat/pdr/pdrInt.h13
-rw-r--r--src/sat/pdr/pdrInv.c2
-rw-r--r--src/sat/pdr/pdrMan.c35
-rw-r--r--src/sat/pdr/pdrSat.c20
-rw-r--r--src/sat/pdr/pdrTsim.c2
-rw-r--r--src/sat/pdr/pdrUtil.c200
10 files changed, 243 insertions, 37 deletions
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*************************************************************
@@ -301,6 +294,46 @@ int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
/**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).]
Description []
@@ -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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:39:23 +0000