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

Making &cec use precomputed simulation info.

This commit is contained in:
Alan Mishchenko 2020-08-12 19:32:42 -07:00
parent b74b7dfc2d
commit 850d39fec3
4 changed files with 43 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -37156,6 +37156,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
if ( pGias[0]->vSimsPi )
{
pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi);
pMiter->nSimWords = pGias[0]->nSimWords;
}
pAbc->Status = Cec_ManVerify( pMiter, pPars );
Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
Gia_ManStop( pMiter );

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

@ -349,6 +349,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_ManStop( p );
return RetValue;
}
if ( pInit->vSimsPi )
{
p->vSimsPi = Vec_WrdDup(pInit->vSimsPi);
p->nSimWords = pInit->nSimWords;
}
// sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;

35
src/proof/cec/cecClass.c
View File

@ -878,19 +878,34 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
if ( pObj->Value )
Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
// perform simulation
p->nWords = 1;
do {
if ( p->pAig->nSimWords )
{
p->nWords = 2*p->pAig->nSimWords;
assert( Vec_WrdSize(p->pAig->vSimsPi) == Gia_ManCiNum(p->pAig) * p->pAig->nSimWords );
//Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
memmove( Vec_PtrEntry(p->vCiSimInfo, i), Vec_WrdEntryP(p->pAig->vSimsPi, i*p->pAig->nSimWords), sizeof(word)*p->pAig->nSimWords );
if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
return 1;
if ( p->pPars->fVerbose )
Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
for ( i = 0; i < 4; i++ )
{
Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
return 1;
}
p->nWords = 2 * p->nWords + 1;
}
while ( p->nWords <= p->pPars->nWords );
else
{
p->nWords = 1;
do {
if ( p->pPars->fVerbose )
Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
for ( i = 0; i < 4; i++ )
{
Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
return 1;
}
p->nWords = 2 * p->nWords + 1;
}
while ( p->nWords <= p->pPars->nWords );
}
return 0;
}

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

@ -360,6 +360,11 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
Vec_IntFreeP( &pAig->vIdsEquiv );
pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
}
if ( pAig->vSimsPi )
{
pIni->vSimsPi = Vec_WrdDup(pAig->vSimsPi);
pIni->nSimWords = pAig->nSimWords;
}
// prepare the managers
// SAT sweeping
@ -368,12 +373,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
pPars->fColorDiff = 1;
// simulation
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nWords = Abc_MaxInt(2*pAig->nSimWords, pPars->nWords);
pParsSim->nFrames = pPars->nRounds;
pParsSim->fCheckMiter = pPars->fCheckMiter;
pParsSim->fDualOut = pPars->fDualOut;
pParsSim->fVerbose = pPars->fVerbose;
pSim = Cec_ManSimStart( p->pAig, pParsSim );
pSim = Cec_ManSimStart( pIni, pParsSim );
// SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
@ -386,7 +391,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
clk = Abc_Clock();
if ( p->pAig->pReprs == NULL )
{
if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
if ( Cec_ManSimClassesPrepare(pSim, -1) || (!p->pAig->nSimWords && Cec_ManSimClassesRefine(pSim)) )
{
Gia_ManStop( p->pAig );
p->pAig = NULL;