Skip to content

A
abc
Commit 66b65935 by Alan Mishchenko
Options

Specialized inductive check.

parent e3560904
Showing with 159 additions and 4 deletions
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;
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 );
......
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 ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment