Skip to content

A
abc
Commit b6f85cfc by Alan Mishchenko
Options

Enabling counter-example generation in the new BMC engine.

parent 16f79036
Showing with 57 additions and 12 deletions
src/sat/bmc/bmcBmcAnd.c
...@@ -223,7 +223,7 @@ void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int ...@@ -223,7 +223,7 @@ void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap ) void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
{ {
if ( !pObj->fPhase ) if ( !pObj->fPhase )
return; return;
...@@ -233,9 +233,9 @@ void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_In ...@@ -233,9 +233,9 @@ void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_In
{ {
int iLit0 = 1, iLit1 = 1; int iLit0 = 1, iLit1 = 1;
if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap ); Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap, vPiMap );
if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
...@@ -245,17 +245,20 @@ void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_In ...@@ -245,17 +245,20 @@ void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_In
else if ( Gia_ObjIsRo(p, pObj) ) else if ( Gia_ObjIsRo(p, pObj) )
assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 ); assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 );
else if ( Gia_ObjIsPi(p, pObj) ) else if ( Gia_ObjIsPi(p, pObj) )
{
Vec_IntPush( vPiMap, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) ); Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
}
else assert( 0 ); else assert( 0 );
} }
void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap ) void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, iLit; int i, iLit;
Gia_ManForEachObjVec( vCos, p, pObj, i ) Gia_ManForEachObjVec( vCos, p, pObj, i )
{ {
assert( Gia_ObjIsCo(pObj) ); assert( Gia_ObjIsCo(pObj) );
Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit ); Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit );
} }
...@@ -276,12 +279,12 @@ void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_ ...@@ -276,12 +279,12 @@ void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose ) Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose, Vec_Int_t ** pvPiMap )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Vec_Ptr_t * vStates, * vBegins; Vec_Ptr_t * vStates, * vBegins;
Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap; Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap, * vPiMap;
unsigned * pStateF, * pStateP; unsigned * pStateF, * pStateP;
int f, i, iFirst; int f, i, iFirst;
Gia_ManCleanPhase( pGia ); Gia_ManCleanPhase( pGia );
...@@ -290,6 +293,7 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, ...@@ -290,6 +293,7 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd,
// perform ternary simulation // perform ternary simulation
vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst ); vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst );
// go backward // go backward
vPiMap = Vec_IntAlloc( 1000 );
vBegins = Vec_PtrStart( Vec_PtrSize(vStates) ); vBegins = Vec_PtrStart( Vec_PtrSize(vStates) );
for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- ) for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- )
{ {
...@@ -336,8 +340,9 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, ...@@ -336,8 +340,9 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd,
Gia_ManForEachPo( pGia, pObj, i ) Gia_ManForEachPo( pGia, pObj, i )
Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 ); Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 );
// find the cone // find the cone
Vec_IntPush( vPiMap, -f-1 );
Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap ); // computes pNew Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap, vPiMap ); // computes pNew
if ( fVerbose ) if ( fVerbose )
printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n", printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n",
f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) ); f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
...@@ -363,6 +368,7 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, ...@@ -363,6 +368,7 @@ Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd,
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
// Gia_ManPrintStats( pNew, NULL ); // Gia_ManPrintStats( pNew, NULL );
*pvPiMap = vPiMap;
return pNew; return pNew;
} }
...@@ -487,7 +493,7 @@ int Gia_ManBmcAssignVarIds( Bmc_Mna_t * p, Vec_Int_t * vIns, Vec_Int_t * vUsed, ...@@ -487,7 +493,7 @@ int Gia_ManBmcAssignVarIds( Bmc_Mna_t * p, Vec_Int_t * vIns, Vec_Int_t * vUsed,
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManBmcAddCnf( Bmc_Mna_t * p, Gia_Man_t * pGia, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts ) void Gia_ManBmcAddCnf( Bmc_Mna_t * p, Gia_Man_t * pGia, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts, Vec_Int_t * vSatMap )
{ {
Gia_Man_t * pNew = Gia_ManBmcDupCone( pGia, vIns, vNodes, vOuts ); Gia_Man_t * pNew = Gia_ManBmcDupCone( pGia, vIns, vNodes, vOuts );
Aig_Man_t * pAig = Gia_ManToAigSimple( pNew ); Aig_Man_t * pAig = Gia_ManToAigSimple( pNew );
...@@ -655,7 +661,7 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -655,7 +661,7 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// create another slice // create another slice
Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
// create CNF in the SAT solver // create CNF in the SAT solver
Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs, NULL );
// try solving the outputs // try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{ {
...@@ -713,6 +719,41 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -713,6 +719,41 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Generate counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManBmcCexGen( Gia_Man_t * p, sat_solver * pSat, Vec_Int_t * vPiMap, Vec_Int_t * vSatMap, int iOut )
{
Abc_Cex_t * pCex;
int i, iOrigPi, iFramePi = 0, iSatVar, iFrame = -1;
pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), iOut / Gia_ManPoNum(p) + 1 );
pCex->iPo = iOut % Gia_ManPoNum(p);
pCex->iFrame = iOut / Gia_ManPoNum(p);
// fill in the input values
Vec_IntForEachEntry( vPiMap, iOrigPi, i )
{
if ( iOrigPi < 0 )
{
iFrame = -iOrigPi-1;
continue;
}
// iOrigPi in iFrame has index iFramePi in the frames
iSatVar = Vec_IntEntry( vSatMap, iFramePi );
if ( sat_solver_var_value(pSat, iSatVar) )
Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + Gia_ManPiNum(p) * iFrame + iFramePi );
iFramePi++;
}
return pCex;
}
/**Function*************************************************************
Synopsis [] Synopsis []
Description [] Description []
...@@ -725,10 +766,11 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -725,10 +766,11 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{ {
Bmc_Mna_t * p; Bmc_Mna_t * p;
Vec_Int_t * vPiMap, * vSatMap;
int nFramesMax, f, i=0, Lit, status, RetValue = -2; int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
p = Bmc_MnaAlloc(); p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose ); p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &vPiMap );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
...@@ -742,6 +784,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -742,6 +784,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" ); printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
} }
vSatMap = Vec_IntStartFull( Gia_ManPoNum(p->pFrames) );
for ( f = 0; f < nFramesMax; f++ ) for ( f = 0; f < nFramesMax; f++ )
{ {
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
...@@ -749,7 +792,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -749,7 +792,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// create another slice // create another slice
Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
// create CNF in the SAT solver // create CNF in the SAT solver
Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs, vSatMap );
// try solving the outputs // try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{ {
...@@ -782,6 +825,8 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -782,6 +825,8 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f ); printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
else else
{ {
// ABC_FREE( pGia->pCexSeq );
// pGia->pCexSeq = Gia_ManBmcCexGen( pGia, p->pSat, vPiMap, vSatMap, i );
printf( "Output %d of miter \"%s\" was asserted in frame %d. ", printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f ); i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment