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

Interfacing SAT sweepers.

This commit is contained in:
Alan Mishchenko 2023-02-02 09:15:42 -08:00
parent 70a07869c6
commit acdb94d1d3
2 changed files with 127 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -37280,12 +37280,13 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose );
extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle );
extern Gia_Man_t * Gia_ManIvyFraig( Gia_Man_t * p, int nConfLimit, int fUseProve, int fVerbose );
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0;
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0, fUseIvy = 0, fUseProve = 0;
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF )
{
switch ( c )
{
@ -37388,6 +37389,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nGenIters < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
nMaxNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nMaxNodes < 0 )
goto usage;
break;
case 'r':
pPars->fRewriting ^= 1;
break;
@ -37418,6 +37430,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fUseSave ^= 1;
break;
case 'o':
fUseIvy ^= 1;
break;
case 'p':
fUseProve ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@ -37438,6 +37456,8 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose );
return 0;
}
else if ( fUseIvy && (!nMaxNodes || Gia_ManAndNum(pAbc->pGia) < nMaxNodes) )
pTemp = Gia_ManIvyFraig( pAbc->pGia, pPars->nBTLimit, fUseProve, pPars->fVerbose );
else if ( fUseAlgo )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
@ -37458,7 +37478,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxyswvh]\n" );
Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-rmdckngxysopwvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@ -37469,6 +37489,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
Abc_Print( -2, "\t-M num : the node count limit to call the old sweeper [default = %d]\n", nMaxNodes );
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" );
@ -37479,6 +37500,8 @@ usage:
Abc_Print( -2, "\t-x : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" );
Abc_Print( -2, "\t-y : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" );
Abc_Print( -2, "\t-s : toggle dumping equivalences into a file [default = %s]\n", fUseSave? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" );
Abc_Print( -2, "\t-p : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "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");

100
src/base/abci/abcIvy.c
View File

@ -25,6 +25,7 @@
#include "proof/fraig/fraig.h"
#include "map/mio/mio.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
@ -1141,6 +1142,105 @@ Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
return vArray;
}
/**Function*************************************************************
Synopsis [Convert Ivy into Gia.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Ivy_Obj_t * Gia_ObjChild0Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Ivy_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
static inline Ivy_Obj_t * Gia_ObjChild1Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Ivy_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
Ivy_Man_t * Gia_ManToIvySimple( Gia_Man_t * p )
{
Ivy_Man_t * pNew;
Gia_Obj_t * pObj; int i;
Ivy_Obj_t ** ppNodes = ABC_FALLOC( Ivy_Obj_t *, Gia_ManObjNum(p) );
// create the new manager
pNew = Ivy_ManStart( Gia_ManObjNum(p) );
// create the PIs
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
ppNodes[i] = Ivy_And( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, i), Gia_ObjChild1Copy3(ppNodes, pObj, i) );
else if ( Gia_ObjIsCi(pObj) )
ppNodes[i] = Ivy_ObjCreatePi( pNew );
else if ( Gia_ObjIsCo(pObj) )
ppNodes[i] = Ivy_ObjCreatePo( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, Gia_ObjId(p, pObj)) );
else if ( Gia_ObjIsConst0(pObj) )
ppNodes[i] = Ivy_Not(Ivy_ManConst1(pNew));
else
assert( 0 );
assert( i == 0 || Ivy_ObjId(ppNodes[i]) == i );
}
ABC_FREE( ppNodes );
return pNew;
}
static inline int Gia_ObjChild0Copy4( int * pNodes, Ivy_Obj_t * pObj ) { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin0)->Id], Ivy_IsComplement(pObj->pFanin0) ); }
static inline int Gia_ObjChild1Copy4( int * pNodes, Ivy_Obj_t * pObj ) { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin1)->Id], Ivy_IsComplement(pObj->pFanin1) ); }
Gia_Man_t * Gia_ManFromIvySimple( Ivy_Man_t * p )
{
Gia_Man_t * pNew;
Ivy_Obj_t * pObj;
int i, * pNodes = ABC_FALLOC( int, Ivy_ManObjIdMax(p) + 1 );
pNew = Gia_ManStart( Ivy_ManObjIdMax(p) );
pNew->pName = Abc_UtilStrsav( "from_ivy" );
Ivy_ManForEachObj( p, pObj, i )
{
if ( Ivy_ObjIsAnd(pObj) )
pNodes[pObj->Id] = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy4(pNodes, pObj), Gia_ObjChild1Copy4(pNodes, pObj) );
else if ( Ivy_ObjIsCi(pObj) )
pNodes[pObj->Id] = Gia_ManAppendCi( pNew );
else if ( Ivy_ObjIsCo(pObj) )
pNodes[pObj->Id] = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy4(pNodes, pObj) );
else if ( Ivy_ObjIsConst1(pObj) )
pNodes[pObj->Id] = 1;
else
assert( 0 );
}
ABC_FREE( pNodes );
return pNew;
}
Gia_Man_t * Gia_ManIvyFraig( Gia_Man_t * p, int nConfLimit, int fUseProve, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Gia_Man_t * pNew;
Ivy_Man_t * pMan, * pTemp;
pMan = Gia_ManToIvySimple( p );
if ( pMan == NULL )
return NULL;
Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose;
pParams->fProve = fUseProve;
pParams->fDoSparse = 1;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
pNew = Gia_ManFromIvySimple( pMan );
if ( pMan->pData )
{
p->pCexSeq = Abc_CexDeriveFromCombModel( (int *)pMan->pData, Ivy_ManPiNum(pMan), 0, -1 );
p->pCexSeq->iPo = Gia_ManFindFailedPoCex( p, p->pCexSeq, 0 );
ABC_FREE( pMan->pData );
}
Ivy_ManStop( pTemp );
Ivy_ManStop( pMan );
return pNew;
}
Gia_Man_t * Gia_ManIvyFraigTest( Gia_Man_t * p, int nConfLimit, int fVerbose )
{
Ivy_Man_t * pMan = Gia_ManToIvySimple( p );
Gia_Man_t * pNew = Gia_ManFromIvySimple( pMan );
Ivy_ManStop( pMan );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////