summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-11-05 19:37:46 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2013-11-05 19:37:46 -0800
commit66b6593513bee13732999d4b2216d7a411003ce0 (patch)
tree264e477a1c33ed89305f65c893c56bc59d4da47d /src
parente3560904ec9a9bd225237b113f75f18d7182c2a2 (diff)
downloadabc-66b6593513bee13732999d4b2216d7a411003ce0.tar.gz
abc-66b6593513bee13732999d4b2216d7a411003ce0.tar.bz2
abc-66b6593513bee13732999d4b2216d7a411003ce0.zip
Specialized inductive check.
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c23
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcICheck.c139
3 files changed, 159 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0ac0b7cf..c9159d3f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32686,9 +32686,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fVerbose = 0;
+ int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "MTevh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrdvh" ) ) != EOF )
{
switch ( c )
{
@@ -32717,6 +32717,15 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e':
fEmpty ^= 1;
break;
+ case 's':
+ fSearch ^= 1;
+ break;
+ case 'r':
+ fReverse ^= 1;
+ break;
+ case 'd':
+ fDump ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -32736,15 +32745,21 @@ 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, fEmpty, fVerbose );
+ if ( fSearch )
+ Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
+ else
+ Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &icheck [-MT num] [-evh]\n" );
+ Abc_Print( -2, "usage: &icheck [-MT num] [-esrdvh]\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-e : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" );
+ Abc_Print( -2, "\t-s : toggle searching for a minimal subset [default = %s]\n", fSearch? "yes": "no" );
+ Abc_Print( -2, "\t-r : toggle searching in the reverse order [default = %s]\n", fReverse? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggle printing out the resulting set [default = %s]\n", fDump? "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 0cfc9b37..2f7af2ba 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -132,6 +132,7 @@ extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
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 fEmpty, int fVerbose );
+extern void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, 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 17408e78..13ab1038 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -293,6 +293,145 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
Vec_IntFree( vUsed );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t * vLits )
+{
+ int fUseOldCnf = 0;
+ Gia_Man_t * pMiter, * pTemp;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+// Vec_Int_t * vLits;
+ int i, Iter, status;
+ int nLitsUsed;
+ 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, 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 positive literals
+ vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+*/
+ // derive SAT solver
+ pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
+ 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_True )
+ {
+ printf( "I = %4d : ", nFramesMax );
+ printf( "Problem is satisfiable.\n" );
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ Gia_ManStop( pMiter );
+ return;
+ }
+ assert( status == l_False );
+
+ // count the number of positive literals
+ nLitsUsed = 0;
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+ nLitsUsed++;
+
+ // try removing variables
+ for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
+ {
+ i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
+ if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+ continue;
+ Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
+ 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 );
+ break;
+ }
+ if ( status == l_True )
+ Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
+ else if ( status == l_False )
+ nLitsUsed--;
+ else assert( 0 );
+ // report the results
+ //printf( "Round %d: ", o );
+ printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
+ i, (nFramesMax+1) * Gia_ManAndNum(pMiter),
+ Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
+ sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
+ ABC_PRTr( "Time", Abc_Clock() - clkStart );
+ fflush( stdout );
+ }
+ // report the results
+ //printf( "Round %d: ", o );
+ 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) + sat_solver_nvars(pSat),
+ sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+ fflush( stdout );
+
+ // cleanup
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ Gia_ManStop( pMiter );
+// Vec_IntFree( vLits );
+}
+void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
+{
+ Vec_Int_t * vLits;
+ int i, f;
+ 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) );
+ fflush( stdout );
+
+ // collect positive literals
+ vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+
+ for ( f = 1; f < nFramesMax; f++ )
+ Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits );
+
+ // dump the numbers of the flops
+ if ( fDump )
+ {
+ int nLitsUsed = 0;
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+ nLitsUsed++;
+ printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
+ for ( i = 0; i < Gia_ManRegNum(p); i++ )
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+ printf( "%d ", i );
+ printf( "\n" );
+ }
+ Vec_IntFree( vLits );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////