summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/module.make1
-rw-r--r--src/aig/ssw/ssw.h6
-rw-r--r--src/aig/ssw/sswClass.c47
-rw-r--r--src/aig/ssw/sswCnf.c2
-rw-r--r--src/aig/ssw/sswCore.c50
-rw-r--r--src/aig/ssw/sswDyn.c384
-rw-r--r--src/aig/ssw/sswInt.h23
-rw-r--r--src/aig/ssw/sswLcorr.c3
-rw-r--r--src/aig/ssw/sswMan.c18
-rw-r--r--src/aig/ssw/sswSat.c5
-rw-r--r--src/aig/ssw/sswSemi.c5
-rw-r--r--src/aig/ssw/sswSim.c173
-rw-r--r--src/aig/ssw/sswSweep.c221
-rw-r--r--src/aig/ssw/sswUnique.c35
14 files changed, 772 insertions, 201 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 915f7dd0..a7d940b4 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/sswClass.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
+ src/aig/ssw/sswDyn.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 2d067a17..73226dbe 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -17,7 +17,7 @@
Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#ifndef __SSW_H__
#define __SSW_H__
@@ -55,12 +55,16 @@ struct Ssw_Pars_t_
int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints
+ int fDynamic; // enable dynamic addition of constraints
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
+ // optimized signal correspondence
+ int nSatVarMax2; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
+ int nRecycleCalls2;// calls to perform before recycling SAT solver (optimized latch corr only)
// internal parameters
int nIters; // the number of iterations performed
int nConflicts; // the total number of conflicts performed
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index cfbb138c..f234a58f 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -493,11 +493,22 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
***********************************************************************/
Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
{
+// int nFrames = 4;
+// int nWords = 1;
+// int nIters = 16;
+
+// int nFrames = 32;
+// int nWords = 4;
+// int nIters = 0;
+
+ int nFrames = 4;
+ int nWords = 2;
+ int nIters = 16;
Ssw_Cla_t * p;
Ssw_Sml_t * pSml;
Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
Aig_Obj_t * pObj, * pTemp, * pRepr;
- int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
+ int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2, RetValue;
int clk;
// start the classes
@@ -505,10 +516,13 @@ 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 );
+ pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
-PRT( "Simulation of 32 frames with 4 words", clock() - clk );
+ printf( "Allocated %.2f Mb for simulation information.\n",
+ 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
+ printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords );
+ PRT( "Time", clock() - clk );
}
// set comparison procedures
@@ -603,13 +617,36 @@ clk = clock();
// now it is time to refine the classes
Ssw_ClassesRefine( p, 1 );
+if ( fVerbose )
+{
+ printf( "Collecting candidate equivalence classes. " );
+PRT( "Time", clock() - clk );
+}
+
+clk = clock();
+ // perform iterative refinement using simulation
+ k = 0;
+ for ( i = 1; i < nIters; i++ )
+ {
+ Ssw_SmlResimulateSeq( pSml );
+ // simulate internal nodes
+ Ssw_SmlSimulateOne( pSml );
+ // check equivalence classes
+ RetValue = Ssw_ClassesRefineConst1( p, 1 );
+ RetValue += Ssw_ClassesRefine( p, 1 );
+ k++;
+ if ( RetValue == 0 )
+ break;
+ }
Ssw_ClassesCheck( p );
Ssw_SmlStop( pSml );
-// Ssw_ClassesPrint( p, 0 );
if ( fVerbose )
{
-PRT( "Collecting candidate equival classes", clock() - clk );
+ printf( "Simulation of %d frames with %d words (%2d rounds). ",
+ nFrames, nWords, k );
+ PRT( "Time", clock() - clk );
}
+// Ssw_ClassesPrint( p, 0 );
return p;
}
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index d068bb78..c5ea9b28 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -77,6 +77,8 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
***********************************************************************/
void Ssw_SatStop( Ssw_Sat_t * p )
{
+// printf( "Recycling SAT solver with %d vars and %d restarts.\n",
+// p->pSat->size, p->pSat->stats.starts );
if ( p->pSat )
sat_solver_delete( p->pSat );
Vec_IntFree( p->vSatVars );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 39f4c736..6db8cc3a 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -60,6 +60,9 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 1000; // the max number of SAT variables
p->nRecycleCalls = 50; // calls to perform before recycling SAT solver
+ // signal correspondence
+ p->nSatVarMax2 = 5000; // the max number of SAT variables
+ p->nRecycleCalls2 = 250; // calls to perform before recycling SAT solver
// return values
p->nIters = 0; // the number of iterations performed
}
@@ -95,7 +98,7 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
- int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal;
+ int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
Aig_Man_t * pAigNew;
int RetValue, nIter;
int clk, clkTotal = clock();
@@ -137,7 +140,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
}
*/
// refine classes using induction
- nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
+ nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
for ( nIter = 0; ; nIter++ )
{
clk = clock();
@@ -147,29 +150,44 @@ clk = clock();
RetValue = Ssw_ManSweepLatch( p );
if ( p->pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ",
+ printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
PRT( "T", clock() - clk );
- nSatProof = p->nSatProof;
- nSatCallsSat = p->nSatCallsSat;
- nRecycles = p->nRecycles;
- nSatFailsReal = p->nSatFailsReal;
}
}
else
{
- RetValue = Ssw_ManSweep( p );
+ 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 : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ",
+ 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), p->nUniques, p->nSatFailsReal );
+ p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+ if ( p->pPars->fUniqueness )
+ printf( "U =%4d. ", p->nUniques-nUniques );
+ else if ( p->pPars->fDynamic )
+ {
+ printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
+ printf( "R =%3d. ", p->nRecycles-nRecycles );
+ }
+ printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal );
PRT( "T", clock() - clk );
}
}
+ nSatProof = p->nSatProof;
+ nSatCallsSat = p->nSatCallsSat;
+ nRecycles = p->nRecycles;
+ nSatFailsReal = p->nSatFailsReal;
+ nUniques = p->nUniques;
+
+ p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );
@@ -234,13 +252,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
pPars->nFramesAddSim = 0;
if ( pPars->nFramesK != 2 )
- printf( "Setting K = 2 for uniqueness constaints to work.\n" );
+ printf( "Setting K = 2 for uniqueness constraints to work.\n" );
pPars->nFramesK = 2;
}
if ( pPars->fLatchCorrOpt )
{
pPars->fLatchCorr = 1;
- pPars->nFramesAddSim = 0;
}
else
{
@@ -259,7 +276,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// perform one round of seq simulation and generate candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
// p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
- p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
+ if ( pPars->fLatchCorrOpt )
+ p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
+ else if ( pPars->fDynamic )
+ 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
@@ -271,7 +293,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
if ( pPars->fUniqueness )
- printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n",
+ printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n",
p->nUniquesAdded, p->nUniquesUseful );
// cleanup
Ssw_ManStop( p );
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
new file mode 100644
index 00000000..d5559408
--- /dev/null
+++ b/src/aig/ssw/sswDyn.c
@@ -0,0 +1,384 @@
+/**CFile****************************************************************
+
+ FileName [sswDyn.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Dynamic loading of constraints.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "bar.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Label PIs nodes of the frames corresponding to PIs of AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObjFrames;
+ int f, i;
+ Aig_ManConst1( p->pFrames )->fMarkA = 1;
+ Aig_ManConst1( p->pFrames )->fMarkB = 1;
+ for ( f = 0; f < p->nFrames; f++ )
+ {
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjFrames = Ssw_ObjFrame( p, pObj, f );
+ assert( Aig_ObjIsPi(pObjFrames) );
+ assert( pObjFrames->fMarkB == 0 );
+ pObjFrames->fMarkA = 1;
+ pObjFrames->fMarkB = 1;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects new POs in p->vNewPos.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
+{
+ assert( !Aig_IsComplement(pObj) );
+ if ( pObj->fMarkA )
+ return;
+ pObj->fMarkA = 1;
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_PtrPush( vNewPis, pObj );
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
+ Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects new POs in p->vNewPos.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
+{
+ Aig_Obj_t * pFanout;
+ int iFanout = -1, i;
+ assert( !Aig_IsComplement(pObj) );
+ if ( pObj->fMarkB )
+ return;
+ pObj->fMarkB = 1;
+ if ( pObj->Id > p->nSRMiterMaxId )
+ return;
+ if ( Aig_ObjIsPo(pObj) )
+ {
+ // skip if it is a register input PO
+ if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+ return;
+ // add the number of this constraint
+ Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
+ return;
+ }
+ // visit the fanouts
+ assert( p->pFrames->pFanData != NULL );
+ Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
+ Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Loads logic cones and relevant constraints.]
+
+ Description [Both pRepr and pObj are objects of the AIG.
+ The result is the current SAT solver loaded with the logic cones
+ for pRepr and pObj corresponding to them in the frames,
+ as well as all the relevant constraints.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pObjFrames, * pReprFrames;
+ Aig_Obj_t * pTemp, * pObj0, * pObj1;
+ int i, iConstr, RetValue;
+
+ assert( pRepr != pObj );
+ // get the corresponding frames nodes
+ pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
+ pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
+ assert( pReprFrames != pObjFrames );
+ /*
+ // compute the AIG support
+ Vec_PtrClear( p->vNewLos );
+ Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
+ Ssw_ManCollectPis_rec( pObj, p->vNewLos );
+ // add logic cones for register outputs
+ Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+ {
+ pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
+ }
+*/
+ // add cones for the nodes
+ Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
+ Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
+
+ // compute the frames support
+ Vec_PtrClear( p->vNewLos );
+ Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
+ Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos );
+ // these nodes include both nodes corresponding to PIs and LOs
+ // (the nodes corresponding to PIs should be labeled with fMarkB!)
+
+ // collect the related constraint POs
+ Vec_IntClear( p->vNewPos );
+ Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+ Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
+ // check if the corresponding pairs are added
+ Vec_IntForEachEntry( p->vNewPos, iConstr, i )
+ {
+ pObj0 = Aig_ManPo( p->pFrames, 2*iConstr );
+ pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
+// if ( pObj0->fMarkB && pObj1->fMarkB )
+ if ( pObj0->fMarkB || pObj1->fMarkB )
+ {
+ pObj0->fMarkB = 1;
+ pObj1->fMarkB = 1;
+ Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
+ }
+ }
+ if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
+ {
+ RetValue = sat_solver_simplify(p->pMSat->pSat);
+ assert( RetValue != 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tranfers simulation information from FRAIG to AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObjFraig;
+ unsigned * pInfo;
+ int i, f, nFrames;
+
+ // transfer simulation information
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
+ if ( pObjFraig == Aig_ManConst0(p->pFrames) )
+ {
+ Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
+ continue;
+ }
+ assert( !Aig_IsComplement(pObjFraig) );
+ assert( Aig_ObjIsPi(pObjFraig) );
+ pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
+ }
+ // set random simulation info for the second frame
+ for ( f = 1; f < p->nFrames; f++ )
+ {
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ {
+ pObjFraig = Ssw_ObjFrame( p, pObj, f );
+ assert( !Aig_IsComplement(pObjFraig) );
+ assert( Aig_ObjIsPi(pObjFraig) );
+ pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
+ }
+ }
+ // create random info
+ nFrames = Ssw_SmlNumFrames( p->pSml );
+ for ( ; f < nFrames; f++ )
+ {
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of simulation with counter-examples.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
+{
+ int RetValue1, RetValue2, clk = clock();
+ // transfer PI simulation information from storage
+// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
+ Ssw_ManSweepTransferDyn( p );
+ // simulate internal nodes
+// Ssw_SmlSimulateOneFrame( p->pSml );
+ Ssw_SmlSimulateOne( p->pSml );
+ // check equivalence classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+ // prepare simulation info for the next round
+ Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+ p->nPatterns = 0;
+ p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+ return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepDyn( Ssw_Man_t * p )
+{
+ Bar_Progress_t * pProgress = NULL;
+ Aig_Obj_t * pObj, * pObjNew;
+ int clk, i, f;
+
+ // perform speculative reduction
+clk = clock();
+ // create timeframes
+ p->pFrames = Ssw_FramesWithClasses( p );
+ Aig_ManFanoutStart( p->pFrames );
+ p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );
+
+ // map constants and PIs of the last frame
+ f = p->pPars->nFramesK;
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ Aig_ManSetPioNumbers( p->pFrames );
+ // label nodes corresponding to primary inputs
+ Ssw_ManLabelPiNodes( p );
+p->timeReduce += clock() - clk;
+
+ // prepare simulation info
+ assert( p->vSimInfo == NULL );
+ p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+ Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+
+ // 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_ManSweepNode( 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_ManSweepNode( p, pObj, f, 0 );
+ }
+ // check if it is time to recycle the solver
+ if ( p->pMSat->pSat == NULL ||
+ (p->pPars->nSatVarMax2 &&
+ p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
+ p->nRecycleCalls > p->pPars->nRecycleCalls2) )
+ {
+ // resimulate
+ if ( p->nPatterns > 0 )
+ Ssw_ManSweepResimulateDyn( p, f );
+// printf( "Recycling SAT solver with %d vars and %d calls.\n",
+// p->pMSat->nSatVars, p->nRecycleCalls );
+// Aig_ManCleanMarkAB( p->pAig );
+ Aig_ManCleanMarkAB( p->pFrames );
+ // label nodes corresponding to primary inputs
+ Ssw_ManLabelPiNodes( p );
+ // replace the solver
+ if ( p->pMSat )
+ {
+ p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
+ Ssw_SatStop( p->pMSat );
+ p->nRecycles++;
+ p->nRecyclesTotal++;
+ p->nRecycleCalls = 0;
+ }
+ p->pMSat = Ssw_SatStart( 0 );
+ assert( p->nPatterns == 0 );
+ }
+ // resimulate
+ if ( p->nPatterns == 32 )
+ Ssw_ManSweepResimulateDyn( p, f );
+ }
+ // resimulate
+ if ( p->nPatterns > 0 )
+ Ssw_ManSweepResimulateDyn( p, f );
+ // collect stats
+ if ( p->pPars->fVerbose )
+ Bar_ProgressStop( pProgress );
+
+ // cleanup
+// Ssw_ClassesCheck( p->ppClasses );
+ return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 0a3f7e21..8d8d3265 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -72,14 +72,20 @@ struct Ssw_Man_t_
int nCallsUnsat; // the number of UNSAT calls in this round
int nRecycleCalls; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
- int nConeMax; // the maximum cone size
+ int nRecyclesTotal; // the number of time SAT solver was recycled
+ int nVarsMax; // the maximum variables in the solver
+ int nCallsMax; // the maximum number of SAT calls
// uniqueness
Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
- int iOutputLit; // the output literal of the uniqueness constaint
+ int iOutputLit; // the output literal of the uniqueness constraint
Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff
- int nUniques; // the number of uniqueness constaints used
+ int nUniques; // the number of uniqueness constraints used
int nUniquesAdded; // useful uniqueness constraints
int nUniquesUseful; // useful uniqueness constraints
+ // dynamic constraint addition
+ int nSRMiterMaxId; // max ID after which the last frame begins
+ Vec_Ptr_t * vNewLos; // new time frame LOs of to constrain
+ Vec_Int_t * vNewPos; // new time frame POs of to add constraints
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
@@ -93,7 +99,6 @@ struct Ssw_Man_t_
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
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
@@ -124,9 +129,9 @@ struct Ssw_Sat_t_
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
Vec_Int_t * vSatVars; // mapping of each node into its SAT var
- int nSatVarsTotal; // the total number of SAT vars created
Vec_Ptr_t * vFanins; // fanins of the CNF node
Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
+ int nSolverCalls; // the total number of SAT calls
};
// internal frames manager
@@ -211,6 +216,9 @@ extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
+/*=== sswDyn.c ===================================================*/
+extern void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int Ssw_ManSweepDyn( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
extern int Ssw_ManSweepLatch( Ssw_Man_t * p );
/*=== sswMan.c ===================================================*/
@@ -229,15 +237,18 @@ extern int Ssw_SmlObjIsConstWord( 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 int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame );
extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Ssw_SmlClean( Ssw_Sml_t * p );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
+extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
extern void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
extern void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern void Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
@@ -248,7 +259,7 @@ extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
-extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int Ssw_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
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index d374c5f6..8cb8b81b 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -300,6 +300,8 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
{
+ p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = Ssw_SatStart( 0 );
p->nRecycles++;
@@ -311,7 +313,6 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
Ssw_ManSweepResimulate( p );
// cleanup
Vec_PtrFree( vClass );
- p->nSatFailsTotal += p->nSatFailsReal;
// if ( p->pPars->fVerbose )
// Bar_ProgressStop( pProgress );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 1b29037c..91f6e713 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -58,6 +58,9 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ // other
+ p->vNewLos = Vec_PtrAlloc( 100 );
+ p->vNewPos = Vec_IntAlloc( 100 );
return p;
}
@@ -101,10 +104,10 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
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 );
- printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n",
- p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
- printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n",
- 0, p->nConeMax, p->nRecycles, p->nSimRounds );
+ 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",
+ p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
@@ -135,10 +138,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p )
{
+// Aig_ManCleanMarkAB( p->pAig );
assert( p->pMSat == NULL );
if ( p->pFrames )
{
- Aig_ManCleanMarkA( p->pFrames );
+ Aig_ManCleanMarkAB( p->pFrames );
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
@@ -165,8 +169,6 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManStop( Ssw_Man_t * p )
{
- Aig_ManCleanMarkA( p->pAig );
- Aig_ManCleanMarkB( p->pAig );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
@@ -175,6 +177,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_SmlStop( p->pSml );
if ( p->vDiffPairs )
Vec_IntFree( p->vDiffPairs );
+ Vec_PtrFree( p->vNewLos );
+ Vec_IntFree( p->vNewPos );
Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames );
FREE( p->pPatWords );
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index fc902560..2fd0fba3 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -44,6 +44,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
int nBTLimit = p->pPars->nBTLimit;
int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
+ p->pMSat->nSolverCalls++;
// sanity checks
assert( !Aig_IsComplement(pOld) );
@@ -231,7 +232,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// consider the constant 1 case
if ( pOld == Aig_ManConst1(p->pFrames) )
{
- // add constaint A = 1 ----> A
+ // add constraint A = 1 ----> A
pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
if ( p->pPars->fPolarFlip )
{
@@ -242,7 +243,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
else
{
- // add constaint A = B ----> (A v !B)(!A v B)
+ // add constraint A = B ----> (A v !B)(!A v B)
// (A v !B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index b445c2c4..572ab076 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -267,7 +267,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
}
if ( fVerbose )
{
- printf( "AIG : Const = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
+ printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
}
@@ -279,7 +279,7 @@ clk = clock();
Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
+ printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
p->pMan->nSatFailsReal? "f" : " " );
@@ -300,7 +300,6 @@ clk = clock();
pMan->nSatCalls = 0;
pMan->nSatProof = 0;
pMan->nSatFailsReal = 0;
- pMan->nSatFailsTotal = 0;
pMan->nSatCallsUnsat = 0;
pMan->nSatCallsSat = 0;
pMan->timeSimSat = 0;
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index b80c3710..ce6ca38c 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -359,11 +359,15 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
- int i;
+ int i, f;
assert( Aig_ObjIsPi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id );
for ( i = 0; i < p->nWordsTotal; i++ )
pSims[i] = Ssw_ObjRandomSim();
+ // set the first bit 0 in each frame
+ assert( p->nWordsFrame * p->nFrames == p->nWordsTotal );
+ for ( f = 0; f < p->nFrames; f++ )
+ pSims[p->nWordsFrame*f] <<= 1;
}
/**Function*************************************************************
@@ -381,6 +385,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pSims;
int i;
+ assert( iFrame < p->nFrames );
assert( Aig_ObjIsPi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
@@ -402,6 +407,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
{
unsigned * pSims;
int i;
+ assert( iFrame < p->nFrames );
assert( Aig_ObjIsPi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
@@ -422,6 +428,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
{
unsigned * pSims;
+ assert( iFrame < p->nFrames );
assert( Aig_ObjIsPi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = Word;
@@ -429,39 +436,6 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
/**Function*************************************************************
- Synopsis [Assings random simulation info for the PIs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
-{
- Aig_Obj_t * pObj;
- int i;
- if ( fInit )
- {
- assert( Aig_ManRegNum(p->pAig) > 0 );
- 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 );
- // assign the initial state for the latches
- Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
- }
- else
- {
- Aig_ManForEachPi( p->pAig, pObj, i )
- Ssw_SmlAssignRandom( p, pObj );
- }
-}
-
-/**Function*************************************************************
-
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
@@ -558,6 +532,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
+ assert( iFrame < p->nFrames );
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -623,6 +598,8 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO
{
unsigned * pSims0, * pSims1;
int i;
+ assert( iFrame0 < p->nFrames );
+ assert( iFrame1 < p->nFrames );
assert( !Aig_IsComplement(pObj0) );
assert( !Aig_IsComplement(pObj1) );
assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -652,6 +629,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pSims, * pSims0;
int fCompl, fCompl0, i;
+ assert( iFrame < p->nFrames );
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsPo(pObj) );
assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -685,6 +663,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
{
unsigned * pSims0, * pSims1;
int i;
+ assert( iFrame < p->nFrames );
assert( !Aig_IsComplement(pOut) );
assert( !Aig_IsComplement(pIn) );
assert( Aig_ObjIsPo(pOut) );
@@ -698,6 +677,92 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
pSims1[i] = pSims0[i];
}
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn )
+{
+ unsigned * pSims0, * pSims1;
+ int i;
+ assert( !Aig_IsComplement(pOut) );
+ assert( !Aig_IsComplement(pIn) );
+ assert( Aig_ObjIsPo(pOut) );
+ assert( Aig_ObjIsPi(pIn) );
+ assert( p->nWordsFrame < p->nWordsTotal );
+ // get hold of the simulation information
+ pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
+ pSims1 = Ssw_ObjSim(p, pIn->Id);
+ // copy information as it is
+ for ( i = 0; i < p->nWordsFrame; i++ )
+ pSims1[i] = pSims0[i];
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Assings random simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ if ( fInit )
+ {
+ assert( Aig_ManRegNum(p->pAig) > 0 );
+ 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 );
+ // assign the initial state for the latches
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
+ }
+ else
+ {
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ Ssw_SmlAssignRandom( p, pObj );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings random simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlReinitialize( Ssw_Sml_t * p )
+{
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i;
+ assert( Aig_ManRegNum(p->pAig) > 0 );
+ 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 );
+ // copy simulation info into the inputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ Ssw_SmlNodeTransferFirst( p, pObjLi, pObjLo );
+}
/**Function*************************************************************
@@ -744,12 +809,12 @@ clk = clock();
// copy simulation info into outputs
Saig_ManForEachPo( p->pAig, pObj, i )
Ssw_SmlNodeCopyFanin( p, pObj, f );
- // quit if this is the last timeframe
- if ( f == p->nFrames - 1 )
- break;
// copy simulation info into outputs
Saig_ManForEachLi( p->pAig, pObj, i )
Ssw_SmlNodeCopyFanin( p, pObj, f );
+ // quit if this is the last timeframe
+ if ( f == p->nFrames - 1 )
+ break;
// copy simulation info into the inputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
@@ -845,6 +910,22 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
free( p );
}
+/**Function*************************************************************
+
+ Synopsis [Deallocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNumFrames( Ssw_Sml_t * p )
+{
+ return p->nFrames;
+}
+
/**Function*************************************************************
@@ -887,6 +968,24 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
return p;
}
+/**Function*************************************************************
+
+ Synopsis [Performs next round of sequential simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
+{
+ Ssw_SmlReinitialize( p );
+ Ssw_SmlSimulateOne( p );
+ p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
+}
+
/**Function*************************************************************
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 36e8bab3..a2f3c175 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -69,6 +69,37 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
/**Function*************************************************************
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_CheckConstraints( Ssw_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObj2;
+ int nConstrPairs, i;
+ int Counter = 0;
+ nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+ assert( (nConstrPairs & 1) == 0 );
+ for ( i = 0; i < nConstrPairs; i += 2 )
+ {
+ pObj = Aig_ManPo( p->pFrames, i );
+ pObj2 = Aig_ManPo( p->pFrames, i+1 );
+ if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
+ {
+ Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
+ Counter++;
+ }
+ }
+ printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
+}
+
+/**Function*************************************************************
+
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
@@ -78,13 +109,13 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
SeeAlso []
***********************************************************************/
-void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
+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 ( Ssw_ManGetSatVarValue( p, pObj, f ) )
+ if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
Aig_InfoSetBit( p->pPatWords, i );
}
@@ -99,18 +130,48 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
SeeAlso []
***********************************************************************/
-void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
+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 ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
+ if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
+ Synopsis [Saves one counter-example into internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ unsigned * pInfo;
+ int i, nVarNum;
+ // iterate through the PIs of the frames
+ Vec_PtrForEachEntry( 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) );
+ Aig_InfoSetBit( pInfo, p->nPatterns );
+ }
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
@@ -123,7 +184,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
- int RetValue;
+ int RetValue, clk;
// get representative of this class
pObjRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pObjRepr == NULL )
@@ -134,48 +195,47 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
// check if constant 0 pattern distinquishes these nodes
assert( pObjFraig != NULL && pObjReprFraig != NULL );
- if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
+ 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;
+ // add constraints on demand
+ if ( !fBmc && p->pPars->fDynamic )
{
- p->nStrangers++;
- Ssw_SmlSavePatternAigPhase( p, f );
+clk = clock();
+ Ssw_ManLoadSolver( p, pObjRepr, pObj );
+ p->nRecycleCalls++;
+p->timeMarkCones += clock() - clk;
}
+ // call equivalence checking
+ if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
+ RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
else
- {
- // 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 the equivalence
- Ssw_SmlSavePatternAig( p, f );
+ 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 ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 &&
- Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
+ if ( RetValue == -1 ) // timed out
+ {
+ Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+ return 1;
+ }
+ // disproved the equivalence
+ if ( !fBmc && p->pPars->fDynamic )
+ {
+ Ssw_SmlAddPatternDyn( p );
+ p->nPatterns++;
+ return 1;
+ }
+ 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 RetValue;
- assert( p->iOutputLit > -1 );
- RetValue = Ssw_ManSweepNode( p, pObj, f, 0 );
- p->iOutputLit = -1;
- return RetValue;
- }
-*/
if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
{
int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@@ -186,7 +246,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
int x;
// printf( "Second time:\n" );
- x = Ssw_ManUniqueOne( p, pObjRepr, pObj );
+ 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 )
@@ -286,63 +346,17 @@ p->timeBmc += clock() - clk;
SeeAlso []
***********************************************************************/
-void Ssw_CheckConstaints( Ssw_Man_t * p )
-{
- Aig_Obj_t * pObj, * pObj2;
- int nConstrPairs, i;
- int Counter = 0;
- nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
- assert( (nConstrPairs & 1) == 0 );
- for ( i = 0; i < nConstrPairs; i += 2 )
- {
- pObj = Aig_ManPo( p->pFrames, i );
- pObj2 = Aig_ManPo( p->pFrames, i+1 );
- if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
- {
- Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
- Counter++;
- }
- }
- printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
- }
-
-/**Function*************************************************************
-
- Synopsis [Performs fraiging for the internal nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
- int nConstrPairs, clk, i, f;
-// int v;
+ int nConstrPairs, clk, i, f, v;
// perform speculative reduction
clk = clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
- // add constraints
-// p->pMSat = Ssw_SatStart( 0 );
-// Ssw_ManStartSolver( p );
-/*
- {
- int clk2 = clock();
- Ssw_CheckConstaints( p );
- PRT( "Time", clock() - clk2 );
- }
-
- Ssw_ManCleanup( p );
- p->pFrames = Ssw_FramesWithClasses( p );
- p->pMSat = Ssw_SatStart( 0 );
-// Ssw_ManStartSolver( p );
-*/
+ // add constants
nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
assert( (nConstrPairs & 1) == 0 );
for ( i = 0; i < nConstrPairs; i += 2 )
@@ -358,39 +372,22 @@ clk = clock();
Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
}
sat_solver_simplify( p->pMSat->pSat );
-p->timeReduce += clock() - clk;
-
-//Ssw_ManUnique( p );
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
- // make sure LOs are assigned
- Saig_ManForEachLo( p->pAig, pObj, i )
- assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
-/*
- // mark the PI/LO of the last frame
- Aig_ManForEachPi( p->pAig, pObj, i )
- {
- pObjNew = Ssw_ObjFrame( p, pObj, f );
- Aig_Regular(pObjNew)->fMarkA = 1;
- }
-*/
-////
-/*
+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;
- p->nSatFailsReal = 0;
- p->nUniques = 0;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
@@ -402,13 +399,11 @@ p->timeReduce += clock() - clk;
p->fRefined |= 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_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
}
}
- p->nSatFailsTotal += p->nSatFailsReal;
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
index 0d9b016f..d6590716 100644
--- a/src/aig/ssw/sswUnique.c
+++ b/src/aig/ssw/sswUnique.c
@@ -42,7 +42,7 @@
void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
{
Aig_Obj_t * pObjLo, * pObj0, * pObj1;
- int i;
+ int i, RetValue, Counter;
if ( p->vDiffPairs == NULL )
p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
Vec_IntClear( p->vDiffPairs );
@@ -54,13 +54,22 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
Vec_IntPush( p->vDiffPairs, 0 );
else if ( pObj0 == Aig_Not(pObj1) )
Vec_IntPush( p->vDiffPairs, 1 );
+// else
+// Vec_IntPush( p->vDiffPairs, 1 );
+ else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
+ Vec_IntPush( p->vDiffPairs, 1 );
else
{
- // assume that if the nodes are structurally different
- // they can also be functionally different
- Vec_IntPush( p->vDiffPairs, 1 );
+ RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
+ Vec_IntPush( p->vDiffPairs, RetValue!=1 );
}
}
+ assert( Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
+ // count the number of ones
+ Counter = 0;
+ Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
+ Counter += RetValue;
+// printf( "The number of different register pairs = %d.\n", Counter );
}
@@ -75,9 +84,8 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose )
{
- int fVerbose = 0;
Aig_Obj_t * ppObjs[2], * pTemp;
int i, k, Value0, Value1, RetValue, fFeasible;
@@ -93,12 +101,15 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
fFeasible = 0;
k = 0;
Vec_PtrForEachEntry( p->vCommon, pTemp, i )
- if ( Saig_ObjIsLo(p->pAig, pTemp) )
- {
- Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
- if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
- fFeasible = 1;
- }
+ {
+ assert( Aig_ObjIsPi(pTemp) );
+ if ( !Saig_ObjIsLo(p->pAig, pTemp) )
+ continue;
+ assert( Aig_ObjPioNum(pTemp) > 0 );
+ Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
+ if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
+ fFeasible = 1;
+ }
Vec_PtrShrink( p->vCommon, k );
if ( fVerbose )
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-15 22:51:42 +0000