luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Naive (SAT-only) CEC option.

This commit is contained in:
Alan Mishchenko 2014-10-10 16:14:48 -07:00
parent 01e1b6345e
commit f6c1fc072c
3 changed files with 116 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/abci/abc.c
View File

@ -30273,7 +30273,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdavh" ) ) != EOF )
{
switch ( c )
{
@ -30299,6 +30299,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->TimeLimit < 0 )
goto usage;
break;
case 'n':
pPars->fNaive ^= 1;
break;
case 'm':
fMiter ^= 1;
break;
@ -30390,10 +30393,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &cec [-CT num] [-mdavh]\n" );
Abc_Print( -2, "usage: &cec [-CT num] [-nmdavh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");

1
src/proof/cec/cec.h
View File

@ -122,6 +122,7 @@ struct Cec_ParCec_t_
// int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fRewriting; // enables AIG rewriting
int fNaive; // performs naive SAT-based checking
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the number of failed output

109
src/proof/cec/cecCec.c
View File

@ -21,6 +21,8 @@
#include "cecInt.h"
#include "proof/fra/fra.h"
#include "aig/gia/giaAig.h"
#include "misc/extra/extra.h"
#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
@ -191,6 +193,107 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
return -1;
}
/**Function*************************************************************
Synopsis [Performs naive checking.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManVerifyNaive( Gia_Man_t * p, Cec_ParCec_t * pPars )
{
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Gia_Obj_t * pObj0, * pObj1;
abctime clkStart = Abc_Clock();
int nPairs = Gia_ManPoNum(p)/2;
int nUnsats = 0, nSats = 0, nUndecs = 0, nTrivs = 0;
int i, iVar0, iVar1, pLits[2], status, RetValue;
ProgressBar * pProgress = Extra_ProgressBarStart( stdout, nPairs );
assert( Gia_ManPoNum(p) % 2 == 0 );
for ( i = 0; i < nPairs; i++ )
{
if ( (i & 0xFF) == 0 )
Extra_ProgressBarUpdate( pProgress, i, NULL );
pObj0 = Gia_ManPo(p, 2*i);
pObj1 = Gia_ManPo(p, 2*i+1);
if ( Gia_ObjChild0(pObj0) == Gia_ObjChild0(pObj1) )
{
nUnsats++;
nTrivs++;
continue;
}
if ( pPars->TimeLimit && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->TimeLimit )
{
printf( "Timeout (%d sec) is reached.\n", pPars->TimeLimit );
nUndecs = nPairs - nUnsats - nSats;
break;
}
iVar0 = pCnf->pVarNums[ Gia_ObjId(p, pObj0) ];
iVar1 = pCnf->pVarNums[ Gia_ObjId(p, pObj1) ];
assert( iVar0 >= 0 && iVar1 >= 0 );
pLits[0] = Abc_Var2Lit( iVar0, 0 );
pLits[1] = Abc_Var2Lit( iVar1, 0 );
// check direct
pLits[0] = lit_neg(pLits[0]);
status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 );
if ( status == l_False )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
assert( RetValue );
}
else if ( status == l_True )
{
printf( "Output %d is SAT.\n", i );
nSats++;
continue;
}
else
{
nUndecs++;
continue;
}
// check inverse
status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 );
if ( status == l_False )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
assert( RetValue );
}
else if ( status == l_True )
{
printf( "Output %d is SAT.\n", i );
nSats++;
continue;
}
else
{
nUndecs++;
continue;
}
nUnsats++;
}
Extra_ProgressBarStop( pProgress );
printf( "UNSAT = %6d. SAT = %6d. UNDEC = %6d. Trivial = %6d. ", nUnsats, nSats, nUndecs, nTrivs );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
if ( nSats )
return 0;
if ( nUndecs )
return -1;
return 1;
}
/**Function*************************************************************
Synopsis [New CEC engine.]
@ -222,6 +325,12 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_ManEquivFixOutputPairs( p );
p = Gia_ManCleanup( pNew = p );
Gia_ManStop( pNew );
if ( pPars->fNaive )
{
RetValue = Cec_ManVerifyNaive( p, pPars );
Gia_ManStop( p );
return RetValue;
}
// sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;