summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/module.make2
-rw-r--r--src/aig/ssw/ssw.h51
-rw-r--r--src/aig/ssw/sswAig.c22
-rw-r--r--src/aig/ssw/sswBmc.c9
-rw-r--r--src/aig/ssw/sswClass.c114
-rw-r--r--src/aig/ssw/sswCnf.c15
-rw-r--r--src/aig/ssw/sswConstr.c635
-rw-r--r--src/aig/ssw/sswCore.c225
-rw-r--r--src/aig/ssw/sswDyn.c19
-rw-r--r--src/aig/ssw/sswFilter.c492
-rw-r--r--src/aig/ssw/sswInt.h38
-rw-r--r--src/aig/ssw/sswIslands.c31
-rw-r--r--src/aig/ssw/sswLcorr.c13
-rw-r--r--src/aig/ssw/sswMan.c29
-rw-r--r--src/aig/ssw/sswPairs.c13
-rw-r--r--src/aig/ssw/sswPart.c22
-rw-r--r--src/aig/ssw/sswSat.c39
-rw-r--r--src/aig/ssw/sswSemi.c11
-rw-r--r--src/aig/ssw/sswSim.c48
-rw-r--r--src/aig/ssw/sswSimSat.c37
-rw-r--r--src/aig/ssw/sswSweep.c51
-rw-r--r--src/aig/ssw/sswUnique.c11
22 files changed, 1710 insertions, 217 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 1e79c955..9d93fb93 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -2,8 +2,10 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswBmc.c \
src/aig/ssw/sswClass.c \
src/aig/ssw/sswCnf.c \
+ src/aig/ssw/sswConstr.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswDyn.c \
+ src/aig/ssw/sswFilter.c \
src/aig/ssw/sswIslands.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index c2a33ee4..207ebea9 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -21,6 +21,7 @@
#ifndef __SSW_H__
#define __SSW_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -29,9 +30,7 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -45,7 +44,8 @@ struct Ssw_Pars_t_
int nOverSize; // size of the overlap between partitions
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
- int nConstrs; // treat the last nConstrs POs as seq constraints
+ int fConstrs; // treat the last nConstrs POs as seq constraints
+ int fMergeFull; // enables full merge when constraints are used
int nMaxLevs; // the max number of levels of nodes to consider
int nBTLimit; // conflict limit at a node
int nBTLimitGlobal;// conflict limit for multiple runs
@@ -53,10 +53,13 @@ struct Ssw_Pars_t_
int nItersStop; // stop after the given number of iterations
int fDumpSRInit; // dumps speculative reduction
int nResimDelta; // the number of nodes to resimulate
+ int nStepsMax; // (scorr only) the max number of induction steps
+ int TimeLimit; // time out in seconds
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
+ int fOutputCorr; // perform 'PO correspondence'
int fSemiFormal; // enable semiformal filtering
- int fUniqueness; // enable uniqueness constraints
+// int fUniqueness; // enable uniqueness constraints
int fDynamic; // enable dynamic addition of constraints
int fLocalSim; // enable local simulation simulation
int fPartSigCorr; // uses partial signal correspondence
@@ -75,18 +78,9 @@ struct Ssw_Pars_t_
// internal parameters
int nIters; // the number of iterations performed
int nConflicts; // the total number of conflicts performed
-};
-
-// sequential counter-example
-typedef struct Ssw_Cex_t_ Ssw_Cex_t;
-struct Ssw_Cex_t_
-{
- int iPo; // the zero-based number of PO, for which verification failed
- int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
- int nRegs; // the number of registers in the miter
- int nPis; // the number of primary inputs in the miter
- int nBits; // the number of words of bit data used
- unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+ // callback
+ void * pData;
+ void * pFunc;
};
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
@@ -101,6 +95,8 @@ typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
/*=== sswBmc.c ==========================================================*/
extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
+/*=== sswConstr.c ==========================================================*/
+extern int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
@@ -110,7 +106,6 @@ extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPa
extern int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars );
extern int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars );
/*=== sswMiter.c ===================================================*/
-extern int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
@@ -127,15 +122,17 @@ extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-extern void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
-extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
-extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
-extern Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew );
-
-#ifdef __cplusplus
-}
-#endif
+extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+extern void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex );
+extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 62e93d2d..f3174470 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -142,7 +145,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
- int i, f;
+ int i, f, iLits;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
@@ -154,12 +157,17 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
+ iLits = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
+ {
+ pObjNew = Aig_ObjCreatePi(pFrames);
+ pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ }
// set the constraints on the latch outputs
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
@@ -170,10 +178,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
}
+ // transfer to the primary outputs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
+ Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
}
+ assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
// add the POs for the latch outputs of the last frame
Saig_ManForEachLo( p->pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
@@ -186,8 +198,6 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
return pFrames;
}
-
-
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
@@ -245,3 +255,5 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c
index 86d04424..aba32304 100644
--- a/src/aig/ssw/sswBmc.c
+++ b/src/aig/ssw/sswBmc.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -84,9 +87,9 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame )
+Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
Aig_Obj_t * pObj, * pObjFrames;
int f, i, nShift;
assert( Saig_ManRegNum(pFrm->pAig) > 0 );
@@ -217,3 +220,5 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index ce6ebf85..7fd2a21b 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
/*
The candidate equivalence classes are stored as a vector of pointers
to the array of pointers to the nodes in each class.
@@ -144,8 +147,8 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 );
p->vRefined = Vec_PtrAlloc( 1000 );
- assert( pAig->pReprs == NULL );
- Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+ if ( pAig->pReprs == NULL )
+ Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
return p;
}
@@ -412,7 +415,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
Aig_Obj_t ** ppClass;
Aig_Obj_t * pObj;
int i;
- printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
+ printf( "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
p->nCands1, p->nClasses, p->nCands1+p->nLits );
if ( !fVeryVerbose )
return;
@@ -508,7 +511,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
// sort through the candidates
nEntries = 0;
p->nCands1 = 0;
- Vec_PtrForEachEntry( vCands, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
{
assert( p->pClassSizes[pObj->Id] == 0 );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
@@ -547,7 +550,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
// copy the entries into storage in the topological order
nEntries2 = 0;
- Vec_PtrForEachEntry( vCands, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
{
nNodes = p->pClassSizes[pObj->Id];
// skip the nodes that are not representatives of non-trivial classes
@@ -587,7 +590,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
{
// int nFrames = 4;
// int nWords = 1;
@@ -622,7 +625,7 @@ if ( fVerbose )
// set comparison procedures
clk = clock();
- Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+ Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
// collect nodes to be considered as candidates
vCands = Vec_PtrAlloc( 1000 );
@@ -643,6 +646,22 @@ clk = clock();
}
Vec_PtrPush( vCands, pObj );
}
+
+ // this change will consider all PO drivers
+ if ( fOutputCorr )
+ {
+ Vec_PtrClear( vCands );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pObj->fMarkB = 0;
+ Saig_ManForEachPo( p->pAig, pObj, i )
+ if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
+ Aig_ObjFanin0(pObj)->fMarkB = 1;
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ if ( pObj->fMarkB )
+ Vec_PtrPush( vCands, pObj );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pObj->fMarkB = 0;
+ }
// allocate room for classes
p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
@@ -741,6 +760,69 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
SeeAlso []
***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig )
+{
+ Ssw_Cla_t * p;
+ Aig_Obj_t * pObj, * pRepr;
+ int * pClassSizes, nEntries, i;
+ // start the classes
+ p = Ssw_ClassesStart( pAig );
+ // allocate memory for classes
+ p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+ // count classes
+ p->nCands1 = 0;
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
+ {
+ p->nCands1++;
+ continue;
+ }
+ if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
+ {
+ if ( p->pClassSizes[pRepr->Id]++ == 0 )
+ p->pClassSizes[pRepr->Id]++;
+ }
+ }
+ // add nodes
+ nEntries = 0;
+ p->nClasses = 0;
+ pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( p->pClassSizes[i] )
+ {
+ p->pId2Class[i] = p->pMemClasses + nEntries;
+ nEntries += p->pClassSizes[i];
+ p->pId2Class[i][pClassSizes[i]++] = pObj;
+ p->nClasses++;
+ continue;
+ }
+ if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
+ continue;
+ if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
+ p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
+ }
+ p->pMemClassesFree = p->pMemClasses + nEntries;
+ p->nLits = nEntries - p->nClasses;
+ assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
+ ABC_FREE( pClassSizes );
+// printf( "After converting:\n" );
+// Ssw_ClassesPrint( p, 0 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates initial simulation classes.]
+
+ Description [Assumes that simulation info is assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
{
Ssw_Cla_t * p;
@@ -902,20 +984,20 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
// Vec_PtrPush( p->vRefined, pObj );
// get the new representative
- pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+ pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
assert( Vec_PtrSize(p->vClassOld) > 0 );
assert( Vec_PtrSize(p->vClassNew) > 0 );
// create old class
pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
- Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
{
pClassOld[i] = pObj;
Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
}
// create new class
pClassNew = pClassOld + i;
- Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
{
pClassNew[i] = pObj;
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
@@ -972,21 +1054,21 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
return 0;
// collect the nodes to be refined
Vec_PtrClear( p->vClassNew );
- Vec_PtrForEachEntry( vRoots, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
Vec_PtrPush( p->vClassNew, pObj );
// check if there is a new class
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
p->nCands1 -= Vec_PtrSize(p->vClassNew);
- pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+ pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
if ( Vec_PtrSize(p->vClassNew) == 1 )
return 1;
// create a new class composed of these nodes
ppClassNew = p->pMemClassesFree;
p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
- Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
{
ppClassNew[i] = pObj;
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
@@ -1029,14 +1111,14 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
p->nCands1 -= Vec_PtrSize(p->vClassNew);
- pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+ pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
if ( Vec_PtrSize(p->vClassNew) == 1 )
return 1;
// create a new class composed of these nodes
ppClassNew = p->pMemClassesFree;
p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
- Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
{
ppClassNew[i] = pObj;
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
@@ -1054,3 +1136,5 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index 73fa0b02..1970c62f 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -228,7 +231,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
pLits = ABC_ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
{
pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
@@ -241,7 +244,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
assert( RetValue );
}
// add A & B => C or !A + !B + C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
{
pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
if ( p->fPolarFlip )
@@ -357,7 +360,7 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
vFrontier = Vec_PtrAlloc( 100 );
Ssw_ObjAddToFrontier( p, pObj, vFrontier );
// explore nodes in the frontier
- Vec_PtrForEachEntry( vFrontier, pNode, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
{
// create the supergate
assert( Ssw_ObjSatNum(p,pNode) );
@@ -368,14 +371,14 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Ssw_AddClausesMux( p, pNode );
}
else
{
Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Ssw_AddClausesSuper( p, pNode, p->vFanins );
}
@@ -421,3 +424,5 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswConstr.c b/src/aig/ssw/sswConstr.c
new file mode 100644
index 00000000..e233f133
--- /dev/null
+++ b/src/aig/ssw/sswConstr.c
@@ -0,0 +1,635 @@
+/**CFile****************************************************************
+
+ FileName [sswConstr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [One round of SAT sweeping.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswConstr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "cnf.h"
+#include "bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Constructs initialized timeframes with constraints as POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f;
+ assert( Saig_ManConstrNum(p) > 0 );
+ assert( Aig_ManRegNum(p) > 0 );
+ assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+ // start the fraig package
+ pFrames = Aig_ManStart( Aig_ManObjNumMax(p) * nFrames );
+ // create latches for the first frame
+ Saig_ManForEachLo( p, pObj, i )
+ Aig_ObjSetCopy( pObj, Aig_ManConst0(pFrames) );
+ // add timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // map constants and PIs
+ Aig_ObjSetCopy( Aig_ManConst1(p), Aig_ManConst1(pFrames) );
+ Saig_ManForEachPi( p, pObj, i )
+ Aig_ObjSetCopy( pObj, Aig_ObjCreatePi(pFrames) );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( p, pObj, i )
+ Aig_ObjSetCopy( pObj, Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ) );
+ // transfer to the primary output
+ Aig_ManForEachPo( p, pObj, i )
+ Aig_ObjSetCopy( pObj, Aig_ObjChild0Copy(pObj) );
+ // create constraint outputs
+ Saig_ManForEachPo( p, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
+ continue;
+ Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
+ }
+ // transfer latch inputs to the latch outputs
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ Aig_ObjSetCopy( pObjLo, Aig_ObjCopy(pObjLi) );
+ }
+ // remove dangling nodes
+ Aig_ManCleanup( pFrames );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds one satisfiable assignment of the timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
+{
+ Aig_Man_t * pFrames;
+ sat_solver * pSat;
+ Cnf_Dat_t * pCnf;
+ Aig_Obj_t * pObj;
+ int i, RetValue;
+ if ( pvInits )
+ *pvInits = NULL;
+ assert( p->nConstrs > 0 );
+ // derive the timeframes
+ pFrames = Ssw_FramesWithConstraints( p, nFrames );
+ // create CNF
+ pCnf = Cnf_Derive( pFrames, 0 );
+ // create SAT solver
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( pSat == NULL )
+ {
+ Cnf_DataFree( pCnf );
+ Aig_ManStop( pFrames );
+ return 1;
+ }
+ // solve
+ RetValue = sat_solver_solve( pSat, NULL, NULL,
+ (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ if ( RetValue == l_True && pvInits )
+ {
+ *pvInits = Vec_IntAlloc( 1000 );
+ Aig_ManForEachPi( pFrames, pObj, i )
+ Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );
+
+// Aig_ManForEachPi( pFrames, pObj, i )
+// printf( "%d", Vec_IntEntry(*pvInits, i) );
+// printf( "\n" );
+ }
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ Aig_ManStop( pFrames );
+ if ( RetValue == l_False )
+ return 1;
+ if ( RetValue == l_True )
+ return 0;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
+{
+ Vec_Int_t * vLits;
+ sat_solver * pSat;
+ Cnf_Dat_t * pCnf;
+ Aig_Obj_t * pObj;
+ int i, f, iVar, RetValue, nRegs;
+ if ( pvInits )
+ *pvInits = NULL;
+ assert( p->nConstrs > 0 );
+ // create CNF
+ nRegs = p->nRegs; p->nRegs = 0;
+ pCnf = Cnf_Derive( p, Aig_ManPoNum(p) );
+ p->nRegs = nRegs;
+ // create SAT solver
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+ assert( pSat->size == nFrames * pCnf->nVars );
+ // collect constraint literals
+ vLits = Vec_IntAlloc( 100 );
+ Saig_ManForEachLo( p, pObj, i )
+ {
+ assert( pCnf->pVarNums[Aig_ObjId(pObj)] >= 0 );
+ Vec_IntPush( vLits, toLitCond(pCnf->pVarNums[Aig_ObjId(pObj)], 1) );
+ }
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Saig_ManForEachPo( p, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
+ continue;
+ assert( pCnf->pVarNums[Aig_ObjId(pObj)] >= 0 );
+ iVar = pCnf->pVarNums[Aig_ObjId(pObj)] + pCnf->nVars*f;
+ Vec_IntPush( vLits, toLitCond(iVar, 1) );
+ }
+ }
+ RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits),
+ (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits),
+ (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ if ( RetValue == l_True && pvInits )
+ {
+ *pvInits = Vec_IntAlloc( 1000 );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Saig_ManForEachPi( p, pObj, i )
+ {
+ iVar = pCnf->pVarNums[Aig_ObjId(pObj)] + pCnf->nVars*f;
+ Vec_IntPush( *pvInits, sat_solver_var_value(pSat, iVar) );
+ }
+ }
+ }
+ sat_solver_delete( pSat );
+ Vec_IntFree( vLits );
+ Cnf_DataFree( pCnf );
+ if ( RetValue == l_False )
+ return 1;
+ if ( RetValue == l_True )
+ return 0;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManPrintPolarity( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManForEachObj( p, pObj, i )
+ printf( "%d", pObj->fPhase );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObjLi;
+ int f, i, iLits, RetValue1, RetValue2;
+ int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig);
+ assert( Vec_IntSize(p->vInits) % Saig_ManPiNum(p->pAig) == 0 );
+ // assign register outputs
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ pObj->fMarkB = 0;
+ // simulate the timeframes
+ iLits = 0;
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // set the PI simulation information
+ Aig_ManConst1(p->pAig)->fMarkB = 1;
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ pObj->fMarkB = Vec_IntEntry( p->vInits, iLits++ );
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
+ pObj->fMarkB = pObjLi->fMarkB;
+ // simulate internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // assign the COs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+ // check the outputs
+ Saig_ManForEachPo( p->pAig, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
+ {
+ if ( pObj->fMarkB )
+ printf( "output %d failed in frame %d.\n", i, f );
+ }
+ else
+ {
+ if ( pObj->fMarkB )
+ printf( "constraint %d failed in frame %d.\n", i, f );
+ }
+ }
+ // transfer
+ if ( f == 0 )
+ { // copy markB into phase
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pObj->fPhase = pObj->fMarkB;
+ }
+ else
+ { // refine classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
+ }
+ }
+ assert( iLits == Vec_IntSize(p->vInits) );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
+{
+ Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
+ int RetValue;
+ // get representative of this class
+ pObjRepr = Aig_ObjRepr( p->pAig, pObj );
+ if ( pObjRepr == NULL )
+ return 0;
+ // get the fraiged node
+ pObjFraig = Ssw_ObjFrame( p, pObj, f );
+ // get the fraiged representative
+ pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
+ // check if constant 0 pattern distinquishes these nodes
+ assert( pObjFraig != NULL && pObjReprFraig != NULL );
+ assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
+ // if the fraiged nodes are the same, return
+ if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+ return 0;
+ // call equivalence checking
+ 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) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+ Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
+ return 0;
+ }
+ if ( RetValue == -1 ) // timed out
+ {
+ Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+ return 1;
+ }
+ // disproved equivalence
+ Ssw_SmlSavePatternAig( p, f );
+ Ssw_ManResimulateBit( p, pObj, pObjRepr );
+ assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+ if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
+ {
+ printf( "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Ssw_ManSweepBmcConstr_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjNew, * pObjLi;
+ pObjNew = Ssw_ObjFrame( p, pObj, f );
+ if ( pObjNew )
+ return pObjNew;
+ assert( !Saig_ObjIsPi(p->pAig, pObj) );
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ {
+ assert( f > 0 );
+ pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
+ pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObjLi), f-1 );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) );
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f );
+ Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin1(pObj), f );
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ }
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ assert( pObjNew != NULL );
+ return pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
+{
+ Bar_Progress_t * pProgress = NULL;
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
+ int i, f, iLits, clk;
+clk = clock();
+
+ // start initialized timeframes
+ p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
+
+ // build the constraint outputs
+ iLits = 0;
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // map constants and PIs
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi(p->pFrames);
+ pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ }
+ // build the constraint cones
+ Saig_ManForEachPo( p->pAig, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
+ continue;
+ pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+ if ( Aig_Regular(pObjNew) == Aig_ManConst1(p->pFrames) )
+ {
+ assert( Aig_IsComplement(pObjNew) );
+ continue;
+ }
+ Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) );
+ }
+ }
+ assert( Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
+
+ // sweep internal nodes
+ p->fRefined = 0;
+ if ( p->pPars->fVerbose )
+ pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // sweep internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ {
+ if ( p->pPars->fVerbose )
+ Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
+ }
+ // quit if this is the last timeframe
+ if ( f == p->pPars->nFramesK - 1 )
+ break;
+ // transfer latch input to the latch outputs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
+ // build logic cones for register outputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Ssw_ObjFrame( p, pObjLi, f );
+ Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
+ }
+ }
+ if ( p->pPars->fVerbose )
+ Bar_ProgressStop( pProgress );
+
+ // cleanup
+// Ssw_ClassesCheck( p->ppClasses );
+p->timeBmc += clock() - clk;
+ return p->fRefined;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Ssw_FramesWithClasses_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjNew, * pObjLi;
+ pObjNew = Ssw_ObjFrame( p, pObj, f );
+ if ( pObjNew )
+ return pObjNew;
+ assert( !Saig_ObjIsPi(p->pAig, pObj) );
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ {
+ assert( f > 0 );
+ pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
+ pObjNew = Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObjLi), f-1 );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) );
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f );
+ Ssw_FramesWithClasses_rec( p, Aig_ObjFanin1(pObj), f );
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ }
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ assert( pObjNew != NULL );
+ return pObjNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepConstr( Ssw_Man_t * p )
+{
+ Bar_Progress_t * pProgress = NULL;
+ Aig_Obj_t * pObj, * pObj2, * pObjNew;
+ int nConstrPairs, clk, i, f, iLits;
+//Ssw_ManPrintPolarity( p->pAig );
+
+ // perform speculative reduction
+clk = clock();
+ // create timeframes
+ p->pFrames = Ssw_FramesWithClasses( p );
+ // add constants
+ 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 );
+ Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
+ }
+ // build logic cones for register inputs
+ for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+ {
+ pObj = Aig_ManPo( p->pFrames, nConstrPairs + i );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
+ }
+
+ // map constants and PIs of the last frame
+ f = p->pPars->nFramesK;
+// iLits = 0;
+ iLits = f * Saig_ManPiNum(p->pAig);
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi(p->pFrames);
+ pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ }
+ assert( Vec_IntSize(p->vInits) == iLits );
+p->timeReduce += clock() - clk;
+
+ // add constraints to all timeframes
+ for ( f = 0; f <= p->pPars->nFramesK; f++ )
+ {
+ Saig_ManForEachPo( p->pAig, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
+ continue;
+ Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f );
+// if ( Aig_Regular(Ssw_ObjChild0Fra(p,pObj,f)) == Aig_ManConst1(p->pFrames) )
+ if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst0(p->pFrames) )
+ continue;
+ assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) );
+ if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) )
+ {
+ printf( "Polarity violation.\n" );
+ continue;
+ }
+ Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) );
+ }
+ }
+ f = p->pPars->nFramesK;
+ // clean the solver
+ sat_solver_simplify( p->pMSat->pSat );
+
+
+ // sweep internal nodes
+ p->fRefined = 0;
+ Ssw_ClassesClearRefined( p->ppClasses );
+ if ( p->pPars->fVerbose )
+ pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( p->pPars->fVerbose )
+ Bar_ProgressUpdate( pProgress, i, NULL );
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
+ }
+ }
+ if ( p->pPars->fVerbose )
+ Bar_ProgressStop( pProgress );
+ // cleanup
+// Ssw_ClassesCheck( p->ppClasses );
+ return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 6cb84800..c277d76e 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -46,16 +49,18 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth
p->nFramesAddSim = 2; // additional frames to simulate
- p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
+ p->fConstrs = 0; // treat the last nConstrs POs as seq constraints
+ p->fMergeFull = 0; // enables full merge when constraints are used
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 = -1; // stop after the given number of iterations
p->nResimDelta = 1000; // the internal of nodes to resimulate
+ p->nStepsMax = -1; // (scorr only) the max number of induction steps
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
+ p->fOutputCorr = 0; // perform 'PO correspondence'
p->fSemiFormal = 0; // enable semiformal filtering
- p->fUniqueness = 0; // enable uniqueness constraints
p->fDynamic = 0; // dynamic partitioning
p->fLocalSim = 0; // local simulation
p->fVerbose = 0; // verbose stats
@@ -90,6 +95,130 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
/**Function*************************************************************
+ Synopsis [Reports improvements for property cones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop )
+{
+ Aig_Man_t * pAig1, * pAig2, * pAux;
+ pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 );
+ pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0 );
+ Aig_ManStop( pAux );
+ pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
+ pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0 );
+ Aig_ManStop( pAux );
+
+ p->nNodesBegC = Aig_ManNodeNum(pAig1);
+ p->nNodesEndC = Aig_ManNodeNum(pAig2);
+ p->nRegsBegC = Aig_ManRegNum(pAig1);
+ p->nRegsEndC = Aig_ManRegNum(pAig2);
+
+ Aig_ManStop( pAig1 );
+ Aig_ManStop( pAig2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( pObj == Aig_ManConst1(p) )
+ printf( "1" );
+ else if ( pObj == Aig_ManConst0(p) )
+ printf( "0" );
+ else
+ printf( "X" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports improvements for property cones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportOutputs( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
+ printf( "o" );
+ else
+ printf( "c" );
+ Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Remove from-equivs that are in the cone of constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+{
+ Vec_Ptr_t * vCones;
+ Aig_Obj_t ** pArray;
+ Aig_Obj_t * pObj;
+ int i, nTotal = 0, nRemoved = 0;
+ // collect the nodes in the cone of constraints
+ pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos);
+ pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
+ vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
+ // remove all the node that are equiv to something and are in the cones
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ if ( pAig->pReprs[i] != NULL )
+ nTotal++;
+ if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ continue;
+ if ( pAig->pReprs[i] )
+ {
+ if ( p->pPars->fConstrs && !p->pPars->fMergeFull )
+ {
+ pAig->pReprs[i] = NULL;
+ nRemoved++;
+ }
+ }
+ }
+ // collect statistics
+ p->nConesTotal = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig);
+ p->nConesConstr = Vec_PtrSize(vCones);
+ p->nEquivsTotal = nTotal;
+ p->nEquivsConstr = nRemoved;
+ Vec_PtrFree( vCones );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs computation of signal correspondence with constraints.]
Description []
@@ -118,9 +247,10 @@ 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 );
+ if ( p->pPars->fConstrs )
+ Ssw_ManSweepBmcConstr( p );
+ else
+ Ssw_ManSweepBmc( p );
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );
@@ -142,10 +272,25 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Aig_ManStop( pSRed );
}
*/
+ if ( p->pPars->pFunc )
+ {
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+ }
+ if ( p->pPars->nStepsMax == 0 )
+ {
+ printf( "Stopped signal correspondence after BMC.\n" );
+ goto finalize;
+ }
// refine classes using induction
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
for ( nIter = 0; ; nIter++ )
{
+ if ( p->pPars->nStepsMax == nIter )
+ {
+ printf( "Stopped signal correspondence after %d refiment iterations.\n", nIter );
+ goto finalize;
+ }
if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
{
Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
@@ -174,19 +319,20 @@ clk = clock();
}
else
{
- if ( p->pPars->fDynamic )
+ if ( p->pPars->fConstrs )
+ RetValue = Ssw_ManSweepConstr( p );
+ else if ( p->pPars->fDynamic )
RetValue = Ssw_ManSweepDyn( p );
else
RetValue = Ssw_ManSweep( p );
+
p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
if ( p->pPars->fVerbose )
{
printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
- if ( p->pPars->fUniqueness )
- printf( "U =%4d. ", p->nUniques-nUniques );
- else if ( p->pPars->fDynamic )
+ if ( p->pPars->fDynamic )
{
printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
printf( "R =%4d. ", p->nRecycles-nRecycles );
@@ -211,9 +357,15 @@ clk = clock();
Ssw_ManCleanup( p );
if ( !RetValue )
break;
+ if ( p->pPars->pFunc )
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
}
+
+finalize:
p->pPars->nIters = nIter + 1;
p->timeTotal = clock() - clkTotal;
+
+ Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
pAigNew = Aig_ManDupRepr( p->pAig, 0 );
Aig_ManSeqCleanup( pAigNew );
//Ssw_ClassesPrint( p->ppClasses, 1 );
@@ -221,6 +373,9 @@ p->timeTotal = clock() - clkTotal;
p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses );
p->nNodesEnd = Aig_ManNodeNum(pAigNew);
p->nRegsEnd = Aig_ManRegNum(pAigNew);
+ // cleanup
+ Aig_ManSetPhase( p->pAig );
+ Aig_ManCleanMarkB( p->pAig );
return pAigNew;
}
@@ -255,13 +410,6 @@ 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 constraints to work.\n" );
- pPars->nFramesK = 2;
- }
if ( pPars->fLatchCorrOpt )
{
pPars->fLatchCorr = 1;
@@ -291,15 +439,31 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
}
}
-
+
// start the induction manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes
// p->pPars->nConstrs = 1;
- if ( p->pPars->nConstrs == 0 )
+ if ( p->pPars->fConstrs )
+ {
+ // create trivial equivalence classes with all nodes being candidates for constant 1
+ p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+ Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
+ // derive phase bits to satisfy the constraints
+ if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
+ {
+ printf( "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
+ p->pPars->fVerbose = 0;
+ Ssw_ManStop( p );
+ return NULL;
+ }
+ // perform simulation of the first timeframes
+ Ssw_ManRefineByConstrSim( p );
+ }
+ else
{
// perform one round of seq simulation and generate candidate equivalence classes
- p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
// p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
if ( pPars->fLatchCorrOpt )
p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
@@ -307,21 +471,16 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
else
p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 );
- Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
- }
- else
- {
- // create trivial equivalence classes with all nodes being candidates for constant 1
- p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
- Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
}
+ // allocate storage
if ( p->pPars->fLocalSim )
p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
- if ( pPars->fUniqueness )
- printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n",
- p->nUniquesAdded, p->nUniquesUseful );
+// Ssw_ReportOutputs( pAigNew );
+ if ( pPars->fConstrs && pPars->fVerbose )
+ Ssw_ReportConeReductions( p, pAig, pAigNew );
// cleanup
Ssw_ManStop( p );
return pAigNew;
@@ -340,10 +499,14 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
***********************************************************************/
Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
+ Aig_Man_t * pRes;
Ssw_Pars_t Pars;
if ( pPars == NULL )
Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
- return Ssw_SignalCorrespondence( pAig, pPars );
+ pRes = Ssw_SignalCorrespondence( pAig, pPars );
+// if ( pPars->fConstrs && pPars->fVerbose )
+// Ssw_ReportConeReductions( pAig, pRes );
+ return pRes;
}
@@ -352,3 +515,5 @@ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
index 04e66f09..7e8edc66 100644
--- a/src/aig/ssw/sswDyn.c
+++ b/src/aig/ssw/sswDyn.c
@@ -21,6 +21,9 @@
#include "sswInt.h"
#include "bar.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -153,7 +156,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
Ssw_ManCollectPis_rec( pObj, p->vNewLos );
// add logic cones for register outputs
- Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
{
pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
@@ -172,7 +175,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
// collect the related constraint POs
Vec_IntClear( p->vNewPos );
- Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
// check if the corresponding pairs are added
Vec_IntForEachEntry( p->vNewPos, iConstr, i )
@@ -222,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
}
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsPi(pObjFraig) );
- pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
}
// set random simulation info for the second frame
@@ -233,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
pObjFraig = Ssw_ObjFrame( p, pObj, f );
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsPi(pObjFraig) );
- pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
}
}
@@ -327,10 +330,10 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
// Aig_ManIncrementTravId( p->pAig );
// Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
p->nVisCounter++;
- Vec_PtrForEachEntry( p->vResimConsts, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i )
Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
// resimulate the cone of influence of the cand classes
- Vec_PtrForEachEntry( p->vResimClasses, pRepr, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
{
ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
for ( k = 0; k < nSize; k++ )
@@ -343,7 +346,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
// refine these nodes
RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
RetValue2 = 0;
- Vec_PtrForEachEntry( p->vResimClasses, pRepr, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );
// prepare simulation info for the next round
@@ -482,3 +485,5 @@ p->timeReduce += clock() - clk;
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswFilter.c b/src/aig/ssw/sswFilter.c
new file mode 100644
index 00000000..a0c0934a
--- /dev/null
+++ b/src/aig/ssw/sswFilter.c
@@ -0,0 +1,492 @@
+/**CFile****************************************************************
+
+ FileName [sswConstr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [One round of SAT sweeping.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswConstr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
+{
+ Aig_Obj_t * pObj, * pObjLi;
+ int f, i, RetValue1, RetValue2;
+ assert( nFrames > 0 );
+ // assign register outputs
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i );
+ // simulate the timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // set the PI simulation information
+ Aig_ManConst1(p->pAig)->fMarkB = 1;
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ pObj->fMarkB = 0;
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
+ pObj->fMarkB = pObjLi->fMarkB;
+ // simulate internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // assign the COs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+ // transfer
+ if ( f == 0 )
+ { // copy markB into phase
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pObj->fPhase = pObj->fMarkB;
+ }
+ else
+ { // refine classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
+ }
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
+{
+ Aig_Obj_t * pObj, * pObjLi;
+ int f, i;
+ assert( nFrames > 0 );
+ // assign register outputs
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i );
+ // simulate the timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // set the PI simulation information
+ Aig_ManConst1(p->pAig)->fMarkB = 1;
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ pObj->fMarkB = Aig_ManRandom(0) & 1;
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
+ pObj->fMarkB = pObjLi->fMarkB;
+ // simulate internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // assign the COs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+ }
+ // record the new pattern
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ if ( pObj->fMarkB ^ Aig_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) )
+ Aig_InfoXorBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
+{
+ Aig_Obj_t * pObj, * pObjLi;
+ int f, i, iBit;
+ // assign register outputs
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ pObj->fMarkB = 0;
+ // simulate the timeframes
+ iBit = pCex->nRegs;
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ {
+ // set the PI simulation information
+ Aig_ManConst1(p->pAig)->fMarkB = 1;
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit( pCex->pData, iBit++ );
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
+ pObj->fMarkB = pObjLi->fMarkB;
+ // simulate internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // assign the COs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+ }
+ assert( iBit == pCex->nBits );
+ // check that the output failed as expected -- cannot check because it is not an SRM!
+// pObj = Aig_ManPo( p->pAig, pCex->iPo );
+// if ( pObj->fMarkB != 1 )
+// printf( "The counter-example does not refine the output.\n" );
+ // record the new pattern
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ if ( pObj->fMarkB ^ Aig_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) )
+ Aig_InfoXorBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
+ int RetValue;
+ // get representative of this class
+ pObjRepr = Aig_ObjRepr( p->pAig, pObj );
+ if ( pObjRepr == NULL )
+ return 0;
+ // get the fraiged node
+ pObjFraig = Ssw_ObjFrame( p, pObj, f );
+ // get the fraiged representative
+ pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
+ // check if constant 0 pattern distinquishes these nodes
+ assert( pObjFraig != NULL && pObjReprFraig != NULL );
+ assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
+ // if the fraiged nodes are the same, return
+ if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+ return 0;
+ // call equivalence checking
+ 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) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+ Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
+ return 0;
+ }
+ if ( RetValue == -1 ) // timed out
+ {
+// Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+ return 1;
+ }
+ // disproved equivalence
+ Ssw_SmlSavePatternAig( p, f );
+ Ssw_ManResimulateBit( p, pObj, pObjRepr );
+ assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+ if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
+ {
+ printf( "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Ssw_ManSweepBmcFilter_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjNew, * pObjLi;
+ pObjNew = Ssw_ObjFrame( p, pObj, f );
+ if ( pObjNew )
+ return pObjNew;
+ assert( !Saig_ObjIsPi(p->pAig, pObj) );
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ {
+ assert( f > 0 );
+ pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
+ pObjNew = Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin0(pObjLi), f-1 );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObjLi) );
+ }
+ else
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin0(pObj), f );
+ Ssw_ManSweepBmcFilter_rec( p, Aig_ObjFanin1(pObj), f );
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ }
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ assert( pObjNew != NULL );
+ return pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Filter equivalence classes of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
+{
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
+ int f, f1, i, clkTotal = clock();
+ // start initialized timeframes
+ p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ {
+ if ( Aig_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ) )
+ {
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst1(p->pFrames) );
+//printf( "1" );
+ }
+ else
+ {
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
+//printf( "0" );
+ }
+ }
+//printf( "\n" );
+
+ // sweep internal nodes
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // realloc mapping of timeframes
+ if ( f == p->nFrames-1 )
+ {
+ Aig_Obj_t ** pNodeToFrames;
+ pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * 2 * p->nFrames );
+ for ( f1 = 0; f1 < p->nFrames; f1++ )
+ {
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pNodeToFrames[2*p->nFrames*pObj->Id + f1] = Ssw_ObjFrame( p, pObj, f1 );
+ }
+ ABC_FREE( p->pNodeToFrames );
+ p->pNodeToFrames = pNodeToFrames;
+ p->nFrames *= 2;
+ }
+ // map constants and PIs
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi(p->pFrames);
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ }
+ // 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_ManSweepNodeFilter( p, pObj, f ) )
+ break;
+ }
+ // printout
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Frame %4d : ", f );
+ Ssw_ClassesPrint( p->ppClasses, 0 );
+ }
+ if ( i < Vec_PtrSize(p->pAig->vObjs) )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit );
+ break;
+ }
+ // quit if this is the last timeframe
+ if ( f == p->pPars->nFramesK - 1 )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK );
+ break;
+ }
+ // check timeout
+ if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ break;
+ // transfer latch input to the latch outputs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
+ // build logic cones for register outputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Ssw_ObjFrame( p, pObjLi, f );
+ Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
+ }
+ }
+ // verify
+// Ssw_ClassesCheck( p->ppClasses );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Filter equivalence classes of nodes.]
+
+ Description [Unrolls at most nFramesMax frames. Works with nConfMax
+ conflicts until the first undefined SAT call. Verbose prints the message.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
+{
+ Ssw_Pars_t Pars, * pPars = &Pars;
+ Ssw_Man_t * p;
+ int r, TimeLimitPart, clkTotal = clock();
+ assert( Aig_ManRegNum(pAig) > 0 );
+ assert( Aig_ManConstrNum(pAig) == 0 );
+ // consider the case of empty AIG
+ if ( Aig_ManNodeNum(pAig) == 0 )
+ return;
+ // reset random numbers
+ Aig_ManRandom( 1 );
+ // if parameters are not given, create them
+ Ssw_ManSetDefaultParams( pPars = &Pars );
+ pPars->nFramesK = 3; //nFramesMax;
+ pPars->nBTLimit = nConfMax;
+ pPars->TimeLimit = TimeLimit;
+ pPars->fVerbose = fVerbose;
+ // start the induction manager
+ p = Ssw_ManCreate( pAig, pPars );
+ pPars->nFramesK = nFramesMax;
+ // create trivial equivalence classes with all nodes being candidates for constant 1
+ if ( pAig->pReprs == NULL )
+ p->ppClasses = Ssw_ClassesPrepareSimple( pAig, 0, 0 );
+ else
+ p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
+ Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
+ assert( p->vInits == NULL );
+ // compute starting state if needed
+ if ( pCex )
+ Ssw_ManFindStartingState( p, pCex );
+ // refine classes using BMC
+ for ( r = 0; r < nRounds; r++ )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Round %3d:\n", r );
+ // start filtering equivalence classes
+ Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK );
+ if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
+ {
+ printf( "All equivalences are refined away.\n" );
+ break;
+ }
+ // printout
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Initial : " );
+ Ssw_ClassesPrint( p->ppClasses, 0 );
+ }
+ p->pMSat = Ssw_SatStart( 0 );
+ TimeLimitPart = TimeLimit ? TimeLimit - (int)((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) : 0;
+ if ( TimeLimit2 )
+ {
+ if ( TimeLimitPart )
+ TimeLimitPart = ABC_MIN( TimeLimitPart, TimeLimit2 );
+ else
+ TimeLimitPart = TimeLimit2;
+ }
+ Ssw_ManSweepBmcFilter( p, TimeLimitPart );
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = NULL;
+ Ssw_ManCleanup( p );
+ // simulate pattern forward
+ Ssw_ManRollForward( p, p->pPars->nFramesK );
+ // check timeout
+ if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ {
+ printf( "Reached timeout (%d seconds).\n", TimeLimit );
+ break;
+ }
+ }
+ // cleanup
+ Aig_ManSetPhase( p->pAig );
+ Aig_ManCleanMarkB( p->pAig );
+ // cleanup
+ pPars->fVerbose = 0;
+ Ssw_ManStop( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Filter equivalence classes of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
+{
+ Aig_Man_t * pAig;
+ pAig = Gia_ManToAigSimple( p );
+ if ( p->pReprs != NULL )
+ {
+ Gia_ManReprToAigRepr2( pAig, p );
+ ABC_FREE( p->pReprs );
+ ABC_FREE( p->pNexts );
+ }
+ Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fVerbose );
+ Gia_ManReprFromAigRepr( pAig, p );
+ Aig_ManStop( pAig );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 269bdad7..e3a9a341 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -21,6 +21,7 @@
#ifndef __SSW_INT_H__
#define __SSW_INT_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -33,9 +34,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -93,6 +95,7 @@ struct Ssw_Man_t_
int iNodeLast; // the last node considered
Vec_Ptr_t * vResimConsts; // resimulation constants
Vec_Ptr_t * vResimClasses; // resimulation classes
+ Vec_Int_t * vInits; // the init values of primary inputs under constraints
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
@@ -113,6 +116,15 @@ struct Ssw_Man_t_
int nNodesEnd;
int nRegsBeg;
int nRegsEnd;
+ // equiv statistis
+ int nConesTotal;
+ int nConesConstr;
+ int nEquivsTotal;
+ int nEquivsConstr;
+ int nNodesBegC;
+ int nNodesEndC;
+ int nRegsBegC;
+ int nRegsEndC;
// runtime stats
int timeBmc; // bounded model checking
int timeReduce; // speculative reduction
@@ -172,7 +184,7 @@ 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 Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return (Aig_Obj_t *)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; }
@@ -206,8 +218,9 @@ extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr,
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
-extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose );
+extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
@@ -220,6 +233,10 @@ 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 );
+/*=== sswConstr.c ===================================================*/
+extern int Ssw_ManSweepBmcConstr( Ssw_Man_t * p );
+extern int Ssw_ManSweepConstr( Ssw_Man_t * p );
+extern void Ssw_ManRefineByConstrSim( Ssw_Man_t * p );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswDyn.c ===================================================*/
@@ -231,10 +248,10 @@ extern int Ssw_ManSweepLatch( Ssw_Man_t * p );
extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern void Ssw_ManCleanup( Ssw_Man_t * p );
extern void Ssw_ManStop( Ssw_Man_t * p );
-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 );
+extern int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj );
/*=== sswSemi.c ===================================================*/
extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswSim.c ===================================================*/
@@ -259,6 +276,7 @@ extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_
extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
+extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
@@ -267,9 +285,11 @@ extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose );
extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
index 8913116c..d1ebe4bc 100644
--- a/src/aig/ssw/sswIslands.c
+++ b/src/aig/ssw/sswIslands.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -99,7 +102,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
{
if ( pObj0->pData == NULL )
continue;
- pObj1 = pObj0->pData;
+ pObj1 = (Aig_Obj_t *)pObj0->pData;
if ( !Saig_ObjIsLo(p1, pObj1) )
printf( "Mismatch between LO pairs.\n" );
}
@@ -107,7 +110,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
{
if ( pObj1->pData == NULL )
continue;
- pObj0 = pObj1->pData;
+ pObj0 = (Aig_Obj_t *)pObj1->pData;
if ( !Saig_ObjIsLo(p0, pObj0) )
printf( "Mismatch between LO pairs.\n" );
}
@@ -234,9 +237,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
{
Ssw_MatchingExtendOne( p0, vNodes0 );
Ssw_MatchingExtendOne( p1, vNodes1 );
- Vec_PtrForEachEntry( vNodes0, pNext0, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
{
- pNext1 = pNext0->pData;
+ pNext1 = (Aig_Obj_t *)pNext0->pData;
if ( pNext1 == NULL )
continue;
assert( pNext1->pData == pNext0 );
@@ -245,9 +248,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
pNext0->pData = NULL;
pNext1->pData = NULL;
}
- Vec_PtrForEachEntry( vNodes1, pNext0, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
{
- pNext1 = pNext0->pData;
+ pNext1 = (Aig_Obj_t *)pNext0->pData;
if ( pNext1 == NULL )
continue;
assert( pNext1->pData == pNext0 );
@@ -307,7 +310,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
pObj1->pData = pObj0;
}
// create register outputs in p0 that are absent in p1
- Vec_PtrForEachEntry( vNewLis, pObj0Li, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) );
// increment the number of registers
Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
@@ -342,7 +345,7 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
{
if ( Aig_ObjIsPo(pObj0) )
continue;
- pObj1 = pObj0->pData;
+ pObj1 = (Aig_Obj_t *)pObj0->pData;
Vec_IntPush( vPairsNew, pObj0->Id );
Vec_IntPush( vPairsNew, pObj1->Id );
}
@@ -379,11 +382,11 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
assert( pObj1->pData != NULL );
if ( pObj0->pData == pObj1->pData )
continue;
- if ( Aig_ObjIsNone(pObj0->pData) || Aig_ObjIsNone(pObj1->pData) )
+ if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
continue;
// get the miter nodes
- pObj0 = pObj0->pData;
- pObj1 = pObj1->pData;
+ pObj0 = (Aig_Obj_t *)pObj0->pData;
+ pObj1 = (Aig_Obj_t *)pObj1->pData;
assert( !Aig_IsComplement(pObj0) );
assert( !Aig_IsComplement(pObj1) );
assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
@@ -435,7 +438,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
if ( p->pPars->fPartSigCorr )
p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
else
- p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
if ( p->pPars->fDumpSRInit )
{
if ( p->pPars->fPartSigCorr )
@@ -449,7 +452,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
}
p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
- Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
// cleanup
@@ -591,3 +594,5 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index fb36c31d..7cd94727 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -21,6 +21,9 @@
#include "sswInt.h"
//#include "bar.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -56,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
}
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsPi(pObjFraig) );
- pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
}
}
@@ -106,14 +109,14 @@ 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->pMSat->vUsedPis, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i )
{
nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
assert( nVarNum > 0 );
Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
if ( Value == 0 )
continue;
- pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
Aig_InfoSetBit( pInfo, p->nPatterns );
}
}
@@ -284,7 +287,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
if ( Vec_PtrSize(vClass) == 0 )
continue;
// try to prove equivalences in this class
- Vec_PtrForEachEntry( vClass, pTemp, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pTemp, k )
if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
{
Ssw_ManSweepLatchOne( p, pObj, pTemp );
@@ -329,3 +332,5 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 90cc9028..0f1317e1 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -57,13 +60,12 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
- p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
+ p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
// other
p->vNewLos = Vec_PtrAlloc( 100 );
p->vNewPos = Vec_IntAlloc( 100 );
p->vResimConsts = Vec_PtrAlloc( 100 );
p->vResimClasses = Vec_PtrAlloc( 100 );
-
// p->pPars->fVerbose = 1;
return p;
}
@@ -104,10 +106,10 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
- p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
+ p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), 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),
- 0/p->pPars->nIters );
+ 0/(p->pPars->nIters+1) );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
@@ -127,6 +129,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+
+ // report the reductions
+ if ( p->pAig->nConstrs )
+ {
+ printf( "Statistics reflecting the use of constraints:\n" );
+ printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
+ p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal );
+ printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
+ p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal );
+ printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
+ p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) );
+ }
}
/**Function*************************************************************
@@ -174,7 +189,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
void Ssw_ManStop( Ssw_Man_t * p )
{
ABC_FREE( p->pVisited );
- if ( p->pPars->fVerbose )
+ if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
Ssw_ClassesStop( p->ppClasses );
@@ -182,6 +197,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_SmlStop( p->pSml );
if ( p->vDiffPairs )
Vec_IntFree( p->vDiffPairs );
+ if ( p->vInits )
+ Vec_IntFree( p->vInits );
Vec_PtrFree( p->vResimConsts );
Vec_PtrFree( p->vResimClasses );
Vec_PtrFree( p->vNewLos );
@@ -197,3 +214,5 @@ void Ssw_ManStop( Ssw_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index 3c079922..0aba942f 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -113,8 +116,8 @@ Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_
{
pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) );
pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) );
- pObj1m = Aig_Regular(pObj1->pData);
- pObj2m = Aig_Regular(pObj2->pData);
+ pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData);
+ pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData);
assert( pObj1m && pObj2m );
if ( pObj1m == pObj2m )
continue;
@@ -290,7 +293,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
// create equivalence classes using these IDs
p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
- Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
// cleanup
@@ -326,7 +329,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
Aig_ManForEachObj( pAig, pObj, i )
{
- pRepr = Aig_Regular(pObj->pData);
+ pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData);
if ( pRepr == NULL )
continue;
if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL )
@@ -470,3 +473,5 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
index f481b457..8a0e69da 100644
--- a/src/aig/ssw/sswPart.c
+++ b/src/aig/ssw/sswPart.c
@@ -19,6 +19,10 @@
***********************************************************************/
#include "sswInt.h"
+#include "ioa.h"
+
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -50,16 +54,20 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
int clk = clock();
-
+ if ( pPars->fConstrs )
+ {
+ printf( "Cannot use partitioned computation with constraints.\n" );
+ return NULL;
+ }
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
- fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
+ fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
- Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+ Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
@@ -75,9 +83,9 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
- Vec_PtrForEachEntry( vResult, vPart, i )
+ Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
- extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+// extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
@@ -89,7 +97,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// perform SSW with partitions
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
- Vec_PtrForEachEntry( vResult, vPart, i )
+ Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
Aig_ManSetRegNum( pTemp, pTemp->nRegs );
@@ -129,3 +137,5 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 21c5c1f1..7d371cac 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -50,9 +53,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pOld) );
assert( !Aig_IsComplement(pNew) );
assert( pOld != pNew );
-
-// if ( p->pSat == NULL )
-// Ssw_ManStartSolver( p );
assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them
@@ -199,7 +199,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) );
+ assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
// move constant to the old node
if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
@@ -216,9 +216,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
pOld = Aig_Regular(pOld);
pNew = Aig_Not(pNew);
}
-
-// if ( p->pSat == NULL )
-// Ssw_ManStartSolver( p );
assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them
@@ -274,8 +271,36 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Constrains one node in the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj )
+{
+ int RetValue, Lit;
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) );
+ // add constraint A = 1 ----> A
+ Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_ObjFanin0(pPoObj)->fPhase ) Lit = lit_neg( Lit );
+ }
+ RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 );
+ assert( RetValue );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index 1d578291..dfb2fb0f 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -127,7 +130,7 @@ int Ssw_SemCheckTargets( Ssw_Sem_t * p )
{
Aig_Obj_t * pObj;
int i;
- Vec_PtrForEachEntry( p->vTargets, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
return 1;
return 0;
@@ -153,7 +156,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
return;
Saig_ManForEachLo( p->pMan->pAig, pObj, i )
{
- pInfo = Vec_PtrEntry( p->vPatterns, i );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
Aig_InfoSetBit( pInfo, p->nPatterns );
}
@@ -183,7 +186,7 @@ clk = clock();
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
Saig_ManForEachLo( p->pAig, pObj, i )
{
- pInfo = Vec_PtrEntry( pBmc->vPatterns, i );
+ pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) );
Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
}
@@ -315,3 +318,5 @@ clk = clock();
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index cf5270dd..37bf5717 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -349,7 +352,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
for ( i = 0; i < p->nWordsTotal; i++ )
{
uWord = 0;
- Vec_PtrForEachEntry( vObjs, pObj, k )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, k )
{
pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
@@ -858,7 +861,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
if ( fInit )
{
assert( Aig_ManRegNum(p->pAig) > 0 );
- assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+ assert( Aig_ManRegNum(p->pAig) <= Aig_ManPiNum(p->pAig) );
// assign random info for primary inputs
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlAssignRandom( p, pObj );
@@ -1240,12 +1243,12 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
- pCex = (Ssw_Cex_t *)ABC_ALLOC( char, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords );
- memset( pCex, 0, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords );
+ pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+ memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
pCex->nBits = nRegs + nRealPis * nFrames;
@@ -1263,7 +1266,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
SeeAlso []
***********************************************************************/
-void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex )
+void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex )
{
ABC_FREE( pCex );
}
@@ -1279,11 +1282,15 @@ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex )
SeeAlso []
***********************************************************************/
-int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
+int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
+ if ( Saig_ManPiNum(pAig) != p->nPis )
+ return 0;
+// if ( Saig_ManRegNum(pAig) != p->nRegs )
+// return 0;
// assert( Aig_ManRegNum(pAig) > 0 );
// assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
@@ -1293,10 +1300,11 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
Saig_ManForEachLo( pAig, pObj, i )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
+ iBit = Saig_ManRegNum(pAig);
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
- assert( iBit == p->nBits );
+// assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
@@ -1316,7 +1324,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
+int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
@@ -1359,9 +1367,9 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
+Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
unsigned * pSims;
int iPo, iFrame, iBit, i, k;
@@ -1433,9 +1441,9 @@ Ssw_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
+Abc_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
// get the number of frames
@@ -1493,9 +1501,9 @@ Ssw_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
+Abc_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
int nTruePis, nTruePos, iPo, iFrame;
assert( Aig_ManRegNum(pAig) > 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
@@ -1520,9 +1528,9 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
SeeAlso []
***********************************************************************/
-Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew )
+Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
{
- Ssw_Cex_t * pCex;
+ Abc_Cex_t * pCex;
int i;
pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
pCex->iPo = p->iPo;
@@ -1544,7 +1552,7 @@ Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew )
SeeAlso []
***********************************************************************/
-int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p )
+int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
@@ -1614,3 +1622,5 @@ int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index c85b8bcf..6b18a3a6 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -51,21 +54,25 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
Aig_ManForEachNode( p->pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
- // check equivalence classes
- RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
- RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
- // make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
- {
- assert( RetValue1 );
- if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
- }
- else
+ // if repr is given, perform refinement
+ if ( pRepr )
{
- assert( RetValue2 );
- if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
+ // check equivalence classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
+ // make sure refinement happened
+ if ( Aig_ObjIsConst1(pRepr) )
+ {
+ assert( RetValue1 );
+ if ( RetValue1 == 0 )
+ printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
+ }
+ else
+ {
+ assert( RetValue2 );
+ if ( RetValue2 == 0 )
+ printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
+ }
}
p->timeSimSat += clock() - clk;
}
@@ -112,3 +119,5 @@ p->timeSimSat += clock() - clk;
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index a2f3c175..39fcd48e 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -21,6 +21,9 @@
#include "sswInt.h"
#include "bar.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -157,14 +160,14 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
unsigned * pInfo;
int i, nVarNum;
// iterate through the PIs of the frames
- Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i )
{
assert( Aig_ObjIsPi(pObj) );
nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
assert( nVarNum > 0 );
if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
{
- pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
Aig_InfoSetBit( pInfo, p->nPatterns );
}
}
@@ -232,34 +235,7 @@ p->timeMarkCones += clock() - clk;
}
else
Ssw_SmlSavePatternAig( p, f );
- // consider uniqueness
- if ( !fBmc && !p->pPars->fDynamic && p->pPars->fUniqueness && p->pPars->nFramesK > 1 &&
- Ssw_ManUniqueOne( p, pObjRepr, pObj, p->pPars->fVerbose ) && p->iOutputLit == -1 )
- {
- 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, p->pPars->fVerbose );
- 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 )
+ if ( !p->pPars->fConstrs )
Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
Ssw_ManResimulateBit( p, pObj, pObjRepr );
@@ -298,7 +274,6 @@ clk = clock();
p->fRefined = 0;
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
-// Ssw_ManStartSolver( p );
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
@@ -318,10 +293,12 @@ clk = clock();
if ( f == p->pPars->nFramesK - 1 )
break;
// transfer latch input to the latch outputs
+ Aig_ManForEachPo( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
- pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
+ pObjNew = Ssw_ObjFrame( p, pObjLi, f );
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
}
@@ -350,7 +327,7 @@ int Ssw_ManSweep( Ssw_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
- int nConstrPairs, clk, i, f, v;
+ int nConstrPairs, clk, i, f;
// perform speculative reduction
clk = clock();
@@ -380,12 +357,6 @@ clk = clock();
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
p->timeReduce += clock() - clk;
- // bring up the previous frames
- if ( p->pPars->fUniqueness )
- for ( v = 0; v < f; v++ )
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
-
// sweep internal nodes
p->fRefined = 0;
Ssw_ClassesClearRefined( p->ppClasses );
@@ -417,3 +388,5 @@ p->timeReduce += clock() - clk;
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
index d6590716..b5f6a853 100644
--- a/src/aig/ssw/sswUnique.c
+++ b/src/aig/ssw/sswUnique.c
@@ -20,6 +20,9 @@
#include "sswInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -100,7 +103,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
RetValue = Vec_PtrSize( p->vCommon );
fFeasible = 0;
k = 0;
- Vec_PtrForEachEntry( p->vCommon, pTemp, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
{
assert( Aig_ObjIsPi(pTemp) );
if ( !Saig_ObjIsLo(p->pAig, pTemp) )
@@ -119,7 +122,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
// check the current values
RetValue = 1;
- Vec_PtrForEachEntry( p->vCommon, pTemp, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
{
Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
@@ -153,7 +156,7 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
assert( Vec_PtrSize(vCommon) > 0 );
// generate the constraint
pTotal = Aig_ManConst0(p->pFrames);
- Vec_PtrForEachEntry( vCommon, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vCommon, pObj, i )
{
assert( Saig_ObjIsLo(p->pAig, pObj) );
pObj1New = Ssw_ObjFrame( p, pObj, f1 );
@@ -190,3 +193,5 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 16:53:30 +0000