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

Enabled saving vector of counter-examples in the ABC framework.

This commit is contained in:
Alan Mishchenko 2011-08-02 00:31:03 +07:00
parent 4e9f972489
commit 6c6c0b0686
9 changed files with 112 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/aig/aig.h
View File

@ -154,7 +154,7 @@ struct Aig_Man_t_
Vec_Int_t * vFlopNums;
Vec_Int_t * vFlopReprs;
Abc_Cex_t * pSeqModel;
Vec_Ptr_t * pSeqModelVec; // vector of counter-examples (for sequential miters)
Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
Aig_Man_t * pManHaig;

4
src/aig/aig/aigMan.c
View File

@ -211,8 +211,8 @@ void Aig_ManStop( Aig_Man_t * p )
Vec_IntFreeP( &p->vProbs );
Vec_IntFreeP( &p->vCiNumsOrig );
Vec_PtrFreeP( &p->vMapped );
if ( p->pSeqModelVec )
Vec_PtrFreeFree( p->pSeqModelVec );
if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec );
ABC_FREE( p->pTerSimData );
ABC_FREE( p->pFastSim );
ABC_FREE( p->pData );

9
src/aig/saig/saigBmc3.c
View File

@ -612,8 +612,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
assert( p->pAig->pSeqModelVec == NULL );
p->pAig->pSeqModelVec = p->vCexes;
assert( p->pAig->vSeqModelVec == NULL );
p->pAig->vSeqModelVec = p->vCexes;
p->vCexes = NULL;
}
// Vec_PtrFreeFree( p->vCexes );
@ -1133,7 +1133,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
return 0;
}
// consider the next timeframe
pPars->iFrame = f;
if ( RetValue == -1 && pPars->nStart == 0 )
pPars->iFrame = f;
// resize the array
Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
// map nodes of this section
@ -1206,6 +1207,7 @@ clkOther += clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
RetValue = 0;
continue;
}
// solve this output
@ -1254,6 +1256,7 @@ clkOther += clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
RetValue = 0;
}
else
{

63
src/aig/saig/saigCexMin.c
View File

@ -252,7 +252,7 @@ void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_
SeeAlso []
***********************************************************************/
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
{
Vec_Vec_t * vFramePPs;
Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
@ -302,6 +302,67 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
return vFramePPs;
}
/**Function*************************************************************
Synopsis [Collects phase and priority of all timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
{
Vec_Vec_t * vFramePPs;
Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
Aig_Obj_t * pObj;
int i, f, nPrioOffset;
// initialize phase and priority
Aig_ManForEachObj( pAig, pObj, i )
pObj->iData = -1;
// set the constant node to higher priority than the flops
vFramePPs = Vec_VecStart( pCex->iFrame+1 );
nPrioOffset = pCex->nRegs;
Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
vRoots = Vec_IntAlloc( 1000 );
//printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset );
for ( f = 0; f <= pCex->iFrame; f++ )
{
int nPiCount = 0;
// fill in PP for the CIs
vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
assert( Vec_IntSize(vFramePPsOne) == 0 );
Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
{
assert( Aig_ObjIsPi(pObj) );
if ( Saig_ObjIsPi(pAig, pObj) )
Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
else if ( f == 0 )
Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
else
{
Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
}
//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
}
//printf( "\n" );
// compute the PP info
Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
}
Vec_IntFree( vRoots );
// check the output
pObj = Aig_ManPo( pAig, pCex->iPo );
assert( Aig_LitIsCompl(pObj->iData) );
return vFramePPs;
}
/**Function*************************************************************

2
src/base/abc/abc.h
View File

@ -203,7 +203,7 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vSupps; // CO support information
int * pModel; // counter-example (for miters)
Abc_Cex_t * pSeqModel; // counter-example (for sequential miters)
Vec_Ptr_t * pSeqModelVec; // vector of counter-examples (for sequential miters)
Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pExcare; // the EXDC network (if given)
void * pData; // misc

4
src/base/abc/abcNtk.c
View File

@ -995,8 +995,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
if ( pNtk->pSeqModelVec )
Vec_PtrFreeFree( pNtk->pSeqModelVec );
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
TotalMemory = 0;
TotalMemory += pNtk->pMmObj? Mem_FixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Mem_StepReadMemUsage(pNtk->pMmStep) : 0;

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

@ -410,9 +410,38 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc,
***********************************************************************/
void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex )
{
// update CEX
ABC_FREE( pAbc->pCex );
pAbc->pCex = *ppCex;
*ppCex = NULL;
// remove CEX vector
if ( pAbc->vCexVec )
{
Vec_PtrFreeFree( pAbc->vCexVec );
pAbc->vCexVec = NULL;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
{
// update CEX vector
if ( pAbc->vCexVec )
Vec_PtrFreeFree( pAbc->vCexVec );
pAbc->vCexVec = *pvCexVec;
*pvCexVec = NULL;
// remove CEX
ABC_FREE( pAbc->pCex );
}
/**Function*************************************************************
@ -19015,14 +19044,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
if ( pPars->fSolveAll && pPars->fDropSatOuts )
{
if ( pNtk->pSeqModelVec == NULL )
if ( pNtk->vSeqModelVec == NULL )
printf( "The array of counter-examples is not available.\n" );
else if ( Vec_PtrSize(pNtk->pSeqModelVec) != Abc_NtkPoNum(pNtk) )
else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) )
printf( "The array size does not match the number of outputs.\n" );
else
{
extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
Abc_NtkDropSatOutputs( pNtk, pNtk->pSeqModelVec, pPars->fVerbose );
Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose );
pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0 );
if ( pNtkRes == NULL )
{
@ -19032,6 +19061,8 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
}
if ( pNtk->vSeqModelVec )
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
return 0;
usage:

6
src/base/abci/abcDar.c
View File

@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
if ( pNtk->pSeqModelVec )
Vec_PtrFreeFree( pNtk->pSeqModelVec );
pNtk->pSeqModelVec = pMan->pSeqModelVec; pMan->pSeqModelVec = NULL;
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
else // if ( RetValue == 0 )

1
src/base/main/mainInt.h
View File

@ -98,6 +98,7 @@ struct Abc_Frame_t_
Gia_Man_t * pGia;
Gia_Man_t * pGia2;
Abc_Cex_t * pCex;
Vec_Ptr_t * vCexVec;
void * pSave1;
void * pSave2;