summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/module.make1
-rw-r--r--src/aig/ssw/ssw.h6
-rw-r--r--src/aig/ssw/sswAig.c50
-rw-r--r--src/aig/ssw/sswBmc.c350
-rw-r--r--src/aig/ssw/sswCnf.c124
-rw-r--r--src/aig/ssw/sswCore.c58
-rw-r--r--src/aig/ssw/sswInt.h62
-rw-r--r--src/aig/ssw/sswLcorr.c57
-rw-r--r--src/aig/ssw/sswMan.c59
-rw-r--r--src/aig/ssw/sswSat.c74
-rw-r--r--src/aig/ssw/sswSemi.c318
-rw-r--r--src/aig/ssw/sswSim.c39
-rw-r--r--src/aig/ssw/sswSweep.c183
-rw-r--r--src/aig/ssw/sswUnique.c155
14 files changed, 891 insertions, 645 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 625d72d1..915f7dd0 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -8,6 +8,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswPart.c \
src/aig/ssw/sswPairs.c \
src/aig/ssw/sswSat.c \
+ src/aig/ssw/sswSemi.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
src/aig/ssw/sswSweep.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 2785bca6..2d067a17 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -50,8 +50,8 @@ struct Ssw_Pars_t_
int nBTLimit; // conflict limit at a node
int nBTLimitGlobal;// conflict limit for multiple runs
int nMinDomSize; // min clock domain considered for optimization
+ int nItersStop; // stop after the given number of iterations
int fPolarFlip; // uses polarity adjustment
- int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints
@@ -88,13 +88,13 @@ struct Ssw_Cex_t_
/*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
+/*=== sswBmc.c ==========================================================*/
+extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
-/*=== sswLoc.c ==========================================================*/
-extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== sswMiter.c ===================================================*/
extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
/*=== sswPart.c ==========================================================*/
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 0d0fdbee..fda05941 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -30,6 +30,50 @@
/**Function*************************************************************
+ Synopsis [Starts the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
+{
+ Ssw_Frm_t * p;
+ p = ALLOC( Ssw_Frm_t, 1 );
+ memset( p, 0, sizeof(Ssw_Frm_t) );
+ p->pAig = pAig;
+ p->nObjs = Aig_ManObjNumMax( pAig );
+ p->nFrames = 0;
+ p->pFrames = NULL;
+ p->vAig2Frm = Vec_PtrAlloc( 0 );
+ Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_FrmStop( Ssw_Frm_t * p )
+{
+ if ( p->pFrames )
+ Aig_ManStop( p->pFrames );
+ Vec_PtrFree( p->vAig2Frm );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs speculative reduction for one node.]
Description []
@@ -164,7 +208,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
-
+
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// map constants and PIs
@@ -190,8 +234,8 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
// remove dangling nodes
Aig_ManCleanup( pFrames );
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
- printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
- p->nConstrTotal, p->nConstrReduced );
+// printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
+// p->nConstrTotal, p->nConstrReduced );
return pFrames;
}
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c
index e2d47440..93859c01 100644
--- a/src/aig/ssw/sswBmc.c
+++ b/src/aig/ssw/sswBmc.c
@@ -6,7 +6,7 @@
PackageName [Inductive prover with constraints.]
- Synopsis [Bounded model checker for equivalence clases.]
+ Synopsis [Bounded model checker using dynamic unrolling.]
Author [Alan Mishchenko]
@@ -24,32 +24,13 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct Ssw_Bmc_t_ Ssw_Bmc_t; // BMC manager
-
-struct Ssw_Bmc_t_
-{
- // parameters
- int nConfMaxStart; // the starting conflict limit
- int nConfMax; // the intermediate conflict limit
- int nFramesSweep; // the number of frames to sweep
- int fVerbose; // prints output statistics
- // equivalences considered
- Ssw_Man_t * pMan; // SAT sweeping manager
- Vec_Ptr_t * vTargets; // the nodes that are watched
- // storage for patterns
- int nPatternsAlloc; // the max number of interesting states
- int nPatterns; // the number of patterns
- Vec_Ptr_t * vPatterns; // storage for the interesting states
- Vec_Int_t * vHistory; // what state and how many steps
-};
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis []
+ Synopsis [Incrementally unroll the timeframes.]
Description []
@@ -58,60 +39,43 @@ struct Ssw_Bmc_t_
SeeAlso []
***********************************************************************/
-Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
+Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
{
- Ssw_Bmc_t * p;
- Aig_Obj_t * pObj;
- int i;
- // create interpolation manager
- p = ALLOC( Ssw_Bmc_t, 1 );
- memset( p, 0, sizeof(Ssw_Bmc_t) );
- p->nConfMaxStart = nConfMax;
- p->nConfMax = nConfMax;
- p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
- p->fVerbose = fVerbose;
- // equivalences considered
- p->pMan = pMan;
- p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
- Saig_ManForEachPo( p->pMan->pAig, pObj, i )
- Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
- // storage for patterns
- p->nPatternsAlloc = 512;
- p->nPatterns = 1;
- p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Aig_BitWordNum(p->nPatternsAlloc) );
- Vec_PtrCleanSimInfo( p->vPatterns, 0, Aig_BitWordNum(p->nPatternsAlloc) );
- p->vHistory = Vec_IntAlloc( 100 );
- Vec_IntPush( p->vHistory, 0 );
- // update arrays of the manager
- free( p->pMan->pNodeToFrames );
- Vec_IntFree( p->pMan->vSatVars );
- p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
- p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_BmcManStop( Ssw_Bmc_t * p )
-{
- Vec_PtrFree( p->vTargets );
- Vec_PtrFree( p->vPatterns );
- Vec_IntFree( p->vHistory );
- free( p );
+ Aig_Obj_t * pRes, * pRes0, * pRes1;
+ if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) )
+ return pRes;
+ if ( Aig_ObjIsConst1(pObj) )
+ pRes = Aig_ManConst1( pFrm->pFrames );
+ else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
+ pRes = Aig_ObjCreatePi( pFrm->pFrames );
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
+ pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
+ }
+ else if ( Saig_ObjIsLo(pFrm->pAig, pObj) )
+ {
+ if ( f == 0 )
+ pRes = Aig_ManConst0( pFrm->pFrames );
+ else
+ pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
+ Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f );
+ pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f );
+ pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f );
+ pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 );
+ }
+ Ssw_ObjSetFrame_( pFrm, pObj, f, pRes );
+ return pRes;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Derives counter-example.]
Description []
@@ -120,46 +84,34 @@ void Ssw_BmcManStop( Ssw_Bmc_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_BmcCheckTargets( Ssw_Bmc_t * p )
+Ssw_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame )
{
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrForEachEntry( p->vTargets, pObj, i )
- if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
- return 1;
- return 0;
+ Ssw_Cex_t * pCex;
+ Aig_Obj_t * pObj, * pObjFrames;
+ int f, i, nShift;
+ assert( Saig_ManRegNum(pFrm->pAig) > 0 );
+ // allocate the counter example
+ pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
+ pCex->iPo = iPo;
+ pCex->iFrame = iFrame;
+ // create data-bits
+ nShift = Saig_ManRegNum(pFrm->pAig);
+ for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) )
+ Saig_ManForEachPi( pFrm->pAig, pObj, i )
+ {
+ pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f);
+ if ( pObjFrames == NULL )
+ continue;
+ if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) )
+ Aig_InfoSetBit( pCex->pData, nShift + i );
+ }
+ return pCex;
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p )
-{
- unsigned * pInfo;
- Aig_Obj_t * pObj;
- int i;
- if ( p->nPatterns >= p->nPatternsAlloc )
- return;
- Saig_ManForEachLo( p->pMan->pAig, pObj, i )
- {
- pInfo = Vec_PtrEntry( p->vPatterns, i );
- if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
- Aig_InfoSetBit( pInfo, p->nPatterns );
- }
- p->nPatterns++;
-}
/**Function*************************************************************
- Synopsis [Performs fraiging for the internal nodes.]
+ Synopsis [Performs BMC for the given AIG.]
Description []
@@ -168,143 +120,95 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_ManFilterBmc( Ssw_Bmc_t * pBmc, int iPat, int fCheckTargets )
+int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame )
{
- Ssw_Man_t * p = pBmc->pMan;
- Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
- unsigned * pInfo;
- int i, f, clk, RetValue, fFirst = 0;
-clk = clock();
-
- // start initialized timeframes
- p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
- Saig_ManForEachLo( p->pAig, pObj, i )
+ Ssw_Frm_t * pFrm;
+ Ssw_Sat_t * pSat;
+ Aig_Obj_t * pObj, * pObjFrame;
+ int status, clkPart, Lit, i, f, RetValue;
+
+ // start managers
+ assert( Saig_ManRegNum(pAig) > 0 );
+ Aig_ManSetPioNumbers( pAig );
+ pSat = Ssw_SatStart( 0 );
+ pFrm = Ssw_FrmStart( pAig );
+ pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
+ // report statistics
+ if ( fVerbose )
{
- pInfo = Vec_PtrEntry( pBmc->vPatterns, i );
- pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) );
- Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
+ 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) );
+ fflush( stdout );
}
-
- // sweep internal nodes
- Ssw_ManStartSolver( p );
- RetValue = pBmc->nFramesSweep;
- for ( f = 0; f < pBmc->nFramesSweep; f++ )
+ // perform dynamic unrolling
+ RetValue = -1;
+ for ( f = 0; f < nFramesMax; f++ )
{
- // map constants and PIs
- Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
- Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
- // sweep internal nodes
- Aig_ManForEachNode( p->pAig, pObj, i )
+ clkPart = clock();
+ Saig_ManForEachPo( pAig, pObj, i )
{
- pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- if ( Ssw_ManSweepNode( p, pObj, f, 1 ) )
+ // unroll the circuit for this output
+ Ssw_BmcUnroll_rec( pFrm, pObj, f );
+ pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f );
+ Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) );
+ status = sat_solver_simplify(pSat->pSat);
+ assert( status );
+ // solve
+ Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
+ if ( fVerbose )
+ {
+ printf( "Solving output %2d of frame %3d ... \r",
+ i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+ }
+ status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( status == l_False )
{
- Ssw_ManFilterBmcSavePattern( pBmc );
- if ( fFirst == 0 )
+/*
+ Lit = lit_neg( Lit );
+ RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 );
+ assert( RetValue );
+ if ( pSat->pSat->qtail != pSat->pSat->qhead )
{
- fFirst = 1;
- pBmc->nConfMax *= 10;
- }
+ RetValue = sat_solver_simplify(pSat->pSat);
+ assert( RetValue );
+ }
+*/
+ RetValue = 1;
+ continue;
}
- if ( f > 0 && p->pSat->stats.conflicts >= pBmc->nConfMax )
+ else if ( status == l_True )
{
+ pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f );
+ if ( piFrame )
+ *piFrame = f;
+ RetValue = 0;
+ break;
+ }
+ else
+ {
+ if ( piFrame )
+ *piFrame = f;
RetValue = -1;
break;
}
}
- // quit if this is the last timeframe
- if ( p->pSat->stats.conflicts >= pBmc->nConfMax )
- {
- RetValue += f + 1;
- break;
- }
- if ( fCheckTargets && Ssw_BmcCheckTargets( pBmc ) )
- break;
- // transfer latch input to the latch outputs
- // build logic cones for register outputs
- Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- {
- pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
- Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
- }
-//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
- }
- if ( fFirst )
- pBmc->nConfMax /= 10;
-
- // cleanup
- Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if one of the targets has failed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
-{
- Ssw_Bmc_t * p;
- int RetValue, Frames, Iter, clk = clock();
- p = Ssw_BmcManStart( pMan, nConfMax, fVerbose );
- if ( fCheckTargets && Ssw_BmcCheckTargets( p ) )
- {
- assert( 0 );
- Ssw_BmcManStop( p );
- return 1;
- }
- if ( fVerbose )
- {
- printf( "AIG : Const = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
- Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
- Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
- }
- RetValue = 0;
- for ( Iter = 0; Iter < p->nPatterns; Iter++ )
- {
-clk = clock();
- Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
- Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
- Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pSat->stats.conflicts, p->nPatterns,
- p->pMan->nSatFailsReal? "f" : " " );
- PRT( "T", clock() - clk );
- }
- Ssw_ManCleanup( p->pMan );
- if ( fCheckTargets && Ssw_BmcCheckTargets( p ) )
- {
- printf( "Target is hit!!!\n" );
- RetValue = 1;
+ printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
+ printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ",
+ (double)pSat->pSat->stats.conflicts,
+ pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
+ PRT( "T", clock() - clkPart );
+ clkPart = clock();
+ fflush( stdout );
}
- if ( p->nPatterns >= p->nPatternsAlloc )
+ if ( RetValue != 1 )
break;
}
- Ssw_BmcManStop( p );
-
- pMan->nStrangers = 0;
- pMan->nSatCalls = 0;
- pMan->nSatProof = 0;
- pMan->nSatFailsReal = 0;
- pMan->nSatFailsTotal = 0;
- pMan->nSatCallsUnsat = 0;
- pMan->nSatCallsSat = 0;
- pMan->timeSimSat = 0;
- pMan->timeSat = 0;
- pMan->timeSatSat = 0;
- pMan->timeSatUnsat = 0;
- pMan->timeSatUndec = 0;
+
+ Ssw_SatStop( pSat );
+ Ssw_FrmStop( pFrm );
return RetValue;
}
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index e4b8f9f6..d068bb78 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -30,6 +30,63 @@
/**Function*************************************************************
+ Synopsis [Starts the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
+{
+ Ssw_Sat_t * p;
+ int Lit;
+ p = ALLOC( Ssw_Sat_t, 1 );
+ memset( p, 0, sizeof(Ssw_Sat_t) );
+ p->pAig = NULL;
+ p->fPolarFlip = fPolarFlip;
+ p->vSatVars = Vec_IntStart( 10000 );
+ p->vFanins = Vec_PtrAlloc( 100 );
+ p->vUsedPis = Vec_PtrAlloc( 100 );
+ p->pSat = sat_solver_new();
+ sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is not used
+ // var 1 is reserved for const1 node - add the clause
+ p->nSatVars = 1;
+ Lit = toLit( p->nSatVars );
+ if ( fPolarFlip )
+ Lit = lit_neg( Lit );
+ sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+// Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
+ Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stop the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SatStop( Ssw_Sat_t * p )
+{
+ if ( p->pSat )
+ sat_solver_delete( p->pSat );
+ Vec_IntFree( p->vSatVars );
+ Vec_PtrFree( p->vFanins );
+ Vec_PtrFree( p->vUsedPis );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis [Addes clauses to the solver.]
Description []
@@ -39,7 +96,7 @@
SeeAlso []
***********************************************************************/
-void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
+void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
{
Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
@@ -68,7 +125,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -79,7 +136,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -90,7 +147,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -101,7 +158,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -126,7 +183,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -137,7 +194,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -158,7 +215,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
Aig_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
@@ -173,7 +230,7 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -185,13 +242,13 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Vec_PtrForEachEntry( vSuper, pFanin, i )
{
pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
}
}
pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
}
@@ -221,6 +278,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
Vec_PtrPushUnique( vSuper, pObj );
return;
}
+// pObj->fMarkA = 1;
// go through the branches
Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
@@ -256,7 +314,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
SeeAlso []
***********************************************************************/
-void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
assert( !Aig_IsComplement(pObj) );
if ( Ssw_ObjSatNum(p,pObj) )
@@ -264,12 +322,10 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
assert( Ssw_ObjSatNum(p,pObj) == 0 );
if ( Aig_ObjIsConst1(pObj) )
return;
- if ( p->pPars->fLatchCorrOpt )
- {
- Vec_PtrPush( p->vUsedNodes, pObj );
- if ( Aig_ObjIsPi(pObj) )
- Vec_PtrPush( p->vUsedPis, pObj );
- }
+// pObj->fMarkA = 1;
+ // save PIs (used by register correspondence)
+ if ( Aig_ObjIsPi(pObj) )
+ Vec_PtrPush( p->vUsedPis, pObj );
Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
if ( Aig_ObjIsNode(pObj) )
@@ -287,7 +343,7 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
SeeAlso []
***********************************************************************/
-void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
+void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
{
Vec_Ptr_t * vFrontier;
Aig_Obj_t * pNode, * pFanin;
@@ -327,6 +383,36 @@ void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
}
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
+{
+ int Value0, Value1, nVarNum;
+ assert( !Aig_IsComplement(pObj) );
+ nVarNum = Ssw_ObjSatNum( p, pObj );
+ if ( nVarNum > 0 )
+ return sat_solver_var_value( p->pSat, nVarNum );
+// if ( pObj->fMarkA == 1 )
+// return 0;
+ if ( Aig_ObjIsPi(pObj) )
+ return 0;
+ assert( Aig_ObjIsNode(pObj) );
+ Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
+ Value0 ^= Aig_ObjFaninC0(pObj);
+ Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
+ Value1 ^= Aig_ObjFaninC1(pObj);
+ return Value0 & Value1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 2af9e900..39f4c736 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,13 +45,13 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nPartSize = 0; // size of the partition
p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth
- p->nFramesAddSim = 0; // additional frames to simulate
+ p->nFramesAddSim = 2; // additional frames to simulate
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->nBTLimitGlobal = 5000000; // conflict limit for all runs
p->nMinDomSize = 100; // min clock domain considered for optimization
+ p->nItersStop = 0; // stop after the given number of iterations
p->fPolarFlip = 0; // uses polarity adjustment
- p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering
p->fUniqueness = 0; // enable uniqueness constraints
@@ -111,7 +111,12 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
}
if ( !p->pPars->fLatchCorr )
{
+ p->pMSat = Ssw_SatStart( 0 );
Ssw_ManSweepBmc( p );
+ if ( p->pPars->nFramesK > 1 && p->pPars->fUniqueness )
+ Ssw_UniqueRegisterPairInfo( p );
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = NULL;
Ssw_ManCleanup( p );
}
if ( p->pPars->fVerbose )
@@ -120,20 +125,23 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// apply semi-formal filtering
+/*
if ( p->pPars->fSemiFormal )
{
Aig_Man_t * pSRed;
- Ssw_FilterUsingBmc( p, 0, 2000, p->pPars->fVerbose );
-// Ssw_FilterUsingBmc( p, 1, 100000, p->pPars->fVerbose );
+ Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
+// Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
pSRed = Ssw_SpeculativeReduction( p );
Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
Aig_ManStop( pSRed );
}
+*/
// refine classes using induction
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
for ( nIter = 0; ; nIter++ )
{
clk = clock();
+ p->pMSat = Ssw_SatStart( 0 );
if ( p->pPars->fLatchCorrOpt )
{
RetValue = Ssw_ManSweepLatch( p );
@@ -153,34 +161,32 @@ clk = clock();
else
{
RetValue = Ssw_ManSweep( p );
- p->pPars->nConflicts += p->pSat->stats.conflicts;
+ p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
- if ( p->pPars->fSkipCheck )
- printf( "Use = %5d. Skip = %5d. ",
- p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk );
}
}
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = NULL;
Ssw_ManCleanup( p );
- if ( !RetValue )
+ if ( !RetValue )
break;
-/*
+
+ if ( p->pPars->nItersStop && p->pPars->nItersStop == nIter )
{
- static int Flag = 0;
- if ( Flag++ == 4 && nIter == 4 )
- {
- Aig_Man_t * pSRed;
- pSRed = Ssw_SpeculativeReduction( p );
- Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
- Aig_ManStop( pSRed );
- }
+ Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
+ Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+ Aig_ManStop( pSRed );
+ printf( "Iterative refinement is stopped after iteration %d.\n", nIter );
+ printf( "The network is reduced using candidate equivalences.\n" );
+ printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
+ printf( "If the miter is SAT, the reduced result is incorrect.\n" );
+ break;
}
-*/
-
}
p->pPars->nIters = nIter + 1;
p->timeTotal = clock() - clkTotal;
@@ -224,6 +230,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return Aig_ManDupOrdered(pAig);
}
// check and update parameters
+ if ( pPars->fUniqueness )
+ {
+ pPars->nFramesAddSim = 0;
+ if ( pPars->nFramesK != 2 )
+ printf( "Setting K = 2 for uniqueness constaints to work.\n" );
+ pPars->nFramesK = 2;
+ }
if ( pPars->fLatchCorrOpt )
{
pPars->fLatchCorr = 1;
@@ -232,8 +245,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
else
{
assert( pPars->nFramesK > 0 );
- if ( pPars->nFramesK > 1 )
- pPars->fSkipCheck = 0;
// perform partitioning
if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
@@ -259,6 +270,9 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
}
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
+ if ( pPars->fUniqueness )
+ printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n",
+ p->nUniquesAdded, p->nUniquesUseful );
// cleanup
Ssw_ManStop( p );
return pAigNew;
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 636bd139..0a3f7e21 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -42,6 +42,8 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
+typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
+typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
@@ -57,17 +59,10 @@ struct Ssw_Man_t_
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
- int nRefUse; // the number of equivalences used
- int nRefSkip; // the number of equivalences skipped
- // SAT solving
- sat_solver * pSat; // recyclable SAT solver
- int nSatVars; // the counter of SAT variables
- Vec_Int_t * vSatVars; // mapping of each node into its SAT var
- int nSatVarsTotal; // the total number of SAT vars created
- Vec_Ptr_t * vFanins; // fanins of the CNF node
+ // SAT solving
+ Ssw_Sat_t * pMSatBmc; // SAT manager for base case
+ Ssw_Sat_t * pMSat; // SAT manager for inductive case
// SAT solving (latch corr only)
- Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables
- Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs
int nPatterns; // the number of patterns saved
int nSimRounds; // the number of simulation rounds performed
@@ -81,7 +76,10 @@ struct Ssw_Man_t_
// uniqueness
Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
int iOutputLit; // the output literal of the uniqueness constaint
+ Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff
int nUniques; // the number of uniqueness constaints used
+ int nUniquesAdded; // useful uniqueness constraints
+ int nUniquesUseful; // useful uniqueness constraints
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
@@ -118,12 +116,35 @@ struct Ssw_Man_t_
int timeTotal; // total runtime
};
+// internal SAT manager
+struct Ssw_Sat_t_
+{
+ Aig_Man_t * pAig; // the AIG manager
+ int fPolarFlip; // flips polarity
+ sat_solver * pSat; // recyclable SAT solver
+ int nSatVars; // the counter of SAT variables
+ Vec_Int_t * vSatVars; // mapping of each node into its SAT var
+ int nSatVarsTotal; // the total number of SAT vars created
+ Vec_Ptr_t * vFanins; // fanins of the CNF node
+ Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
+};
+
+// internal frames manager
+struct Ssw_Frm_t_
+{
+ Aig_Man_t * pAig; // user-given AIG
+ int nObjs; // offset in terms of AIG nodes
+ int nFrames; // the number of frames in current unrolling
+ Aig_Man_t * pFrames; // unrolled AIG
+ Vec_Ptr_t * vAig2Frm; // mapping of AIG nodes into frame nodes
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, pObj->Id ); }
-static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntWriteEntryFill( p->vSatVars, pObj->Id, Num ); }
+static inline int Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vSatVars, pObj->Id ); }
+static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num); }
static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
@@ -141,15 +162,22 @@ static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int
static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
+static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); }
+static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); }
+
+static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswAig.c ===================================================*/
+extern Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig );
+extern void Ssw_FrmStop( Ssw_Frm_t * p );
extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p );
/*=== sswBmc.c ===================================================*/
-extern int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswClass.c =================================================*/
extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
@@ -177,7 +205,10 @@ extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
/*=== sswCnf.c ===================================================*/
-extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
+extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip );
+extern void Ssw_SatStop( Ssw_Sat_t * p );
+extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
+extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
@@ -190,6 +221,8 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p );
/*=== sswSat.c ===================================================*/
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+/*=== sswSemi.c ===================================================*/
+extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswSim.c ===================================================*/
extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
@@ -214,6 +247,7 @@ extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, i
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
+extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index cde9b0c9..d374c5f6 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -31,48 +31,6 @@
/**Function*************************************************************
- Synopsis [Recycles the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
-{
- int Lit;
- if ( p->pSat )
- {
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
- Ssw_ObjSetSatNum( p, pObj, 0 );
- Vec_PtrClear( p->vUsedNodes );
- Vec_PtrClear( p->vUsedPis );
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
- sat_solver_delete( p->pSat );
- }
- p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 1000 );
- // var 0 is not used
- // var 1 is reserved for const1 node - add the clause
- p->nSatVars = 1;
-// p->nSatVars = 0;
- Lit = toLit( p->nSatVars );
- if ( p->pPars->fPolarFlip )
- Lit = lit_neg( Lit );
- sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
-
- p->nRecycles++;
- p->nRecycleCalls = 0;
-}
-
-
-/**Function*************************************************************
-
Synopsis [Tranfers simulation information from FRAIG to AIG.]
Description []
@@ -148,11 +106,11 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Aig_Obj_t * pObj;
unsigned * pInfo;
int i, nVarNum, Value;
- Vec_PtrForEachEntry( p->vUsedPis, pObj, i )
+ Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i )
{
- nVarNum = Ssw_ObjSatNum( p, pObj );
+ nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
assert( nVarNum > 0 );
- Value = sat_solver_var_value( p->pSat, nVarNum );
+ Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
if ( Value == 0 )
continue;
pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
@@ -339,9 +297,14 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
Ssw_ManSweepResimulate( p );
// attempt recycling the SAT solver
if ( p->pPars->nSatVarMax &&
- p->nSatVars > p->pPars->nSatVarMax &&
+ p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
- Ssw_ManSatSolverRecycle( p );
+ {
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = Ssw_SatStart( 0 );
+ p->nRecycles++;
+ p->nRecycleCalls = 0;
+ }
}
// resimulate
if ( p->nPatterns > 0 )
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index d4a26f64..1b29037c 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -53,12 +53,6 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1;
p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
- // SAT solving
- p->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
- p->vFanins = Vec_PtrAlloc( 100 );
- // SAT solving (latch corr only)
- p->vUsedNodes = Vec_PtrAlloc( 1000 );
- p->vUsedPis = Vec_PtrAlloc( 1000 );
p->vCommon = Vec_PtrAlloc( 100 );
p->iOutputLit = -1;
// allocate storage for sim pattern
@@ -106,11 +100,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
- p->nSatVarsTotal/p->pPars->nIters );
+ 0/p->pPars->nIters );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n",
- p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds );
+ 0, p->nConeMax, p->nRecycles, p->nSimRounds );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
@@ -141,23 +135,14 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p )
{
+ assert( p->pMSat == NULL );
if ( p->pFrames )
{
+ Aig_ManCleanMarkA( p->pFrames );
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
- if ( p->pSat )
- {
- int i;
-// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
- p->nSatVarsTotal += p->pSat->size;
- sat_solver_delete( p->pSat );
- p->pSat = NULL;
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
- for ( i = 0; i < Vec_IntSize(p->vSatVars); i++ )
- p->vSatVars->pArray[i] = 0;
- }
if ( p->vSimInfo )
{
Vec_PtrFree( p->vSimInfo );
@@ -188,46 +173,14 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_ClassesStop( p->ppClasses );
if ( p->pSml )
Ssw_SmlStop( p->pSml );
- Vec_PtrFree( p->vFanins );
- Vec_PtrFree( p->vUsedNodes );
- Vec_PtrFree( p->vUsedPis );
- Vec_IntFree( p->vSatVars );
+ if ( p->vDiffPairs )
+ Vec_IntFree( p->vDiffPairs );
Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames );
FREE( p->pPatWords );
free( p );
}
-/**Function*************************************************************
-
- Synopsis [Starts the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManStartSolver( Ssw_Man_t * p )
-{
- int Lit;
- assert( p->pSat == NULL );
- p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 1000 );
- // var 0 is not used
- // var 1 is reserved for const1 node - add the clause
- p->nSatVars = 1;
- Lit = toLit( p->nSatVars );
- if ( p->pPars->fPolarFlip )
- Lit = lit_neg( Lit );
- sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
-
- Vec_PtrClear( p->vUsedNodes );
- Vec_PtrClear( p->vUsedPis );
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index af3bf80e..fc902560 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -50,18 +50,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pNew) );
assert( pOld != pNew );
- if ( p->pSat == NULL )
- Ssw_ManStartSolver( p );
+// if ( p->pSat == NULL )
+// Ssw_ManStartSolver( p );
+ assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them
- Ssw_CnfNodeAddToSolver( p, pOld );
- Ssw_CnfNodeAddToSolver( p, pNew );
+ Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
+ Ssw_CnfNodeAddToSolver( p->pMSat, pNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
nLits = 2;
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
@@ -71,14 +72,14 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
- if ( p->pSat->qtail != p->pSat->qhead )
+ if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{
- RetValue = sat_solver_simplify(p->pSat);
+ RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 );
}
clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
+ RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -88,8 +89,15 @@ p->timeSatUnsat += clock() - clk;
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue );
+/*
+ if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
+ {
+ RetValue = sat_solver_simplify(p->pMSat->pSat);
+ assert( RetValue != 0 );
+ }
+*/
}
p->nSatCallsUnsat++;
}
@@ -116,8 +124,8 @@ p->timeSatUndec += clock() - clk;
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
nLits = 2;
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
@@ -126,14 +134,14 @@ p->timeSatUndec += clock() - clk;
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
- if ( p->pSat->qtail != p->pSat->qhead )
+ if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{
- RetValue = sat_solver_simplify(p->pSat);
+ RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 );
}
clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
+ RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
@@ -143,8 +151,15 @@ p->timeSatUnsat += clock() - clk;
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue );
+/*
+ if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
+ {
+ RetValue = sat_solver_simplify(p->pMSat->pSat);
+ assert( RetValue != 0 );
+ }
+*/
}
p->nSatCallsUnsat++;
}
@@ -183,6 +198,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// sanity checks
assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
+ assert( Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
// move constant to the old node
if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
@@ -200,13 +216,13 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
pNew = Aig_Not(pNew);
}
- // start the solver
- if ( p->pSat == NULL )
- Ssw_ManStartSolver( p );
+// if ( p->pSat == NULL )
+// Ssw_ManStartSolver( p );
+ assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them
- Ssw_CnfNodeAddToSolver( p, pOld );
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );
// transform the new node
fComplNew = Aig_IsComplement( pNew );
@@ -216,12 +232,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
if ( pOld == Aig_ManConst1(p->pFrames) )
{
// add constaint A = 1 ----> A
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
}
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
assert( RetValue );
}
else
@@ -229,8 +245,8 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// add constaint A = B ----> (A v !B)(!A v B)
// (A v !B)
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -238,12 +254,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue );
// (!A v B)
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -251,7 +267,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue );
}
return 1;
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
new file mode 100644
index 00000000..b445c2c4
--- /dev/null
+++ b/src/aig/ssw/sswSemi.c
@@ -0,0 +1,318 @@
+/**CFile****************************************************************
+
+ FileName [sswSemi.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Semiformal for equivalence clases.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager
+
+struct Ssw_Sem_t_
+{
+ // parameters
+ int nConfMaxStart; // the starting conflict limit
+ int nConfMax; // the intermediate conflict limit
+ int nFramesSweep; // the number of frames to sweep
+ int fVerbose; // prints output statistics
+ // equivalences considered
+ Ssw_Man_t * pMan; // SAT sweeping manager
+ Vec_Ptr_t * vTargets; // the nodes that are watched
+ // storage for patterns
+ int nPatternsAlloc; // the max number of interesting states
+ int nPatterns; // the number of patterns
+ Vec_Ptr_t * vPatterns; // storage for the interesting states
+ Vec_Int_t * vHistory; // what state and how many steps
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
+{
+ Ssw_Sem_t * p;
+ Aig_Obj_t * pObj;
+ int i;
+ // create interpolation manager
+ p = ALLOC( Ssw_Sem_t, 1 );
+ memset( p, 0, sizeof(Ssw_Sem_t) );
+ p->nConfMaxStart = nConfMax;
+ p->nConfMax = nConfMax;
+ p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
+ p->fVerbose = fVerbose;
+ // equivalences considered
+ p->pMan = pMan;
+ p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
+ Saig_ManForEachPo( p->pMan->pAig, pObj, i )
+ Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
+ // storage for patterns
+ p->nPatternsAlloc = 512;
+ p->nPatterns = 1;
+ p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Aig_BitWordNum(p->nPatternsAlloc) );
+ Vec_PtrCleanSimInfo( p->vPatterns, 0, Aig_BitWordNum(p->nPatternsAlloc) );
+ p->vHistory = Vec_IntAlloc( 100 );
+ Vec_IntPush( p->vHistory, 0 );
+ // update arrays of the manager
+ assert( 0 );
+/*
+ free( p->pMan->pNodeToFrames );
+ Vec_IntFree( p->pMan->vSatVars );
+ p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
+ p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
+*/
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SemManStop( Ssw_Sem_t * p )
+{
+ Vec_PtrFree( p->vTargets );
+ Vec_PtrFree( p->vPatterns );
+ Vec_IntFree( p->vHistory );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SemCheckTargets( Ssw_Sem_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( p->vTargets, pObj, i )
+ if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
+{
+ unsigned * pInfo;
+ Aig_Obj_t * pObj;
+ int i;
+ if ( p->nPatterns >= p->nPatternsAlloc )
+ return;
+ Saig_ManForEachLo( p->pMan->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( p->vPatterns, i );
+ if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
+ Aig_InfoSetBit( pInfo, p->nPatterns );
+ }
+ p->nPatterns++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
+{
+ Ssw_Man_t * p = pBmc->pMan;
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
+ unsigned * pInfo;
+ int i, f, clk, RetValue, fFirst = 0;
+clk = clock();
+
+ // start initialized timeframes
+ p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ {
+ pInfo = Vec_PtrEntry( pBmc->vPatterns, i );
+ pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) );
+ Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
+ }
+
+ // sweep internal nodes
+ RetValue = pBmc->nFramesSweep;
+ for ( f = 0; f < pBmc->nFramesSweep; f++ )
+ {
+ // map constants and PIs
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ // sweep internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ if ( Ssw_ManSweepNode( p, pObj, f, 1 ) )
+ {
+ Ssw_ManFilterBmcSavePattern( pBmc );
+ if ( fFirst == 0 )
+ {
+ fFirst = 1;
+ pBmc->nConfMax *= 10;
+ }
+ }
+ if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
+ {
+ RetValue = -1;
+ break;
+ }
+ }
+ // quit if this is the last timeframe
+ if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
+ {
+ RetValue += f + 1;
+ break;
+ }
+ if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
+ break;
+ // transfer latch input to the latch outputs
+ // build logic cones for register outputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
+ Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
+ }
+//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
+ }
+ if ( fFirst )
+ pBmc->nConfMax /= 10;
+
+ // cleanup
+ Ssw_ClassesCheck( p->ppClasses );
+p->timeBmc += clock() - clk;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if one of the targets has failed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
+{
+ Ssw_Sem_t * p;
+ int RetValue, Frames, Iter, clk = clock();
+ p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
+ if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
+ {
+ assert( 0 );
+ Ssw_SemManStop( p );
+ return 1;
+ }
+ if ( fVerbose )
+ {
+ printf( "AIG : Const = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
+ Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
+ }
+ RetValue = 0;
+ for ( Iter = 0; Iter < p->nPatterns; Iter++ )
+ {
+clk = clock();
+ pMan->pMSat = Ssw_SatStart( 0 );
+ Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
+ if ( fVerbose )
+ {
+ printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
+ Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
+ p->pMan->nSatFailsReal? "f" : " " );
+ PRT( "T", clock() - clk );
+ }
+ Ssw_ManCleanup( p->pMan );
+ if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
+ {
+ printf( "Target is hit!!!\n" );
+ RetValue = 1;
+ }
+ if ( p->nPatterns >= p->nPatternsAlloc )
+ break;
+ }
+ Ssw_SemManStop( p );
+
+ pMan->nStrangers = 0;
+ pMan->nSatCalls = 0;
+ pMan->nSatProof = 0;
+ pMan->nSatFailsReal = 0;
+ pMan->nSatFailsTotal = 0;
+ pMan->nSatCallsUnsat = 0;
+ pMan->nSatCallsSat = 0;
+ pMan->timeSimSat = 0;
+ pMan->timeSat = 0;
+ pMan->timeSatSat = 0;
+ pMan->timeSatUnsat = 0;
+ pMan->timeSatUndec = 0;
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index ba8ad247..b80c3710 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -271,45 +271,6 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ );
}
-/**Function*************************************************************
-
- Synopsis [Copy pattern from the solver into the internal storage.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_SmlSavePattern( Ssw_Man_t * p )
-{
- Aig_Obj_t * pObj;
- int i;
- memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Aig_ManForEachPi( p->pFrames, pObj, i )
- if ( p->pSat->model.ptr[Ssw_ObjSatNum(p, pObj)] == l_True )
- Aig_InfoSetBit( p->pPatWords, i );
-/*
- if ( p->vCex )
- {
- Vec_IntClear( p->vCex );
- for ( i = 0; i < Saig_ManPiNum(p->pAig); i++ )
- Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
- for ( i = Saig_ManPiNum(p->pFrames); i < Aig_ManPiNum(p->pFrames); i++ )
- Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
- }
-*/
-
-/*
- printf( "Pattern: " );
- Aig_ManForEachPi( p->pFrames, pObj, i )
- printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
- printf( "\n" );
-*/
-}
-
-
/**Function*************************************************************
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index b971a13a..36e8bab3 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -31,53 +31,6 @@
/**Function*************************************************************
- Synopsis [Mark nodes affected by sweep in the previous iteration.]
-
- Description [Assumes that affected nodes are in p->ppClasses->vRefined.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
-{
- Vec_Ptr_t * vRefined, * vSupp;
- Aig_Obj_t * pObj, * pObjLo, * pObjLi;
- int i, k;
- vRefined = Ssw_ClassesGetRefined( p->ppClasses );
- if ( Vec_PtrSize(vRefined) == 0 )
- {
- Aig_ManForEachObj( p->pAig, pObj, i )
- pObj->fMarkA = 1;
- return;
- }
- // mark the nodes to be refined
- Aig_ManCleanMarkA( p->pAig );
- Vec_PtrForEachEntry( vRefined, pObj, i )
- {
- if ( Aig_ObjIsPi(pObj) )
- {
- pObj->fMarkA = 1;
- continue;
- }
- assert( Aig_ObjIsNode(pObj) );
- vSupp = Aig_Support( p->pAig, pObj );
- Vec_PtrForEachEntry( vSupp, pObjLo, k )
- pObjLo->fMarkA = 1;
- Vec_PtrFree( vSupp );
- }
- // mark refinement
- Aig_ManForEachNode( p->pAig, pObj, i )
- pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
- Saig_ManForEachLi( p->pAig, pObj, i )
- pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA;
- Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- pObjLo->fMarkA |= pObjLi->fMarkA;
-}
-
-/**Function*************************************************************
-
Synopsis [Retrives value of the PI in the original AIG.]
Description []
@@ -89,12 +42,22 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
***********************************************************************/
int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
+ int fUseNoBoundary = 0;
Aig_Obj_t * pObjFraig;
- int nVarNum, Value;
+ int Value;
// assert( Aig_ObjIsPi(pObj) );
pObjFraig = Ssw_ObjFrame( p, pObj, f );
- nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
- Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+ if ( fUseNoBoundary )
+ {
+ Value = Ssw_CnfGetNodeValue( p->pMSat, Aig_Regular(pObjFraig) );
+ Value ^= Aig_IsComplement(pObjFraig);
+ }
+ else
+ {
+ int nVarNum = Ssw_ObjSatNum( p->pMSat, Aig_Regular(pObjFraig) );
+ Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pMSat->pSat, nVarNum ));
+ }
+
// Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
if ( p->pPars->fPolarFlip )
@@ -181,15 +144,8 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return 0;
- // count the number of skipped calls
- if ( !pObj->fMarkA && !pObjRepr->fMarkA )
- p->nRefSkip++;
- else
- p->nRefUse++;
// call equivalence checking
- if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
- RetValue = 1;
- else if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
+ if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
else
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
@@ -204,18 +160,13 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
return 1;
}
- // check if skipping calls works correctly
- if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
- {
- assert( 0 );
- printf( "\nSsw_ManSweepNode(): Error!\n" );
- }
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 &&
Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
{
+/*
if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
{
int RetValue;
@@ -224,12 +175,39 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
p->iOutputLit = -1;
return RetValue;
}
+*/
+ if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
+ {
+ int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+ p->iOutputLit = -1;
+ p->nUniques++;
+ p->nUniquesAdded++;
+ if ( RetValue2 == 0 )
+ {
+ int x;
+// printf( "Second time:\n" );
+ x = Ssw_ManUniqueOne( p, pObjRepr, pObj );
+ Ssw_SmlSavePatternAig( p, f );
+ Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
+ if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
+ printf( "Ssw_ManSweepNode(): Refinement did not happen!!!.\n" );
+ return 1;
+ }
+ else
+ p->nUniquesUseful++;
+// printf( "Counter-example prevented!!!\n" );
+ return 0;
+ }
}
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
Ssw_ManResimulateBit( p, pObj, pObjRepr );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+ if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
+ {
+ printf( "Ssw_ManSweepNode(): Failed to refine representative.\n" );
+ }
return 1;
}
@@ -260,7 +238,7 @@ clk = clock();
p->fRefined = 0;
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
- Ssw_ManStartSolver( p );
+// Ssw_ManStartSolver( p );
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
@@ -285,7 +263,7 @@ clk = clock();
{
pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
}
}
if ( p->pPars->fVerbose )
@@ -308,19 +286,63 @@ p->timeBmc += clock() - clk;
SeeAlso []
***********************************************************************/
-int Ssw_ManSweep( Ssw_Man_t * p )
+void Ssw_CheckConstaints( Ssw_Man_t * p )
{
+ Aig_Obj_t * pObj, * pObj2;
+ int nConstrPairs, i;
+ int Counter = 0;
+ nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+ assert( (nConstrPairs & 1) == 0 );
+ for ( i = 0; i < nConstrPairs; i += 2 )
+ {
+ pObj = Aig_ManPo( p->pFrames, i );
+ pObj2 = Aig_ManPo( p->pFrames, i+1 );
+ if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
+ {
+ Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
+ Counter++;
+ }
+ }
+ printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
+ }
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweep( Ssw_Man_t * p )
+{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f;
- int v;
+// int v;
// perform speculative reduction
clk = clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
// add constraints
- Ssw_ManStartSolver( p );
+// p->pMSat = Ssw_SatStart( 0 );
+// Ssw_ManStartSolver( p );
+/*
+ {
+ int clk2 = clock();
+ Ssw_CheckConstaints( p );
+ PRT( "Time", clock() - clk2 );
+ }
+
+ Ssw_ManCleanup( p );
+ p->pFrames = Ssw_FramesWithClasses( p );
+ p->pMSat = Ssw_SatStart( 0 );
+// Ssw_ManStartSolver( p );
+*/
nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
assert( (nConstrPairs & 1) == 0 );
for ( i = 0; i < nConstrPairs; i += 2 )
@@ -333,17 +355,11 @@ clk = clock();
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
{
pObj = Aig_ManPo( p->pFrames, nConstrPairs + i );
- Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
}
- sat_solver_simplify( p->pSat );
+ sat_solver_simplify( p->pMSat->pSat );
p->timeReduce += clock() - clk;
- // mark nodes that do not have to be refined
-clk = clock();
- if ( p->pPars->fSkipCheck )
- Ssw_ManSweepMarkRefinement( p );
-p->timeMarkCones += clock() - clk;
-
//Ssw_ManUnique( p );
// map constants and PIs of the last frame
@@ -354,17 +370,26 @@ p->timeMarkCones += clock() - clk;
// make sure LOs are assigned
Saig_ManForEachLo( p->pAig, pObj, i )
assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
+/*
+ // mark the PI/LO of the last frame
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjNew = Ssw_ObjFrame( p, pObj, f );
+ Aig_Regular(pObjNew)->fMarkA = 1;
+ }
+*/
////
+/*
// bring up the previous frames
if ( p->pPars->fUniqueness )
for ( v = 0; v < f; v++ )
Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
+*/
////
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
- p->nRefUse = p->nRefSkip = 0;
p->nUniques = 0;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
index 888ed3da..0d9b016f 100644
--- a/src/aig/ssw/sswUnique.c
+++ b/src/aig/ssw/sswUnique.c
@@ -30,83 +30,39 @@
/**Function*************************************************************
- Synopsis [Returns the result of merging the two vectors.]
+ Synopsis [Performs computation of signal correspondence with constraints.]
- Description [Assumes that the vectors are sorted in the increasing order.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
{
- Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
- Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
- Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
- Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
- Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
- Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
- pBeg = (Aig_Obj_t **)vArr->pArray;
- while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ Aig_Obj_t * pObjLo, * pObj0, * pObj1;
+ int i;
+ if ( p->vDiffPairs == NULL )
+ p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
+ Vec_IntClear( p->vDiffPairs );
+ Saig_ManForEachLo( p->pAig, pObjLo, i )
{
- if ( (*pBeg1)->Id == (*pBeg2)->Id )
- *pBeg++ = *pBeg1++, pBeg2++;
- else if ( (*pBeg1)->Id < (*pBeg2)->Id )
- *pBeg++ = *pBeg1++;
+ pObj0 = Ssw_ObjFrame( p, pObjLo, 0 );
+ pObj1 = Ssw_ObjFrame( p, pObjLo, 1 );
+ if ( pObj0 == pObj1 )
+ Vec_IntPush( p->vDiffPairs, 0 );
+ else if ( pObj0 == Aig_Not(pObj1) )
+ Vec_IntPush( p->vDiffPairs, 1 );
else
- *pBeg++ = *pBeg2++;
+ {
+ // assume that if the nodes are structurally different
+ // they can also be functionally different
+ Vec_IntPush( p->vDiffPairs, 1 );
+ }
}
- while ( pBeg1 < pEnd1 )
- *pBeg++ = *pBeg1++;
- while ( pBeg2 < pEnd2 )
- *pBeg++ = *pBeg2++;
- vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
- assert( vArr->nSize <= vArr->nCap );
- assert( vArr->nSize >= vArr1->nSize );
- assert( vArr->nSize >= vArr2->nSize );
}
-/**Function*************************************************************
-
- Synopsis [Returns the result of merging the two vectors.]
-
- Description [Assumes that the vectors are sorted in the increasing order.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
-{
- Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
- Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
- Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
- Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
- Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
- Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
- pBeg = (Aig_Obj_t **)vArr->pArray;
- while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
- {
- if ( (*pBeg1)->Id == (*pBeg2)->Id )
- *pBeg++ = *pBeg1++, pBeg2++;
- else if ( (*pBeg1)->Id < (*pBeg2)->Id )
-// *pBeg++ = *pBeg1++;
- pBeg1++;
- else
-// *pBeg++ = *pBeg2++;
- pBeg2++;
- }
-// while ( pBeg1 < pEnd1 )
-// *pBeg++ = *pBeg1++;
-// while ( pBeg2 < pEnd2 )
-// *pBeg++ = *pBeg2++;
- vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
- assert( vArr->nSize <= vArr->nCap );
- assert( vArr->nSize <= vArr1->nSize );
- assert( vArr->nSize <= vArr2->nSize );
-}
/**Function*************************************************************
@@ -123,56 +79,32 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
int fVerbose = 0;
Aig_Obj_t * ppObjs[2], * pTemp;
- Vec_Ptr_t * vSupp, * vSupp2;
- int i, k, Value0, Value1, RetValue;
- assert( p->pPars->nFramesK > 1 );
+ int i, k, Value0, Value1, RetValue, fFeasible;
- vSupp = Vec_PtrAlloc( 100 );
- vSupp2 = Vec_PtrAlloc( 100 );
- Vec_PtrClear( p->vCommon );
+ assert( p->pPars->nFramesK > 1 );
+ assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
// compute the first support in terms of LOs
ppObjs[0] = pRepr;
ppObjs[1] = pObj;
- Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
- // modify support to be in terms of LIs
+ Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
+ // keep only LOs
+ RetValue = Vec_PtrSize( p->vCommon );
+ fFeasible = 0;
k = 0;
- Vec_PtrForEachEntry( vSupp, pTemp, i )
+ Vec_PtrForEachEntry( p->vCommon, pTemp, i )
if ( Saig_ObjIsLo(p->pAig, pTemp) )
- Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
- Vec_PtrShrink( vSupp, k );
- // compute the support of support
- Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
- // return support to LO
- Vec_PtrForEachEntry( vSupp, pTemp, i )
- Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
- // find the number of common vars
- Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
- Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
- Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
-/*
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
- printf( "Not unique!\n" );
- }
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
- printf( "Not unique!\n" );
- }
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
- printf( "Not unique!\n" );
- }
-*/
+ {
+ Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
+ if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
+ fFeasible = 1;
+ }
+ Vec_PtrShrink( p->vCommon, k );
+
if ( fVerbose )
- printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ",
- Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
+ printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
+ Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
+ fFeasible? "yes": "no " );
// check the current values
RetValue = 1;
@@ -185,14 +117,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
if ( fVerbose )
printf( "%d", Value0 ^ Value1 );
}
- if ( Vec_PtrSize(p->vCommon) == 0 )
- RetValue = 0;
if ( fVerbose )
printf( "\n" );
- Vec_PtrFree( vSupp );
- Vec_PtrFree( vSupp2 );
- return RetValue;
+ return RetValue && fFeasible;
}
/**Function*************************************************************
@@ -227,11 +155,10 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
// printf( "Skipped\n" );
return 0;
}
- p->nUniques++;
// create CNF
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) );
// add output constraint
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 05:41:57 +0000