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

Enabling circuit solver in &fraig.

This commit is contained in:
Alan Mishchenko 2014-08-12 18:54:43 -07:00
parent 9055265394
commit f907347484
6 changed files with 100 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -28931,7 +28931,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManFraSetDefaultParams( pPars );
pPars->fSatSweeping = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcwvh" ) ) != EOF )
{
switch ( c )
{
@ -29010,6 +29010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDualOut ^= 1;
break;
case 'c':
pPars->fRunCSat ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@ -29030,7 +29033,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdwvh]\n" );
Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcwvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
@ -29041,6 +29044,7 @@ usage:
Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

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

@ -107,6 +107,7 @@ struct Cec_ParFra_t_
int fDualOut; // miter with separate outputs
int fColorDiff; // miter with separate outputs
int fSatSweeping; // enable SAT sweeping
int fRunCSat; // enable another solver
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the failed output

5
src/proof/cec/cecCore.c
View File

@ -426,7 +426,10 @@ p->timeSim += Abc_Clock() - clk;
break;
}
clk = Abc_Clock();
Cec_ManSatSolve( pPat, pSrm, pParsSat );
if ( pPars->fRunCSat )
Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
else
Cec_ManSatSolve( pPat, pSrm, pParsSat );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{

2
src/proof/cec/cecInt.h
View File

@ -190,6 +190,7 @@ extern Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * p
extern void Cec_ManFraStop( Cec_ManFra_t * p );
/*=== cecPat.c ============================================================*/
extern void Cec_ManPatSavePattern( Cec_ManPat_t * pPat, Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat );
extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWords );
extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
/*=== cecSeq.c ============================================================*/
@ -201,6 +202,7 @@ extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );

28
src/proof/cec/cecPat.c
View File

@ -360,20 +360,21 @@ void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t *
{
Vec_Int_t * vPat;
int nPatLits;
abctime clk, clkTotal = Abc_Clock();
abctime clkTotal = Abc_Clock();
// abctime clk;
assert( Gia_ObjIsCo(pObj) );
pMan->nPats++;
pMan->nPatsAll++;
// compute values in the cone of influence
clk = Abc_Clock();
//clk = Abc_Clock();
Gia_ManIncrementTravId( p->pAig );
nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
pMan->nPatLits += nPatLits;
pMan->nPatLitsAll += nPatLits;
pMan->timeFind += Abc_Clock() - clk;
//pMan->timeFind += Abc_Clock() - clk;
// compute sensitizing path
clk = Abc_Clock();
//clk = Abc_Clock();
Vec_IntClear( pMan->vPattern1 );
Gia_ManIncrementTravId( p->pAig );
Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
@ -385,19 +386,26 @@ clk = Abc_Clock();
vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
pMan->nPatLitsMin += Vec_IntSize(vPat);
pMan->nPatLitsMinAll += Vec_IntSize(vPat);
pMan->timeShrink += Abc_Clock() - clk;
//pMan->timeShrink += Abc_Clock() - clk;
// verify pattern using ternary simulation
clk = Abc_Clock();
Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
pMan->timeVerify += Abc_Clock() - clk;
//clk = Abc_Clock();
// Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
//pMan->timeVerify += Abc_Clock() - clk;
// sort pattern
clk = Abc_Clock();
//clk = Abc_Clock();
Vec_IntSort( vPat, 0 );
pMan->timeSort += Abc_Clock() - clk;
//pMan->timeSort += Abc_Clock() - clk;
// save pattern
Cec_ManPatStore( pMan, vPat );
pMan->timeTotal += Abc_Clock() - clkTotal;
}
void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat )
{
// sort pattern
Vec_IntSort( vPat, 0 );
// save pattern
Cec_ManPatStore( pMan, vPat );
}
/**Function*************************************************************

69
src/proof/cec/cecSolve.c
View File

@ -735,6 +735,75 @@ clk2 = Abc_Clock();
Cec_ManSatStop( p );
}
/**Function*************************************************************
Synopsis [Performs one round of solving for the POs of the AIG.]
Description [Labels the nodes that have been proved (pObj->fMark1)
and returns the set of satisfying assignments.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat )
{
int k, nSize;
Vec_IntClear( vPat );
// skip the output number
iStart++;
// get the number of items
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
return iStart;
// extract pattern
for ( k = 0; k < nSize; k++ )
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
return iStart;
}
void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
{
Vec_Str_t * vStatus;
Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
Gia_Obj_t * pObj;
int i, status, iStart = 0;
assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
// reset the manager
if ( pPat )
{
pPat->iStart = Vec_StrSize(pPat->vStorage);
pPat->nPats = 0;
pPat->nPatLits = 0;
pPat->nPatLitsMin = 0;
}
Gia_ManForEachCo( pAig, pObj, i )
{
status = (int)Vec_StrEntry(vStatus, i);
pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
if ( Vec_IntSize(vCexStore) > 0 && status != 1 )
iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat );
if ( status != 0 )
continue;
// save the pattern
if ( pPat && Vec_IntSize(vPat) > 0 )
{
abctime clk3 = Abc_Clock();
Cec_ManPatSavePatternCSat( pPat, vPat );
pPat->timeTotalSave += Abc_Clock() - clk3;
}
// quit if one of them is solved
if ( pPars->fCheckMiter )
break;
}
assert( iStart == Vec_IntSize(vCexStore) );
Vec_IntFree( vPat );
Vec_StrFree( vStatus );
Vec_IntFree( vCexStore );
}
/**Function*************************************************************