summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c18
-rw-r--r--src/sat/bmc/bmc.h2
-rw-r--r--src/sat/bmc/bmcICheck.c144
-rw-r--r--src/sat/bsat/satSolver.h39
4 files changed, 143 insertions, 60 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 075dd9ca..3da41636 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32576,9 +32576,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c, nFramesMax = 1, nTimeOut = 0, fVerbose = 0;
+ int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "MTvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MTevh" ) ) != EOF )
{
switch ( c )
{
@@ -32604,6 +32604,9 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nTimeOut < 0 )
goto usage;
break;
+ case 'e':
+ fEmpty ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -32623,15 +32626,16 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9ICheck(): The AIG is combinational.\n" );
return 0;
}
- Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fVerbose );
+ Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &icheck [-MT num] [-cvh]\n" );
+ Abc_Print( -2, "usage: &icheck [-MT num] [-evh]\n" );
Abc_Print( -2, "\t performs specialized induction check\n" );
- Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax );
- Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax );
+ Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
+ Abc_Print( -2, "\t-e : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index ae76ff6b..5d45c562 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -129,7 +129,7 @@ extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== bmcICheck.c ==========================================================*/
-extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbose );
+extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
/*=== bmcUnroll.c ==========================================================*/
extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index d7048c21..e388db04 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -88,48 +88,26 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl
SeeAlso []
***********************************************************************/
-void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbose )
+sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pCnf, int nFramesMax, int nTimeOut, int fVerbose )
{
- int fUseOldCnf = 0;
- Gia_Man_t * pMiter, * pTemp;
- Cnf_Dat_t * pCnf;
sat_solver * pSat;
Vec_Int_t * vLits;
Gia_Obj_t * pObj, * pObj0, * pObj1;
- int i, k, status, iVar0, iVar1, iVarOut;
- int nLits, * pLits;
- abctime clkStart = Abc_Clock();
- assert( nFramesMax > 0 );
- assert( Gia_ManRegNum(p) > 0 );
-
- // create miter
- pTemp = Gia_ManDup( p );
- pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
- Gia_ManStop( pTemp );
- assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
- assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
- // derive CNF
- if ( fUseOldCnf )
- pCnf = Cnf_DeriveGiaRemapped( pMiter );
- else
- {
- pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
- Gia_ManStop( pTemp );
- pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
- }
+ int i, k, iVar0, iVar1, iVarOut;
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
- // load the last timeframe
- Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
// add one large OR clause
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( p, pObj, i )
Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) );
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+
+ // load the last timeframe
+ Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
// add XOR clauses
Gia_ManForEachPo( p, pObj, i )
{
@@ -147,7 +125,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i;
- sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
+ sat_solver_add_xor_and( pSat, iVarOut, iVar0, iVar1, i );
}
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
@@ -155,8 +133,6 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
assert( 0 );
// add other timeframes
- printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
- Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
for ( k = 0; k < nFramesMax; k++ )
{
// collect variables of the RO nodes
@@ -196,18 +172,72 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
}
+// sat_solver_compress( pSat );
+ Vec_IntFree( vLits );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose )
+{
+ int fUseOldCnf = 0;
+ Gia_Man_t * pMiter, * pTemp;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Vec_Int_t * vLits, * vUsed;
+ int i, status, Lit;
+ int nLitsUsed, nLits, * pLits;
+ abctime clkStart = Abc_Clock();
+ assert( nFramesMax > 0 );
+ assert( Gia_ManRegNum(p) > 0 );
+
+ printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
+ Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
+
+ // create miter
+ pTemp = Gia_ManDup( p );
+ pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
+ Gia_ManStop( pTemp );
+ assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
+ assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
+ // derive CNF
+ if ( fUseOldCnf )
+ pCnf = Cnf_DeriveGiaRemapped( pMiter );
+ else
+ {
+ pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
+ Gia_ManStop( pTemp );
+ pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
+ }
- // collect literals
- Vec_IntClear( vLits );
+ // collect positive literals
+ vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
- // call the SAT solver
- sat_solver_compress( pSat );
+ // iteratively compute a minimal M-inductive set of next-state functions
+ nLitsUsed = Vec_IntSize(vLits);
+ vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
while ( 1 )
{
+ int fChanges = 0;
+ // derive SAT solver
+ pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
// sat_solver_bookmark( pSat );
- status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ if ( fEmpty )
+ status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ else
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
printf( "Timeout reached after %d seconds.\n", nTimeOut );
@@ -215,37 +245,47 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
}
if ( status == l_True )
{
- printf( "The problem is satisfiable (this is an error).\n" );
+ printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
break;
}
assert( status == l_False );
// call analize_final
nLits = sat_solver_final( pSat, &pLits );
+ // mark used literals
+ Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
+ for ( i = 0; i < nLits; i++ )
+ Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
+
+ // check if there are any positive unused
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ assert( i == Abc_Lit2Var(Lit) );
+ if ( Abc_LitIsCompl(Lit) )
+ continue;
+ if ( Vec_IntEntry(vUsed, i) )
+ continue;
+ // positive literal became unused
+ Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
+ nLitsUsed--;
+ fChanges = 1;
+ }
+ // report the results
printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
- Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1),
- sat_solver_nconflicts(pSat), nLits, 100.0 * nLits / Gia_ManRegNum(p) );
+ Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
+ sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
- if ( nLits == Vec_IntSize(vLits) )
+ // count the number of negative literals
+ sat_solver_delete( pSat );
+ if ( !fChanges || fEmpty )
break;
- break;
+// break;
// sat_solver_rollback( pSat );
-
- // add another large OR clause
- Vec_IntClear( vLits );
- for ( i = 0; i < nLits; i++ )
- Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + Abc_Lit2Var(pLits[i]), 0) );
- sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
- // create new literals
- Vec_IntClear( vLits );
- for ( i = 0; i < nLits; i++ )
- Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
}
-
- sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
Vec_IntFree( vLits );
+ Vec_IntFree( vUsed );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 087bef8c..0d46b86b 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -368,6 +368,45 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i
assert( Cid );
return 4;
}
+static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
+{
+ // F = (a (+) b) * c
+ lit Lits[4];
+ int Cid;
+ assert( iVarF >= 0 && iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+ Lits[0] = toLitCond( iVarF, 1 );
+ Lits[1] = toLitCond( iVarA, 1 );
+ Lits[2] = toLitCond( iVarB, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarF, 1 );
+ Lits[1] = toLitCond( iVarA, 0 );
+ Lits[2] = toLitCond( iVarB, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarF, 1 );
+ Lits[1] = toLitCond( iVarC, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarF, 0 );
+ Lits[1] = toLitCond( iVarA, 1 );
+ Lits[2] = toLitCond( iVarB, 0 );
+ Lits[3] = toLitCond( iVarC, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarF, 0 );
+ Lits[1] = toLitCond( iVarA, 0 );
+ Lits[2] = toLitCond( iVarB, 1 );
+ Lits[3] = toLitCond( iVarC, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+ return 5;
+}
static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int iVar2, int fCompl )
{
lit Lits[2];
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 00:32:51 +0000