summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h2
-rw-r--r--src/aig/aig/aigDfs.c49
-rw-r--r--src/aig/aig/aigPartReg.c36
-rw-r--r--src/aig/fra/fra.h4
-rw-r--r--src/aig/fra/fraCec.c16
-rw-r--r--src/aig/fra/fraInd.c38
-rw-r--r--src/aig/fra/fraSec.c2
-rw-r--r--src/aig/ntl/ntlFraig.c37
-rw-r--r--src/aig/ssw/module.make1
-rw-r--r--src/aig/ssw/ssw.h5
-rw-r--r--src/aig/ssw/sswClass.c55
-rw-r--r--src/aig/ssw/sswCore.c41
-rw-r--r--src/aig/ssw/sswInt.h10
-rw-r--r--src/aig/ssw/sswMan.c30
-rw-r--r--src/aig/ssw/sswPart.c129
-rw-r--r--src/aig/ssw/sswSimSat.c26
-rw-r--r--src/aig/ssw/sswSweep.c191
17 files changed, 529 insertions, 143 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 03c05420..093912c3 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -470,6 +470,7 @@ extern int Aig_ManLevelNum( Aig_Man_t * p );
extern int Aig_ManChoiceLevel( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
@@ -562,6 +563,7 @@ extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize,
extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
/*=== aigPartReg.c =========================================================*/
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
+extern void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
extern Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index c9893ed2..3c6658d9 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -685,6 +685,55 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Counts the support size of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_Support_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
+{
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_PtrPush( vSupp, pObj );
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+ Aig_Support_rec( p, Aig_ObjFanin0(pObj), vSupp );
+ if ( Aig_ObjFanin1(pObj) )
+ Aig_Support_rec( p, Aig_ObjFanin1(pObj), vSupp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the support size of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Vec_Ptr_t * vSupp;
+ assert( !Aig_IsComplement(pObj) );
+ assert( !Aig_ObjIsPo(pObj) );
+ Aig_ManIncrementTravId( p );
+ vSupp = Vec_PtrAlloc( 100 );
+ Aig_Support_rec( p, pObj, vSupp );
+ return vSupp;
+}
+
+/**Function*************************************************************
+
Synopsis [Transfers the AIG from one manager into another.]
Description []
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 6baeae31..36be0810 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -498,6 +498,42 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOve
/**Function*************************************************************
+ Synopsis [Divides a large partition into several ones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
+{
+ Vec_Int_t * vPart;
+ int i, Counter;
+ assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
+ if ( nOverSize >= nPartSize )
+ {
+ printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
+ printf( "Adjusting it to be equal to half of the partition size.\n" );
+ nOverSize = nPartSize/2;
+ }
+ assert( nOverSize < nPartSize );
+ for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
+ {
+ vPart = Vec_IntAlloc( nPartSize );
+ for ( i = 0; i < nPartSize; i++, Counter++ )
+ if ( Counter < Vec_IntSize(vDomain) )
+ Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
+ if ( Vec_IntSize(vPart) <= nOverSize )
+ Vec_IntFree(vPart);
+ else
+ Vec_PtrPush( vResult, vPart );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Computes partitioning of registers.]
Description []
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 6721634e..91689196 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -283,8 +283,8 @@ static inline int Fra_ImpCreate( int Left, int Right )
/*=== fraCec.c ========================================================*/
extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
-extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
+extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
+extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 9046d574..fdf87ccd 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -157,11 +157,11 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
SeeAlso []
***********************************************************************/
-int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
+int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
{
- int nBTLimitStart = 300; // starting SAT run
- int nBTLimitFirst = 2; // first fraiging iteration
- int nBTLimitLast = 1000000; // the last-gasp SAT run
+ int nBTLimitStart = 300; // starting SAT run
+ int nBTLimitFirst = 2; // first fraiging iteration
+ int nBTLimitLast = nConfLimit; // the last-gasp SAT run
Fra_Par_t Params, * pParams = &Params;
Aig_Man_t * pAig = *ppAig, * pTemp;
@@ -270,7 +270,7 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
{
Aig_Man_t * pAig;
Vec_Ptr_t * vParts;
@@ -294,7 +294,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
continue;
if ( RetValue == 0 )
break;
- RetValue = Fra_FraigCec( &pAig, 0 );
+ RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
Vec_PtrWriteEntry( vParts, i, pAig );
if ( RetValue == 1 )
continue;
@@ -361,9 +361,9 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
if ( nPartSize )
- RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+ RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
else // no partitioning
- RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
+ RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
// report the miter
if ( RetValue == 1 )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ce9ec69b..f7674f7d 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -233,42 +233,6 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
free( pLatches );
}
-/**Function*************************************************************
-
- Synopsis [Divides a large partition into several ones.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Fra_FraigInductionPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
-{
- Vec_Int_t * vPart;
- int i, Counter;
- assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
- if ( nOverSize >= nPartSize )
- {
- printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
- printf( "Adjusting it to be equal to half of the partition size.\n" );
- nOverSize = nPartSize/2;
- }
- assert( nOverSize < nPartSize );
- for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
- {
- vPart = Vec_IntAlloc( nPartSize );
- for ( i = 0; i < nPartSize; i++, Counter++ )
- if ( Counter < Vec_IntSize(vDomain) )
- Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
- if ( Vec_IntSize(vPart) <= nOverSize )
- Vec_IntFree(vPart);
- else
- Vec_PtrPush( vResult, vPart );
- }
-}
-
/**Function*************************************************************
@@ -304,7 +268,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
- Fra_FraigInductionPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+ Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 5944cf56..b8f767df 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -230,7 +230,7 @@ PRT( "Time", clock() - clk );
}
if ( pNew->nRegs == 0 )
- RetValue = Fra_FraigCec( &pNew, 0 );
+ RetValue = Fra_FraigCec( &pNew, 100000, 0 );
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue >= 0 )
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 0a991fff..b1239e47 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -20,6 +20,7 @@
#include "ntl.h"
#include "fra.h"
+#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -494,7 +495,43 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Returns AIG with WB after fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
+{
+ Ntl_Man_t * pNew, * pAux;
+ Aig_Man_t * pAig, * pAigCol, * pTemp;
+
+ // collapse the AIG
+ pAig = Ntl_ManExtract( p );
+ pNew = Ntl_ManInsertAig( p, pAig );
+ pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+ if ( pAigCol == NULL )
+ {
+ Aig_ManStop( pAig );
+ return pNew;
+ }
+ // perform SCL for the given design
+ pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
+ Aig_ManStop( pTemp );
+
+ // finalize the transformation
+ pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
+ Ntl_ManFree( pAux );
+ Aig_ManStop( pAig );
+ Aig_ManStop( pAigCol );
+ return pNew;
+}
/**Function*************************************************************
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 2619751e..b176d4db 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -3,6 +3,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswMan.c \
+ src/aig/ssw/sswPart.c \
src/aig/ssw/sswSat.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index aaaa6407..f76664ec 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -44,11 +44,14 @@ struct Ssw_Pars_t_
int nPartSize; // size of the partition
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 nMaxLevs; // the max number of levels of nodes to consider
int nBTLimit; // conflict limit at a node
+ int nMinDomSize; // min clock domain considered for optimization
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
+ int fSkipCheck; // does not run equivalence check for unaffected cones
int fVerbose; // verbose stats
// internal parameters
int nIters; // the number of iterations performed
@@ -77,6 +80,8 @@ struct Ssw_Cex_t_
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+/*=== sswPart.c ==========================================================*/
+extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
#ifdef __cplusplus
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 66b86009..d06cce49 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -46,6 +46,7 @@ struct Ssw_Cla_t_
// temporary data
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
+ Vec_Ptr_t * vRefined; // the nodes refined since the last iteration
// procedures used for class refinement
void * pManData;
unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
@@ -141,6 +142,7 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(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) );
return p;
@@ -183,6 +185,7 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
{
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
+ Vec_PtrFree( p->vRefined );
FREE( p->pId2Class );
FREE( p->pClassSizes );
FREE( p->pMemClasses );
@@ -191,6 +194,38 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
+{
+ return p->vRefined;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
+{
+ Vec_PtrClear( p->vRefined );
+}
+
+/**Function*************************************************************
+
Synopsis [Stop representation of equivalence classes.]
Description []
@@ -368,12 +403,14 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
+ Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
Aig_ObjSetRepr( p->pAig, pObj, NULL );
p->nCands1--;
return;
}
+ Vec_PtrPush( p->vRefined, pRepr );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
assert( p->pId2Class[pRepr->Id][0] == pRepr );
assert( p->pClassSizes[pRepr->Id] >= 2 );
@@ -409,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
{
Ssw_Cla_t * p;
Ssw_Sml_t * pSml;
@@ -424,7 +461,10 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
// perform sequential simulation
clk = clock();
pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 4 );
+if ( fVerbose )
+{
PRT( "Simulation of 32 frames with 4 words", clock() - clk );
+}
// set comparison procedures
clk = clock();
@@ -441,7 +481,7 @@ clk = clock();
{
if ( fLatchCorr )
{
- if ( !Saig_ObjIsPi(p->pAig, pObj) )
+ if ( !Saig_ObjIsLo(p->pAig, pObj) )
continue;
}
else
@@ -521,7 +561,10 @@ clk = clock();
Ssw_ClassesCheck( p );
Ssw_SmlStop( pSml );
// Ssw_ClassesPrint( p, 0 );
+if ( fVerbose )
+{
PRT( "Collecting candidate equival classes", clock() - clk );
+}
return p;
}
@@ -597,8 +640,6 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
}
// allocate room for classes
p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
- // set comparison procedures
- Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
// Ssw_ClassesPrint( p, 0 );
return p;
}
@@ -631,6 +672,9 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
// check if splitting happened
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
+ // remember that this class is refined
+ Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+ Vec_PtrPush( p->vRefined, pObj );
// get the new representative
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@@ -751,7 +795,10 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
{
pObj = Aig_ManObj( p->pAig, i );
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+ {
Vec_PtrPush( p->vClassNew, pObj );
+ Vec_PtrPush( p->vRefined, pObj );
+ }
}
// check if there is a new class
if ( Vec_PtrSize(p->vClassNew) == 0 )
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 409a1ebe..e6096c54 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,8 +45,10 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nPartSize = 0; // size of the partition
p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth
+ p->nFramesAddSim = 2; // additional frames to simulate
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
+ p->nMinDomSize = 100; // min clock domain considered for optimization
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
p->fVerbose = 0; // verbose stats
@@ -71,21 +73,44 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
int RetValue, nIter, clk, clkTotal = clock();
// reset random numbers
Aig_ManRandom( 1 );
+
+ // consider the case of empty AIG
+ if ( Aig_ManNodeNum(pAig) == 0 )
+ {
+ pPars->nIters = 0;
+ // Ntl_ManFinalize() needs the following to satisfy an assertion
+ Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
+ return Aig_ManDupOrdered(pAig);
+ }
+
+ // check and update parameters
+ assert( Aig_ManRegNum(pAig) > 0 );
+ assert( pPars->nFramesK > 0 );
+ if ( pPars->nFramesK > 1 )
+ pPars->fSkipCheck = 0;
+
+ // perform partitioning
+ if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+ || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
+ return Ssw_SignalCorrespondencePart( pAig, pPars );
+
// start the choicing manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes
+// p->pPars->nConstrs = 1;
if ( p->pPars->nConstrs == 0 )
{
- p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
- p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 );
+ // perform one round of seq simulation and generate candidate equivalence classes
+ p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
}
else
{
- assert( 0 );
+ // 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_NodeIsConstCex, Ssw_NodesAreEqualCex );
}
-// Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
// get the starting stats
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
@@ -111,9 +136,11 @@ clk = clock();
RetValue = Ssw_ManSweep( p );
if ( pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ",
+ printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
- p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+ p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+ printf( "Use = %5d. Skip = %5d. ",
+ p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk );
}
Ssw_ManCleanup( p );
@@ -133,6 +160,8 @@ p->timeTotal = clock() - clkTotal;
return pAigNew;
}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 009c09c4..c9dd1958 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -57,6 +57,8 @@ struct Ssw_Man_t_
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
+ int nRefUse;
+ int nRefSkip;
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
@@ -77,8 +79,8 @@ struct Ssw_Man_t_
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
- int nSatFails; // the number of timeouts
int nSatFailsReal; // the number of timeouts
+ int nSatFailsTotal; // the number of timeouts
int nSatCallsUnsat; // the number of unsat SAT calls
int nSatCallsSat; // the number of sat SAT calls
// node/register/lit statistics
@@ -91,6 +93,7 @@ struct Ssw_Man_t_
// runtime stats
int timeBmc; // bounded model checking
int timeReduce; // speculative reduction
+ int timeMarkCones; // marking the cones not to be refined
int timeSimSat; // simulation of the counter-examples
int timeSat; // solving SAT
int timeSatSat; // sat
@@ -136,6 +139,8 @@ extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void Ssw_ClassesStop( Ssw_Cla_t * p );
+extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p );
+extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
@@ -143,7 +148,7 @@ extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int
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 fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
@@ -171,6 +176,7 @@ extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
+extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index a6e02125..f25cee45 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -99,27 +99,28 @@ 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: Frames = %d. Conf limit = %d. Constrs = %d. Max lev = %d. Mem = %0.2f Mb.\n",
- p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
+ printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
+ p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
p->nSatVarsTotal/p->pPars->nIters );
- printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Equivs = %d. Str = %d.\n",
- p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStrangers );
+ printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n",
+ p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
- p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
- PRTP( "BMC ", p->timeBmc, p->timeTotal );
- PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
- PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
- PRTP( "SAT solving", p->timeSat, p->timeTotal );
- PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
- PRTP( " sat ", p->timeSatSat, p->timeTotal );
- PRTP( " undecided", p->timeSatUndec, p->timeTotal );
- PRTP( "Other ", p->timeOther, p->timeTotal );
- PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+ p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
+ PRTP( "BMC ", p->timeBmc, p->timeTotal );
+ PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
+ PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
+ PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
+ PRTP( "SAT solving", p->timeSat, p->timeTotal );
+ PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
+ PRTP( " sat ", p->timeSatSat, p->timeTotal );
+ PRTP( " undecided", p->timeSatUndec, p->timeTotal );
+ PRTP( "Other ", p->timeOther, p->timeTotal );
+ PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
/**Function*************************************************************
@@ -167,6 +168,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManStop( Ssw_Man_t * p )
{
+ Aig_ManCleanMarkA( p->pAig );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
new file mode 100644
index 00000000..7eb6b8fe
--- /dev/null
+++ b/src/aig/ssw/sswPart.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+ FileName [sswPart.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Partitioned signal correspondence.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs partitioned sequential SAT sweepingG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+ int fPrintParts = 0;
+ char Buffer[100];
+ Aig_Man_t * pTemp, * pNew;
+ Vec_Ptr_t * vResult;
+ Vec_Int_t * vPart;
+ int * pMapBack;
+ int i, nCountPis, nCountRegs;
+ int nClasses, nPartSize, fVerbose;
+ int clk = clock();
+
+ // save parameters
+ nPartSize = pPars->nPartSize; pPars->nPartSize = 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 )
+ {
+ if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
+ Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+ else
+ Vec_PtrPush( vResult, Vec_IntDup(vPart) );
+ }
+ }
+ else
+ vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
+// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+ if ( fPrintParts )
+ {
+ // print partitions
+ printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+ Vec_PtrForEachEntry( vResult, vPart, i )
+ {
+ 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 );
+ printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
+ i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+ Aig_ManStop( pTemp );
+ }
+ }
+
+ // perform SSW with partitions
+ Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+ Vec_PtrForEachEntry( vResult, vPart, i )
+ {
+ pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+ Aig_ManSetRegNum( pTemp, pTemp->nRegs );
+ // create the projection of 1-hot registers
+ if ( pAig->vOnehots )
+ pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
+ // run SSW
+ pNew = Ssw_SignalCorrespondence( pTemp, pPars );
+ nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+ if ( fVerbose )
+ printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
+ i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+ Aig_ManStop( pNew );
+ Aig_ManStop( pTemp );
+ free( pMapBack );
+ }
+ // remap the AIG
+ pNew = Aig_ManDupRepr( pAig, 0 );
+ Aig_ManSeqCleanup( pNew );
+// Aig_ManPrintStats( pAig );
+// Aig_ManPrintStats( pNew );
+ Vec_VecFree( (Vec_Vec_t *)vResult );
+ pPars->nPartSize = nPartSize;
+ pPars->fVerbose = fVerbose;
+ if ( fVerbose )
+ {
+ PRT( "Total time", clock() - clk );
+ }
+ return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 547755f0..6ef5ec20 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -234,7 +234,8 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
// set the PI simulation information
Aig_ManConst1(p->pAig)->fMarkB = 1;
Aig_ManForEachPi( p->pAig, pObj, i )
- pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+// pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+ pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
// simulate internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
@@ -253,27 +254,6 @@ p->timeSimSat += clock() - clk;
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
-{
- Aig_Obj_t * pObj;
- int i;
- memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
- Aig_InfoSetBit( p->pPatWords, i );
-}
-
-/**Function*************************************************************
-
Synopsis [Handle the counter-example.]
Description []
@@ -287,7 +267,7 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
{
int RetValue1, RetValue2, clk = clock();
// save the counter-example
- Ssw_SmlSavePatternAig( p, f );
+// Ssw_SmlSavePatternAig( p, f );
// set the PI simulation information
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
// simulate internal nodes
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 7c99fad2..5ad6d78e 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -31,6 +31,95 @@
/**Function*************************************************************
+ Synopsis [Mark nodes affected by sweep in the previous iteration.]
+
+ Description [Assumes that affected nodes are in p->ppClasses->vRefined.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
+{
+ Vec_Ptr_t * vRefined, * vSupp;
+ Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+ int i, k;
+ vRefined = Ssw_ClassesGetRefined( p->ppClasses );
+ if ( Vec_PtrSize(vRefined) == 0 )
+ {
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ pObj->fMarkA = 1;
+ return;
+ }
+ // mark the nodes to be refined
+ Aig_ManCleanMarkA( p->pAig );
+ Vec_PtrForEachEntry( vRefined, pObj, i )
+ {
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ pObj->fMarkA = 1;
+ continue;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ vSupp = Aig_Support( p->pAig, pObj );
+ Vec_PtrForEachEntry( vSupp, pObjLo, k )
+ pObjLo->fMarkA = 1;
+ Vec_PtrFree( vSupp );
+ }
+ // mark refinement
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA;
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ pObjLo->fMarkA |= pObjLi->fMarkA;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
+ Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+ Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
@@ -40,7 +129,7 @@
SeeAlso []
***********************************************************************/
-void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
@@ -50,59 +139,58 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
// get the fraiged node
pObjFraig = Ssw_ObjFraig( p, pObj, f );
- assert( pObjFraig != NULL );
// get the fraiged representative
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
- assert( pObjReprFraig != NULL );
// check if constant 0 pattern distinquishes these nodes
+ assert( pObjFraig != NULL && pObjReprFraig != NULL );
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
{
- Aig_Obj_t * pObj;
- int i;
- if ( p->pSat->model.cap < p->pSat->size )
- {
- veci_resize(&p->pSat->model, 0);
- for ( i = 0; i < p->pSat->size; i++ )
- veci_push( &p->pSat->model, (int)l_False );
- }
- // set the values of SAT vars to be equal to the phase of the nodes
- Aig_ManForEachObj( p->pFrames, pObj, i )
- if ( Ssw_ObjSatNum( p, pObj ) )
- {
- int iVar = Ssw_ObjSatNum( p, pObj );
- assert( iVar < p->pSat->size );
- p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
- p->pSat->model.size = p->pSat->size;
- }
p->nStrangers++;
- return;
+ Ssw_SmlSavePatternAigPhase( p, f );
}
- // if the fraiged nodes are the same, return
- if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
- return;
-// assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
- if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
- RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
else
- RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
-
- if ( RetValue == -1 ) // timed out
- {
-// assert( 0 );
- Ssw_ClassesRemoveNode( p->ppClasses, pObj );
- p->fRefined = 1;
- return;
- }
- if ( RetValue == 1 ) // proved equivalent
{
- pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
- Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
- return;
+ // if the fraiged nodes are the same, return
+ if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+ return;
+ // count the number of skipped calls
+ if ( !pObj->fMarkA && !pObjRepr->fMarkA )
+ p->nRefSkip++;
+ else
+ p->nRefUse++;
+ // call equivalence checking
+ if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+ RetValue = 1;
+ else if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
+ 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_ObjSetFraig( p, pObj, f, pObjFraig2 );
+ return;
+ }
+ if ( RetValue == -1 ) // timed out
+ {
+ Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+ p->fRefined = 1;
+ return;
+ }
+ // check if skipping calls works correctly
+ if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+ {
+ assert( 0 );
+ printf( "\nMistake!!!\n" );
+ }
+ // disproved the equivalence
+ Ssw_SmlSavePatternAig( p, f );
}
- // disproved the equivalence
// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
-// Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
- Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+ if ( p->pPars->nConstrs == 0 )
+ Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+ else
+ Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
@@ -147,7 +235,7 @@ clk = clock();
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_ObjSetFraig( p, pObj, f, pObjNew );
- Ssw_ManSweepNode( p, pObj, f );
+ Ssw_ManSweepNode( p, pObj, f, 1 );
}
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
@@ -205,6 +293,12 @@ clk = clock();
sat_solver_simplify( p->pSat );
p->timeReduce += clock() - clk;
+ // mark nodes that do not have to be refined
+clk = clock();
+ if ( p->pPars->fSkipCheck )
+ Ssw_ManSweepMarkRefinement( p );
+p->timeMarkCones += clock() - clk;
+
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
@@ -215,6 +309,9 @@ p->timeReduce += clock() - clk;
assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
+ p->nSatFailsReal = 0;
+ p->nRefUse = p->nRefSkip = 0;
+ Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
@@ -222,14 +319,16 @@ p->timeReduce += clock() - clk;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
- Ssw_ManSweepNode( p, pObj, f );
+ Ssw_ManSweepNode( p, pObj, f, 0 );
else if ( Aig_ObjIsNode(pObj) )
{
+ pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
- Ssw_ManSweepNode( p, pObj, f );
+ Ssw_ManSweepNode( p, pObj, f, 0 );
}
}
+ p->nSatFailsTotal += p->nSatFailsReal;
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-24 00:34:41 +0000