summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigAbs.c322
-rw-r--r--src/aig/saig/saigBmc.c215
-rw-r--r--src/aig/saig/saigDup.c9
4 files changed, 317 insertions, 230 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index a6f5631b..02db900b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -80,6 +80,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
+extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index b1e36fcc..cfbba7e1 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -28,100 +28,102 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { return ppMap[nFrames*pObj->Id + i]; }
-static inline void Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Create timeframes of the manager for BMC.]
+ Synopsis [Creates SAT solver for BMC.]
- Description [The resulting manager is combinational. The only PO is
- the output of the last frame.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
+sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
{
- Aig_Man_t * pFrames;
- Aig_Obj_t ** ppMap;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pResult;
- int i, f;
- assert( Saig_ManRegNum(pAig) > 0 );
- // start the mapping
- ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
- // start the manager
- pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
- // create variables for register outputs
- Saig_ManForEachLo( pAig, pObj, i )
- {
-// pObj->pData = Aig_ManConst0( pFrames );
- pObj->pData = Aig_ObjCreatePi( pFrames );
- Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
- }
- // add timeframes
- pResult = Aig_ManConst0(pFrames);
+ sat_solver * pSat;
+ Vec_Int_t * vPoLits;
+ Aig_Obj_t * pObjPo, * pObjLi, * pObjLo;
+ int f, i, Lit, Lits[2], iVarOld, iVarNew;
+ // start array of output literals
+ vPoLits = Vec_IntAlloc( nFrames * Saig_ManPoNum(pCnf->pMan) );
+ // create the SAT solver
+ pSat = sat_solver_new();
+ sat_solver_store_alloc( pSat );
+ sat_solver_setnvars( pSat, pCnf->nVars * nFrames );
+
+ // add clauses for the timeframes
for ( f = 0; f < nFrames; f++ )
{
- // map the constant node
- Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
- Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
- // create PI nodes for this frame
- Saig_ManForEachPi( pAig, pObj, i )
- {
- pObj->pData = Aig_ObjCreatePi( pFrames );
- Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
- }
- // add internal nodes of this frame
- Aig_ManForEachNode( pAig, pObj, i )
- {
- pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
- }
- // OR the POs
- Saig_ManForEachPo( pAig, pObj, i )
- pResult = Aig_Or( pFrames, pResult, Aig_ObjChild0Copy(pObj) );
- // create POs for this frame
- if ( f == nFrames - 1 )
- {
-// Saig_ManForEachPo( pAig, pObj, i )
-// {
-// pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-// Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
-// }
- break;
- }
- // save register inputs
- Saig_ManForEachLi( pAig, pObj, i )
+ for ( i = 0; i < pCnf->nClauses; i++ )
{
- pObj->pData = Aig_ObjChild0Copy(pObj);
- Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+ if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+ {
+ printf( "The BMC problem is trivially UNSAT.\n" );
+ sat_solver_delete( pSat );
+ Vec_IntFree( vPoLits );
+ return NULL;
+ }
}
- // transfer to register outputs
- Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ // remember output literal
+ Saig_ManForEachPo( pCnf->pMan, pObjPo, i )
+ Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) );
+ // lift CNF to the next frame
+ Cnf_DataLift( pCnf, pCnf->nVars );
+ }
+ // put CNF back to the original level
+ Cnf_DataLift( pCnf, - pCnf->nVars * nFrames );
+
+ // add auxiliary clauses (output, connectors, initial)
+ // add output clause
+ if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
+ assert( 0 );
+ Vec_IntFree( vPoLits );
+ // add connecting clauses
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // connect to the previous timeframe
+ if ( f > 0 )
{
- pObjLo->pData = pObjLi->pData;
- Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
+ Saig_ManForEachLiLo( pCnf->pMan, pObjLi, pObjLo, i )
+ {
+ iVarOld = pCnf->pVarNums[pObjLi->Id] - pCnf->nVars;
+ iVarNew = pCnf->pVarNums[pObjLo->Id];
+ // add clauses connecting existing variables
+ Lits[0] = toLitCond( iVarOld, 0 );
+ Lits[1] = toLitCond( iVarNew, 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ Lits[0] = toLitCond( iVarOld, 1 );
+ Lits[1] = toLitCond( iVarNew, 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ }
}
+ // lift CNF to the next frame
+ Cnf_DataLift( pCnf, pCnf->nVars );
}
- Aig_ObjCreatePo( pFrames, pResult );
- Aig_ManCleanup( pFrames );
- // remove mapping for the nodes that are no longer there
- for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
- if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
- ppMap[i] = NULL;
- return pFrames;
+ // put CNF back to the original level
+ Cnf_DataLift( pCnf, - pCnf->nVars * nFrames );
+ // add unit clauses
+ Saig_ManForEachLo( pCnf->pMan, pObjLo, i )
+ {
+ assert( pCnf->pVarNums[pObjLo->Id] >= 0 );
+ Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 );
+ if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
+ assert( 0 );
+ }
+ sat_solver_store_mark_roots( pSat );
+ return pSat;
}
/**Function*************************************************************
- Synopsis [Finds the set of variables involved in the UNSAT core.]
+ Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
@@ -130,88 +132,40 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
SeeAlso []
***********************************************************************/
-int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nRegs, int nConfMax, int fVerbose )
+Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
{
+ Vec_Int_t * vCore;
void * pSatCnf;
Intp_Man_t * pManProof;
- Aig_Obj_t * pObj;
- sat_solver * pSat;
- Vec_Int_t * vCore;
- int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
- int i, Lit, RetValue;
- // create the SAT solver
- pSat = sat_solver_new();
- sat_solver_store_alloc( pSat );
- sat_solver_setnvars( pSat, pCnf->nVars );
- for ( i = 0; i < pCnf->nClauses; i++ )
- {
- if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
- {
- printf( "The BMC problem is trivially UNSAT.\n" );
- sat_solver_delete( pSat );
- return NULL;
- }
- }
- Aig_ManForEachPi( pCnf->pMan, pObj, i )
- {
- if ( i == nRegs )
- break;
- assert( pCnf->pVarNums[pObj->Id] >= 0 );
- Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
- if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
- assert( 0 );
- }
- sat_solver_store_mark_roots( pSat );
+ int RetValue;
// solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_Undef )
{
printf( "Conflict limit is reached.\n" );
- sat_solver_delete( pSat );
return NULL;
}
if ( RetValue == l_True )
{
printf( "The BMC problem is SAT.\n" );
- sat_solver_delete( pSat );
return NULL;
}
- printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
+ if ( fVerbose )
+ printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat );
- sat_solver_delete( pSat );
// derive the UNSAT core
pManProof = Intp_ManAlloc();
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
Intp_ManFree( pManProof );
Sto_ManFree( pSatCnf );
- // derive the set of variables on which the core depends
- // collect the variable numbers
- nVars = 0;
- pVars = ALLOC( int, pCnf->nVars );
- memset( pVars, 0, sizeof(int) * pCnf->nVars );
- Vec_IntForEachEntry( vCore, iClause, i )
- {
- pClause1 = pCnf->pClauses[iClause];
- pClause2 = pCnf->pClauses[iClause+1];
- for ( pLit = pClause1; pLit < pClause2; pLit++ )
- {
- if ( pVars[ (*pLit) >> 1 ] == 0 )
- nVars++;
- pVars[ (*pLit) >> 1 ] = 1;
- if ( fVerbose )
- printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
- }
- if ( fVerbose )
- printf( "\n" );
- }
- Vec_IntFree( vCore );
- return pVars;
+ return vCore;
}
+
/**Function*************************************************************
- Synopsis [Labels nodes with the given CNF variable.]
+ Synopsis [Performs proof-based abstraction using BMC of the given depth.]
Description []
@@ -220,15 +174,44 @@ int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nRegs, int nConfMax, int
SeeAlso []
***********************************************************************/
-void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
+Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vCore )
{
- int iVarThis = pCnf->pVarNums[pObj->Id];
- if ( iVarThis >= 0 && iVarThis != iVar )
- return;
- assert( Aig_ObjIsNode(pObj) );
- Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
- Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
- pCnf->pVarNums[pObj->Id] = iVar;
+ Aig_Obj_t * pObj;
+ Vec_Int_t * vFlops;
+ int * pVars, * pFlops;
+ int i, iClause, iReg, * piLit;
+ // mark register variables
+ pVars = ALLOC( int, pCnf->nVars );
+ for ( i = 0; i < pCnf->nVars; i++ )
+ pVars[i] = -1;
+ Saig_ManForEachLi( pCnf->pMan, pObj, i )
+ pVars[ pCnf->pVarNums[pObj->Id] ] = i;
+ Saig_ManForEachLo( pCnf->pMan, pObj, i )
+ pVars[ pCnf->pVarNums[pObj->Id] ] = i;
+ // mark used registers
+ pFlops = CALLOC( int, Aig_ManRegNum(pCnf->pMan) );
+ Vec_IntForEachEntry( vCore, iClause, i )
+ {
+ // skip auxiliary clauses
+ if ( iClause >= pCnf->nClauses * nFrames )
+ continue;
+ // consider the clause
+ iClause = iClause % pCnf->nClauses;
+ for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ )
+ {
+ iReg = pVars[ lit_var(*piLit) ];
+ if ( iReg >= 0 )
+ pFlops[iReg] = 1;
+ }
+ }
+ // collect registers
+ vFlops = Vec_IntAlloc( Aig_ManRegNum(pCnf->pMan) );
+ for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ )
+ if ( pFlops[i] )
+ Vec_IntPush( vFlops, i );
+ free( pFlops );
+ free( pVars );
+ return vFlops;
}
/**Function*************************************************************
@@ -244,65 +227,32 @@ void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iV
***********************************************************************/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
{
+ Aig_Man_t * pResult;
Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Vec_Int_t * vCore;
Vec_Int_t * vFlops;
- Aig_Man_t * pFrames, * pResult;
- Aig_Obj_t ** ppAigToFrames;
- Aig_Obj_t * pObj, * pObjFrame;
- int f, i, * pUnsatCoreVars, clk = clock();
- assert( Saig_ManPoNum(p) == 1 );
+ int clk = clock();
+ assert( Aig_ManRegNum(p) > 0 );
Aig_ManSetPioNumbers( p );
if ( fVerbose )
printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
- // create the timeframes
- pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
- printf( "AIG nodes = %d. Frames = %d.\n", Aig_ManNodeNum(p), Aig_ManNodeNum(pFrames) );
- // convert them into CNF
-// pCnf = Cnf_Derive( pFrames, 0 );
- pCnf = Cnf_DeriveSimple( pFrames, 0 );
- // collect CNF variables involved in UNSAT core
- pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, Saig_ManRegNum(p), nConfMax, 0 );
- if ( pUnsatCoreVars == NULL )
+ // create CNF for the AIG
+ pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
+ // create SAT solver for the unrolled AIG
+ pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+ // compute UNSAT core
+ vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
+ sat_solver_delete( pSat );
+ if ( vCore == NULL )
{
- Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
return NULL;
}
- if ( fVerbose )
- {
- int Counter = 0;
- for ( i = 0; i < pCnf->nVars; i++ )
- Counter += pUnsatCoreVars[i];
- printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
- }
- // map other nodes into existing CNF variables
- Aig_ManForEachNode( pFrames, pObj, i )
- if ( pCnf->pVarNums[pObj->Id] >= 0 )
- Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
- // collect relevant registers
- for ( f = 0; f < nFrames; f++ )
- {
- Saig_ManForEachLo( p, pObj, i )
- {
- pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
- if ( pObjFrame == NULL )
- continue;
- pObjFrame = Aig_Regular(pObjFrame);
- if ( Aig_ObjIsConst1( pObjFrame ) )
- continue;
- assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
- if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
- pObj->fMarkA = 1;
- }
- }
- // collect the flops
- vFlops = Vec_IntAlloc( 1000 );
- Saig_ManForEachLo( p, pObj, i )
- if ( pObj->fMarkA )
- {
- pObj->fMarkA = 0;
- Vec_IntPush( vFlops, i );
- }
+ // collect registers
+ vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
+ Cnf_DataFree( pCnf );
+ Vec_IntFree( vCore );
if ( fVerbose )
{
printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
@@ -310,14 +260,8 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
}
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
- // cleanup
- Aig_ManStop( pFrames );
- Cnf_DataFree( pCnf );
- free( ppAigToFrames );
- free( pUnsatCoreVars );
Vec_IntFree( vFlops );
return pResult;
-
}
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 0bbf63f9..2248fb37 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -21,6 +21,7 @@
#include "saig.h"
#include "cnf.h"
#include "satStore.h"
+#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -33,9 +34,9 @@ struct Saig_Bmc_t_
{
// parameters
int nFramesMax; // the max number of timeframes to consider
+ int nNodesMax; // the max number of nodes to add
int nConfMaxOne; // the max number of conflicts at a target
int nConfMaxAll; // the max number of conflicts for all targets
- int nNodesMax; // the max number of nodes to add
int fVerbose; // enables verbose output
// AIG managers
Aig_Man_t * pAig; // the user's AIG manager
@@ -46,11 +47,14 @@ struct Saig_Bmc_t_
Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
// SAT solver
sat_solver * pSat; // SAT solver
- Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
int nSatVars; // the number of used SAT variables
+ Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
+ // subproblems
Vec_Ptr_t * vTargets; // targets to be solved in this interval
- int iFramelast; // last frame
+ int iFrameLast; // last frame
int iOutputLast; // last output
+ int iFrameFail; // failed frame
+ int iOutputFail; // failed output
};
static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
@@ -77,7 +81,7 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i
SeeAlso []
***********************************************************************/
-Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
{
Saig_Bmc_t * p;
Aig_Obj_t * pObj;
@@ -86,10 +90,10 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl
p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
memset( p, 0, sizeof(Saig_Bmc_t) );
// set parameters
- p->nFramesMax = 1000000;
+ p->nFramesMax = nFramesMax;
+ p->nNodesMax = nNodesMax;
p->nConfMaxOne = nConfMaxOne;
p->nConfMaxAll = nConfMaxAll;
- p->nNodesMax = nNodesMax;
p->fVerbose = fVerbose;
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax(pAig);
@@ -103,15 +107,17 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl
Saig_ManForEachLo( pAig, pObj, i )
Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) );
// create SAT solver
+ p->nSatVars = 1;
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 2000 );
- p->nSatVars = 1;
Lit = toLit( p->nSatVars );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
// other data structures
p->vTargets = Vec_PtrAlloc( 0 );
p->vVisited = Vec_PtrAlloc( 0 );
+ p->iOutputFail = -1;
+ p->iFrameFail = -1;
return p;
}
@@ -174,15 +180,15 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
p1 = Saig_BmcObjChild1( p, pObj, i );
if ( p0 == Aig_Not(p1) )
- pRes = Aig_Not(pConst1);
+ pRes = Aig_ManConst0(p->pFrm);
else if ( Aig_Regular(p0) == pConst1 )
- pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1);
+ pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
else if ( Aig_Regular(p1) == pConst1 )
- pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1);
+ pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
else
pRes = AIG_VISITED;
- if ( pRes != pConst1 && pRes != Aig_Not(pConst1) )
+ if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
pRes = AIG_VISITED;
}
Saig_BmcObjSetFrame( p, pObj, i, pRes );
@@ -222,6 +228,7 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
}
+ assert( pRes != AIG_VISITED );
Saig_BmcObjSetFrame( p, pObj, i, pRes );
return pRes;
}
@@ -239,23 +246,30 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
***********************************************************************/
void Saig_BmcInterval( Saig_Bmc_t * p )
{
- Aig_Obj_t * pTarget, * pObj;
- int i, nNodes = Aig_ManNodeNum( p->pFrm );
+ Aig_Obj_t * pTarget;
+// Aig_Obj_t * pObj;
+// int i;
+ int nNodes = Aig_ManObjNum( p->pFrm );
Vec_PtrClear( p->vTargets );
- for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 )
+ for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
{
if ( p->iOutputLast == 0 )
{
- Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) );
- Saig_ManForEachPi( p->pAig, pObj, i )
- Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) );
+ Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
+// Saig_ManForEachPi( p->pAig, pObj, i )
+// Saig_BmcObjSetFrame( p, pObj, p->iFrameLast, Aig_ObjCreatePi(p->pFrm) );
}
for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
{
- if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax )
+ if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
return;
- Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
- pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+ Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
+ pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
+
+ /////////
+// if ( Aig_ObjIsConst1(Aig_Regular(pTarget)) )
+// continue;
+
Vec_PtrPush( p->vTargets, pTarget );
}
}
@@ -281,6 +295,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj
return pObj->pData = Aig_ObjCreatePi(pNew);
Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
+ assert( pObj->pData == NULL );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
@@ -300,13 +315,18 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i;
+ Aig_ManForEachObj( p->pFrm, pObj, i )
+ assert( pObj->pData == NULL );
+
pNew = Aig_ManStart( p->nNodesMax );
Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
Vec_PtrClear( p->vVisited );
Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
+// assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
+ assert( !Aig_IsComplement(pObjNew) );
Aig_ObjCreatePo( pNew, pObjNew );
}
return pNew;
@@ -329,12 +349,14 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
int i, Lits[2], VarNumOld, VarNumNew;
Vec_PtrForEachEntry( p->vVisited, pObj, i )
{
- pObjNew = pObj->pData;
+ // get the new variable of this node
+ pObjNew = pObj->pData;
pObj->pData = NULL;
- VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
+ VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
if ( VarNumNew == -1 )
continue;
- VarNumOld = Saig_BmcSatNum( p, pObj );
+ // get the old variable of this node
+ VarNumOld = Saig_BmcSatNum( p, pObj );
if ( VarNumOld == 0 )
{
Saig_BmcSetSatNum( p, pObj, VarNumNew );
@@ -369,11 +391,88 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
SeeAlso []
***********************************************************************/
+void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
+{
+ int k;
+ p->iOutputFail = p->iOutputLast;
+ p->iFrameFail = p->iFrameLast;
+ for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
+ {
+ if ( p->iOutputFail == 0 )
+ {
+ p->iOutputFail = Saig_ManPoNum(p->pAig);
+ p->iFrameFail--;
+ }
+ p->iOutputFail--;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves targets with the given resource limit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
+{
+ Ssw_Cex_t * pCex;
+ Aig_Obj_t * pObj, * pObjFrm;
+ int i, f, iVarNum;
+ // start the counter-example
+ pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
+ pCex->iFrame = p->iFrameFail;
+ pCex->iPo = p->iOutputFail;
+ // copy the bit data
+ for ( f = 0; f <= p->iFrameFail; f++ )
+ {
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjFrm = Saig_BmcObjFrame( p, pObj, f );
+ if ( pObjFrm == NULL )
+ continue;
+ iVarNum = Saig_BmcSatNum( p, pObjFrm );
+ if ( iVarNum == 0 )
+ continue;
+ if ( sat_solver_var_value( p->pSat, iVarNum ) )
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
+ }
+ }
+ // verify the counter example
+ if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
+ {
+ printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
+ Ssw_SmlFreeCounterExample( pCex );
+ pCex = NULL;
+ }
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves targets with the given resource limit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Saig_BmcSolveTargets( Saig_Bmc_t * p )
{
Aig_Obj_t * pObj;
int i, VarNum, Lit, RetValue;
assert( Vec_PtrSize(p->vTargets) > 0 );
+ if ( p->pSat->qtail != p->pSat->qhead )
+ {
+ RetValue = sat_solver_simplify(p->pSat);
+ assert( RetValue != 0 );
+ }
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
if ( p->pSat->stats.conflicts > p->nConfMaxAll )
@@ -386,6 +485,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
if ( RetValue == l_Undef ) // undecided
return l_Undef;
// generate counter-example
+ Saig_BmcDeriveFailed( p, i );
+ p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
return l_True;
}
return l_False;
@@ -393,6 +494,28 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( p->vTargets, pObj, i )
+ Aig_ObjCreatePo( p->pFrm, pObj );
+ Aig_ManPrintStats( p->pFrm );
+ Aig_ManCleanup( p->pFrm );
+ Aig_ManPrintStats( p->pFrm );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs BMC with the given parameters.]
Description []
@@ -402,17 +525,27 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
-void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
{
Saig_Bmc_t * p;
Aig_Man_t * pNew;
Cnf_Dat_t * pCnf;
- int RetValue, clk = clock();
- p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose );
- while ( 1 )
+ int Iter, RetValue, clk = clock(), clk2;
+ p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
+ if ( fVerbose )
+ {
+ printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
+ Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
+ Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+ printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
+ nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
+ }
+ for ( Iter = 0; ; Iter++ )
{
- // add new logic slice to frames
+ clk2 = clock();
+ // add new logic interval to frames
Saig_BmcInterval( p );
+// Saig_BmcAddTargetsAsPos( p );
if ( Vec_PtrSize(p->vTargets) == 0 )
break;
// convert logic slice into new AIG
@@ -427,20 +560,30 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nN
Aig_ManStop( pNew );
// solve the targets
RetValue = Saig_BmcSolveTargets( p );
+ if ( fVerbose )
+ {
+ printf( "%3d : F = %3d. O = %3d. And = %7d. Var = %7d. Conf = %7d. ",
+ Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );
+ PRT( "Time", clock() - clk2 );
+ }
if ( RetValue != l_False )
break;
}
if ( RetValue == l_True )
- printf( "BMC failed for output %d in frame %d. ", p->iOutputLast, p->iFramelast );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
+ p->iOutputFail, p->iFrameFail );
else // if ( RetValue == l_False || RetValue == l_Undef )
- printf( "BMC completed for %d timeframes. ", p->iFramelast );
+ printf( "No output was asserted in %d frames. ", p->iFrameLast );
PRT( "Time", clock() - clk );
- if ( p->iFramelast >= p->nFramesMax )
- printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
- else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
- printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
- else
- printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+ if ( RetValue != l_True )
+ {
+ if ( p->iFrameLast >= p->nFramesMax )
+ printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+ else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+ printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
+ else
+ printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+ }
Saig_BmcManStop( p );
}
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 165a08f2..61ea6ca0 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -108,13 +108,12 @@ Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
pObj->fMarkA = 0;
pObj->pData = Aig_ObjCreatePi( pAigNew );
}
- // add internal nodes of this frame
+ // add internal nodes
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs
- Aig_ManForEachPo( pAig, pObj, i )
- if ( !pObj->fMarkA )
- Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ Saig_ManForEachPo( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
// create LIs
Aig_ManForEachPo( pAig, pObj, i )
if ( pObj->fMarkA )
@@ -122,8 +121,8 @@ Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
pObj->fMarkA = 0;
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
}
- Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
+ Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 15:49:27 +0000