Skip to content

A
abc
Commit dd71ca94 by Alan Mishchenko
Options

Added cex generation for clustered reachability.

parent 813245b2
Showing with 302 additions and 37 deletions
abclib.dsp
......@@ -4163,6 +4163,10 @@ SOURCE=.\src\aig\llb\llb3Nonlin.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb4Cex.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\llb\llb4Cluster.c
# End Source File
# Begin Source File
......
src/aig/llb/llb4Cex.c 0 → 100644
/**CFile****************************************************************
FileName [llb2Cex.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Non-linear quantification scheduling.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Cex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
#include "cnf.h"
#include "satSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Translates a sequence of states into a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose )
{
Abc_Cex_t * pCex;
Cnf_Dat_t * pCnf;
Vec_Int_t * vAssumps;
sat_solver * pSat;
Aig_Obj_t * pObj;
unsigned * pNext, * pThis;
int i, k, iBit, status, nRegs, clk = clock();
/*
Vec_PtrForEachEntry( unsigned *, vStates, pNext, i )
{
printf( "%4d : ", i );
Extra_PrintBinary( stdout, pNext, Aig_ManRegNum(pAig) );
printf( "\n" );
}
*/
// derive SAT solver
nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
pAig->nRegs = nRegs;
// Cnf_DataTranformPolarity( pCnf, 0 );
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
printf( "Llb4_Nonlin4TransformCex(): Counter-example generation has failed.\n" );
Cnf_DataFree( pCnf );
return NULL;
}
// simplify the problem
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
printf( "Llb4_Nonlin4TransformCex(): SAT solver is invalid.\n" );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return NULL;
}
// start the counter-example
pCex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), Vec_PtrSize(vStates) );
pCex->iFrame = Vec_PtrSize(vStates)-1;
pCex->iPo = -1;
// solve each time frame
iBit = Saig_ManRegNum(pAig);
pThis = Vec_PtrEntry( vStates, 0 );
vAssumps = Vec_IntAlloc( 2 * Aig_ManRegNum(pAig) );
Vec_PtrForEachEntryStart( unsigned *, vStates, pNext, i, 1 )
{
// create assumptions
Vec_IntClear( vAssumps );
Saig_ManForEachLo( pAig, pObj, k )
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Aig_InfoHasBit(pThis,k) ) );
Saig_ManForEachLi( pAig, pObj, k )
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Aig_InfoHasBit(pNext,k) ) );
// solve SAT problem
status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
// if the problem is SAT, get the counterexample
if ( status != l_True )
{
printf( "Llb4_Nonlin4TransformCex(): There is no transition between state %d and %d.\n", i-1, i );
Vec_IntFree( vAssumps );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
ABC_FREE( pCex );
return NULL;
}
// get the assignment of PIs
Saig_ManForEachPi( pAig, pObj, k )
if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
Aig_InfoSetBit( pCex->pData, iBit + k );
// update the counter
iBit += Saig_ManPiNum(pAig);
pThis = pNext;
}
// add the last frame when the property fails
Vec_IntClear( vAssumps );
Saig_ManForEachPo( pAig, pObj, k )
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
// add clause
status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) );
if ( status == 0 )
{
printf( "Llb4_Nonlin4TransformCex(): The SAT solver is unsat after adding last clause.\n" );
Vec_IntFree( vAssumps );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
ABC_FREE( pCex );
return NULL;
}
// create assumptions
Vec_IntClear( vAssumps );
Saig_ManForEachLo( pAig, pObj, k )
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Aig_InfoHasBit(pThis,k) ) );
// solve the last frame
status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status != l_True )
{
printf( "Llb4_Nonlin4TransformCex(): There is no last transition that makes the property fail.\n" );
Vec_IntFree( vAssumps );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
ABC_FREE( pCex );
return NULL;
}
// get the assignment of PIs
Saig_ManForEachPi( pAig, pObj, k )
if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
Aig_InfoSetBit( pCex->pData, iBit + k );
iBit += Saig_ManPiNum(pAig);
assert( iBit == pCex->nBits );
// free the sat_solver
Vec_IntFree( vAssumps );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
// verify counter-example
status = Saig_ManFindFailedPoCex( pAig, pCex );
if ( status >= 0 && status < Saig_ManPoNum(pAig) )
pCex->iPo = status;
else
{
printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
ABC_FREE( pCex );
return NULL;
}
// report the results
// if ( fVerbose )
// Abc_PrintTime( 1, "SAT-based cex generation time", clock() - clk );
return pCex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/aig/llb/llb4Cluster.c
......@@ -402,7 +402,7 @@ void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrde
// create the BDD manager
vOrder = Llb_Nonlin4FindOrder( pAig, &nVarNum );
dd = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder );
......
src/aig/llb/llb4Nonlin.c
......@@ -384,6 +384,7 @@ Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t
else
{
Aig_ManForEachPi( pAig, pObj, i )
// Saig_ManForEachLo( pAig, pObj, i )
Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
}
return vVars2Q;
......@@ -468,12 +469,10 @@ DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * v
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLo( pAig, pObj, i )
{
if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 2 )
continue;
// get the correspoding flop input variable
pObjLi = Saig_ObjLoToLi(pAig, pObj);
bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 0 )
if ( pValues[Llb_MnxBddVar(vOrder, pObj)] != 1 )
bVar = Cudd_Not(bVar);
// create cube
bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
......@@ -496,37 +495,47 @@ DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * v
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p )
Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, Vec_Ptr_t * vStates, int fVerbose )
{
Abc_Cex_t * pCex;
Abc_Cex_t * pCex = NULL;
Aig_Obj_t * pObj;
DdNode * bState, * bImage, * bOneCube, * bRing;
int i, v, RetValue, nPiOffset;
char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
int i, v, RetValue, nPiOffset = -1, clk = clock();
char * pValues;
assert( Vec_PtrSize(p->vRings) > 0 );
// disable the timeout
p->dd->TimeStop = 0;
// update quantifiable vars
Vec_IntFreeP( &p->vVars2Q );
p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 );
// allocate room for the counter-example
pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
// get the last cube
pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
bOneCube = Cudd_bddIntersect( p->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad ); Cudd_Ref( bOneCube );
RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
Cudd_RecursiveDeref( p->dd, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// record the cube
if ( vStates == NULL )
{
// allocate room for the counter-example
pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
// write PIs of the counter-example
nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
}
else
{
Saig_ManForEachLo( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( (unsigned *)Vec_PtrEntryLast(vStates), i );
}
// update quantifiable vars
Vec_IntFreeP( &p->vVars2Q );
p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 );
// write state in terms of NS variables
if ( Vec_PtrSize(p->vRings) > 1 )
......@@ -545,7 +554,7 @@ Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p )
Cudd_RecursiveDeref( p->dd, bState );
// intersect with the previous set
bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube );
bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube );
Cudd_RecursiveDeref( p->dd, bImage );
// find any assignment of the BDD
......@@ -553,11 +562,21 @@ Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p )
Cudd_RecursiveDeref( p->dd, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset -= Saig_ManPiNum(p->pAig);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
// record the cube
if ( vStates == NULL )
{
// write PIs of counter-example
nPiOffset -= Saig_ManPiNum(p->pAig);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( pCex->pData, nPiOffset + i );
}
else
{
Saig_ManForEachLo( p->pAig, pObj, i )
if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
Aig_InfoSetBit( (unsigned *)Vec_PtrEntry(vStates, v), i );
}
// check that we get the init state
if ( v == 0 )
......@@ -565,19 +584,24 @@ Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p )
Saig_ManForEachLo( p->pAig, pObj, i )
assert( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 0 );
break;
}
}
// write state in terms of NS variables
bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues ); Cudd_Ref( bState );
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
assert( vStates != NULL || nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
//Abc_CexPrint( pCex );
RetValue = Saig_ManFindFailedPoCex( p->pAig, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAig) ); // invalid CEX!!!
pCex->iPo = RetValue;
if ( pCex )
{
//Abc_CexPrint( pCex );
RetValue = Saig_ManFindFailedPoCex( p->pAig, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAig) ); // invalid CEX!!!
pCex->iPo = RetValue;
}
// cleanup
ABC_FREE( pValues );
// if ( fVerbose )
// Abc_PrintTime( 1, "BDD-based cex generation time", clock() - clk );
return pCex;
}
......@@ -644,9 +668,18 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) )
{
assert( p->pAig->pSeqModel == NULL );
if ( !p->pPars->fBackward )
p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p );
if ( !p->pPars->fSilent )
if ( p->pPars->fCluster )
{
Vec_Ptr_t * vStates = Vec_PtrAllocSimInfo( Vec_PtrSize(p->vRings), Aig_BitWordNum(Aig_ManRegNum(p->pAig)) );
Vec_PtrCleanSimInfo( vStates, 0, Aig_BitWordNum(Aig_ManRegNum(p->pAig)) );
p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, vStates, p->pPars->fVerbose );
ABC_FREE( p->pAig->pSeqModel );
p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, p->pPars->fVerbose );
Vec_PtrFreeP( &vStates );
}
else
p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, NULL, p->pPars->fVerbose );
if ( !p->pPars->fSilent && p->pAig->pSeqModel )
{
if ( !p->pPars->fBackward )
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, nIters );
......@@ -905,6 +938,32 @@ void Llb_MnxStop( Llb_Mnx_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_MnxCheckNextStateVars( Llb_Mnx_t * p )
{
Aig_Obj_t * pObj;
int i, Counter0 = 0, Counter1 = 0;
Saig_ManForEachLi( p->pAig, pObj, i )
if ( Saig_ObjIsLo(p->pAig, Aig_ObjFanin0(pObj)) )
{
if ( Aig_ObjFaninC0(pObj) )
Counter0++;
else
Counter1++;
}
printf( "Total = %d. Direct LO = %d. Compl LO = %d.\n", Aig_ManRegNum(p->pAig), Counter1, Counter0 );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
......@@ -924,6 +983,7 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
int clk = clock();
pMnn = Llb_MnxStart( pAig, pPars );
//Llb_MnxCheckNextStateVars( pMnn );
RetValue = Llb_Nonlin4Reachability( pMnn );
pMnn->timeTotal = clock() - clk;
Llb_MnxStop( pMnn );
......
src/aig/llb/llbInt.h
......@@ -182,6 +182,9 @@ extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, V
/*=== llb3Nonlin.c ======================================================*/
extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
/*=== llb4Cex.c =======================================================*/
extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose );
/*=== llb4Cluster.c =======================================================*/
extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
/*=== llb4Image.c =======================================================*/
......
src/aig/llb/module.make
......@@ -17,6 +17,7 @@ SRC += src/aig/llb/llb.c \
src/aig/llb/llb2Image.c \
src/aig/llb/llb3Image.c \
src/aig/llb/llb3Nonlin.c \
src/aig/llb/llb4Cex.c \
src/aig/llb/llb4Cluster.c \
src/aig/llb/llb4Image.c \
src/aig/llb/llb4Nonlin.c
src/base/abci/abc.c
......@@ -8535,6 +8535,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
{
extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
// Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
Ssm_ManExperiment( "m\\manyclocks2.ssim", "m\\manyclocks2_.ssim" );
}
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
......
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