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

Dumping equivalences after SAT sweeping.

This commit is contained in:
Alan Mishchenko 2022-06-26 19:45:03 -07:00
parent 8cf3f54208
commit adcc398bc3
5 changed files with 172 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/aig/miniaig/miniaig.h
View File

@ -368,6 +368,20 @@ static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsi
Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) );
return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 );
}
static char * Mini_AigPhase( Mini_Aig_t * p )
{
char * pRes = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) );
int i;
Mini_AigForEachAnd( p, i )
{
int iFaninLit0 = Mini_AigNodeFanin0( p, i );
int iFaninLit1 = Mini_AigNodeFanin1( p, i );
int Phase0 = pRes[Mini_AigLit2Var(iFaninLit0)] ^ Mini_AigLitIsCompl(iFaninLit0);
int Phase1 = pRes[Mini_AigLit2Var(iFaninLit1)] ^ Mini_AigLitIsCompl(iFaninLit1);
pRes[i] = Phase0 & Phase1;
}
return pRes;
}
// procedure to check the topological order during AIG construction
static int Mini_AigCheck( Mini_Aig_t * p )

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

@ -37195,13 +37195,14 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
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 );
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0;
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF )
{
switch ( c )
{
@ -37331,6 +37332,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'y':
fUseAlgoY ^= 1;
break;
case 's':
fUseSave ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@ -37346,7 +37350,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
return 1;
}
if ( fUseAlgo )
if ( fUseSave )
{
Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose );
return 0;
}
else if ( fUseAlgo )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
@ -37354,7 +37363,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoY )
pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle );
else
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
if ( pAbc->pGia->pCexSeq != NULL )
{
@ -37366,7 +37375,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxywvh]\n" );
Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxyswvh]\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 );
@ -37386,6 +37395,7 @@ usage:
Abc_Print( -2, "\t-g : toggle using another new implementation [default = %s]\n", fUseAlgoG? "yes": "no" );
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-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");

8
src/misc/vec/vecWrd.h
View File

@ -195,6 +195,14 @@ static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars )
}
return p;
}
static inline int Vec_WrdShiftOne( Vec_Wrd_t * p, int nWords )
{
int i, nObjs = p->nSize/nWords;
assert( nObjs * nWords == p->nSize );
for ( i = 0; i < nObjs; i++ )
p->pArray[i*nWords] <<= 1;
return nObjs;
}
/**Function*************************************************************

1
src/proof/acec/acecXor.c
View File

@ -466,6 +466,7 @@ void Gia_ManTestXor( Gia_Man_t * p )
}
Vec_WrdFree( vSimsPi );
Vec_WrdFree( vSims );
nWords = 0;
}
////////////////////////////////////////////////////////////////////////

135
src/proof/cec/cecSatG2.c
View File

@ -1877,9 +1877,9 @@ void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )
abctime clk = Abc_Clock();
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec4_ManSetParams( pPars );
Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
pPars->fVerbose = fVerbose;
pPars->nBTLimit = nConfs;
Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
if ( fVerbose )
Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
}
@ -1912,6 +1912,139 @@ int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose )
return Cec4_ManPerformSweeping( p, pPars, NULL, 1 );
}
/**Function*************************************************************
Synopsis [Internal simulation APIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec4_ManSimulateTest5Int( Gia_Man_t * p, int nConfs, int fVerbose )
{
abctime clk = Abc_Clock();
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec4_ManSetParams( pPars );
pPars->fVerbose = fVerbose;
pPars->nBTLimit = nConfs;
Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
if ( fVerbose )
Abc_PrintTime( 1, "Equivalence detection time", Abc_Clock() - clk );
}
Gia_Man_t * Gia_ManLocalRehash( Gia_Man_t * p )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_ManAppendCi( pNew );
else if ( Gia_ObjIsCo(pObj) )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManForEachObj1( p, pObj, i )
{
int iLitNew = Gia_ManObj(pTemp, Abc_Lit2Var(pObj->Value))->Value;
if ( iLitNew == ~0 )
pObj->Value = iLitNew;
else
pObj->Value = Abc_LitNotCond(iLitNew, Abc_LitIsCompl(pObj->Value));
}
Gia_ManStop( pTemp );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
Vec_Int_t * Cec4_ManComputeMapping( Gia_Man_t * p, Gia_Man_t * pAig, int fVerbose )
{
Gia_Obj_t * pObj;
Vec_Int_t * vReprs = Vec_IntStartFull( Gia_ManObjNum(p) );
int * pAig2Abc = ABC_FALLOC( int, Gia_ManObjNum(pAig) );
int i, nConsts = 0, nReprs = 0;
pAig2Abc[0] = 0;
Gia_ManForEachCand( p, pObj, i )
{
int iLitGia = pObj->Value, iReprGia;
if ( iLitGia == -1 )
continue;
iReprGia = Gia_ObjReprSelf( pAig, Abc_Lit2Var(iLitGia) );
if ( pAig2Abc[iReprGia] == -1 )
pAig2Abc[iReprGia] = i;
else
{
int iLitGia2 = Gia_ManObj(p, pAig2Abc[iReprGia] )->Value;
assert( Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia)) == Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia2)) );
assert( i > pAig2Abc[iReprGia] );
Vec_IntWriteEntry( vReprs, i, pAig2Abc[iReprGia] );
if ( pAig2Abc[iReprGia] == 0 )
nConsts++;
else
nReprs++;
}
}
ABC_FREE( pAig2Abc );
if ( fVerbose )
printf( "Found %d const reprs and %d other reprs.\n", nConsts, nReprs );
return vReprs;
}
void Cec4_ManVerifyEquivs( Gia_Man_t * p, Vec_Int_t * vRes, int fVerbose )
{
int i, iRepr, nWords = 4; word * pSim0, * pSim1;
Vec_Wrd_t * vSimsCi = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWords );
int nObjs = Vec_WrdShiftOne( vSimsCi, nWords ), nFails = 0;
Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsCi, 0 );
assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
assert( nObjs == Gia_ManCiNum(p) );
Vec_IntForEachEntry( vRes, iRepr, i )
{
if ( iRepr == -1 )
continue;
assert( i > iRepr );
pSim0 = Vec_WrdEntryP( vSims, nWords*i );
pSim1 = Vec_WrdEntryP( vSims, nWords*iRepr );
if ( (pSim0[0] ^ pSim1[0]) & 1 )
nFails += !Abc_TtOpposite(pSim0, pSim1, nWords);
else
nFails += !Abc_TtEqual(pSim0, pSim1, nWords);
}
Vec_WrdFree( vSimsCi );
Vec_WrdFree( vSims );
if ( nFails )
printf( "Verification failed at %d nodes.\n", nFails );
else if ( fVerbose )
printf( "Verification succeeded for all (%d) nodes.\n", Gia_ManCandNum(p) );
}
void Cec4_ManConvertToLits( Gia_Man_t * p, Vec_Int_t * vRes )
{
Gia_Obj_t * pObj; int i, iRepr;
Gia_ManSetPhase( p );
Gia_ManForEachObj( p, pObj, i )
if ( (iRepr = Vec_IntEntry(vRes, i)) >= 0 )
Vec_IntWriteEntry( vRes, i, Abc_Var2Lit(iRepr, Gia_ManObj(p, iRepr)->fPhase ^ pObj->fPhase) );
}
void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose )
{
Vec_Int_t * vRes = NULL;
Gia_Man_t * pAig = Gia_ManLocalRehash( p );
Cec4_ManSimulateTest5Int( pAig, nConfs, fVerbose );
vRes = Cec4_ManComputeMapping( p, pAig, fVerbose );
Cec4_ManVerifyEquivs( p, vRes, fVerbose );
Cec4_ManConvertToLits( p, vRes );
Vec_IntDumpBin( "_temp_.equiv", vRes, fVerbose );
Vec_IntFree( vRes );
Gia_ManStop( pAig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////