summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/sswCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw/sswCore.c')
-rw-r--r--src/proof/ssw/sswCore.c522
1 files changed, 522 insertions, 0 deletions
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
new file mode 100644
index 00000000..df48a5b8
--- /dev/null
+++ b/src/proof/ssw/sswCore.c
@@ -0,0 +1,522 @@
+/**CFile****************************************************************
+
+ FileName [sswCore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [The core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
+{
+ memset( p, 0, sizeof(Ssw_Pars_t) );
+ 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->fConstrs = 0; // treat the last nConstrs POs as seq constraints
+ p->fMergeFull = 0; // enables full merge when constraints are used
+ p->nBTLimit = 1000; // conflict limit at a node
+ p->nBTLimitGlobal = 5000000; // conflict limit for all runs
+ p->nMinDomSize = 100; // min clock domain considered for optimization
+ p->nItersStop = -1; // stop after the given number of iterations
+ p->nResimDelta = 1000; // the internal of nodes to resimulate
+ p->nStepsMax = -1; // (scorr only) the max number of induction steps
+ p->fPolarFlip = 0; // uses polarity adjustment
+ p->fLatchCorr = 0; // performs register correspondence
+ p->fConstCorr = 0; // performs constant correspondence
+ p->fOutputCorr = 0; // perform 'PO correspondence'
+ p->fSemiFormal = 0; // enable semiformal filtering
+ p->fDynamic = 0; // dynamic partitioning
+ p->fLocalSim = 0; // local simulation
+ p->fVerbose = 0; // verbose stats
+ p->fEquivDump = 0; // enables dumping equivalences
+
+ // latch correspondence
+ 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
+}
+
+/**Function*************************************************************
+
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
+{
+ Ssw_ManSetDefaultParams( p );
+ p->fLatchCorrOpt = 1;
+ p->nBTLimit = 10000;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports improvements for property cones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop )
+{
+ Aig_Man_t * pAig1, * pAig2, * pAux;
+ pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 );
+ pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0, -1, -1, 0, 0 );
+ Aig_ManStop( pAux );
+ pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
+ pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 );
+ Aig_ManStop( pAux );
+
+ p->nNodesBegC = Aig_ManNodeNum(pAig1);
+ p->nNodesEndC = Aig_ManNodeNum(pAig2);
+ p->nRegsBegC = Aig_ManRegNum(pAig1);
+ p->nRegsEndC = Aig_ManRegNum(pAig2);
+
+ Aig_ManStop( pAig1 );
+ Aig_ManStop( pAig2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( pObj == Aig_ManConst1(p) )
+ printf( "1" );
+ else if ( pObj == Aig_ManConst0(p) )
+ printf( "0" );
+ else
+ printf( "X" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports improvements for property cones.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ReportOutputs( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
+ printf( "o" );
+ else
+ printf( "c" );
+ Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Remove from-equivs that are in the cone of constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+{
+ Vec_Ptr_t * vCones;
+ Aig_Obj_t ** pArray;
+ Aig_Obj_t * pObj;
+ int i, nTotal = 0, nRemoved = 0;
+ // collect the nodes in the cone of constraints
+ pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos);
+ pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
+ vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
+ // remove all the node that are equiv to something and are in the cones
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ if ( pAig->pReprs[i] != NULL )
+ nTotal++;
+ if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ continue;
+ if ( pAig->pReprs[i] )
+ {
+ if ( p->pPars->fConstrs && !p->pPars->fMergeFull )
+ {
+ pAig->pReprs[i] = NULL;
+ nRemoved++;
+ }
+ }
+ }
+ // collect statistics
+ p->nConesTotal = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig);
+ p->nConesConstr = Vec_PtrSize(vCones);
+ p->nEquivsTotal = nTotal;
+ p->nEquivsConstr = nRemoved;
+ Vec_PtrFree( vCones );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs computation of signal correspondence with constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
+{
+ int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
+ Aig_Man_t * pAigNew;
+ int RetValue, nIter = -1;
+ int clk, clkTotal = clock();
+ // get the starting stats
+ p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
+ p->nNodesBeg = Aig_ManNodeNum(p->pAig);
+ p->nRegsBeg = Aig_ManRegNum(p->pAig);
+ // refine classes using BMC
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Before BMC: " );
+ Ssw_ClassesPrint( p->ppClasses, 0 );
+ }
+ if ( !p->pPars->fLatchCorr )
+ {
+ p->pMSat = Ssw_SatStart( 0 );
+ if ( p->pPars->fConstrs )
+ Ssw_ManSweepBmcConstr( p );
+ else
+ Ssw_ManSweepBmc( p );
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = NULL;
+ Ssw_ManCleanup( p );
+ }
+ if ( p->pPars->fVerbose )
+ {
+ printf( "After BMC: " );
+ Ssw_ClassesPrint( p->ppClasses, 0 );
+ }
+ // apply semi-formal filtering
+/*
+ if ( p->pPars->fSemiFormal )
+ {
+ Aig_Man_t * pSRed;
+ Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
+// Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
+ pSRed = Ssw_SpeculativeReduction( p );
+ Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+ Aig_ManStop( pSRed );
+ }
+*/
+ if ( p->pPars->pFunc )
+ {
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+ }
+ if ( p->pPars->nStepsMax == 0 )
+ {
+ printf( "Stopped signal correspondence after BMC.\n" );
+ goto finalize;
+ }
+ // refine classes using induction
+ nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
+ for ( nIter = 0; ; nIter++ )
+ {
+ if ( p->pPars->nStepsMax == nIter )
+ {
+ printf( "Stopped signal correspondence after %d refiment iterations.\n", nIter );
+ goto finalize;
+ }
+ if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
+ {
+ Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
+ Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+ Aig_ManStop( pSRed );
+ printf( "Iterative refinement is stopped before iteration %d.\n", nIter );
+ printf( "The network is reduced using candidate equivalences.\n" );
+ printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
+ printf( "If the miter is SAT, the reduced result is incorrect.\n" );
+ break;
+ }
+
+clk = clock();
+ p->pMSat = Ssw_SatStart( 0 );
+ if ( p->pPars->fLatchCorrOpt )
+ {
+ RetValue = Ssw_ManSweepLatch( p );
+ if ( p->pPars->fVerbose )
+ {
+ printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
+ p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
+ ABC_PRT( "T", clock() - clk );
+ }
+ }
+ else
+ {
+ if ( p->pPars->fConstrs )
+ RetValue = Ssw_ManSweepConstr( p );
+ else if ( p->pPars->fDynamic )
+ RetValue = Ssw_ManSweepDyn( p );
+ else
+ RetValue = Ssw_ManSweep( p );
+
+ p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
+ if ( p->pPars->fVerbose )
+ {
+ printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+ if ( p->pPars->fDynamic )
+ {
+ printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
+ printf( "R =%4d. ", p->nRecycles-nRecycles );
+ }
+ printf( "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
+ (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManPo(p->pAig,0))))? "+" : "-" );
+ ABC_PRT( "T", clock() - clk );
+ }
+// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
+// p->pPars->nBTLimit = 10000;
+ }
+ nSatProof = p->nSatProof;
+ nSatCallsSat = p->nSatCallsSat;
+ nRecycles = p->nRecycles;
+ nSatFailsReal = p->nSatFailsReal;
+ nUniques = p->nUniques;
+
+ p->nVarsMax = Abc_MaxInt( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
+ Ssw_SatStop( p->pMSat );
+ p->pMSat = NULL;
+ Ssw_ManCleanup( p );
+ if ( !RetValue )
+ break;
+ if ( p->pPars->pFunc )
+ ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+ }
+
+finalize:
+ p->pPars->nIters = nIter + 1;
+p->timeTotal = clock() - clkTotal;
+
+ Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
+ pAigNew = Aig_ManDupRepr( p->pAig, 0 );
+ Aig_ManSeqCleanup( pAigNew );
+//Ssw_ClassesPrint( p->ppClasses, 1 );
+ // get the final stats
+ p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses );
+ p->nNodesEnd = Aig_ManNodeNum(pAigNew);
+ p->nRegsEnd = Aig_ManRegNum(pAigNew);
+ // cleanup
+ Aig_ManSetPhase( p->pAig );
+ Aig_ManCleanMarkB( p->pAig );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs computation of signal correspondence with constraints.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+ Ssw_Pars_t Pars;
+ Aig_Man_t * pAigNew;
+ Ssw_Man_t * p;
+ assert( Aig_ManRegNum(pAig) > 0 );
+ // reset random numbers
+ Aig_ManRandom( 1 );
+ // if parameters are not given, create them
+ if ( pPars == NULL )
+ Ssw_ManSetDefaultParams( pPars = &Pars );
+ // 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
+ if ( pPars->fLatchCorrOpt )
+ {
+ pPars->fLatchCorr = 1;
+ pPars->nFramesAddSim = 0;
+ if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
+ return Ssw_SignalCorrespondencePart( pAig, pPars );
+ }
+ else
+ {
+ assert( pPars->nFramesK > 0 );
+ // perform partitioning
+ if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+ || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
+ return Ssw_SignalCorrespondencePart( pAig, pPars );
+ }
+
+ if ( pPars->fScorrGia )
+ {
+ if ( pPars->fLatchCorrOpt )
+ {
+ extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+ return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+ }
+ else
+ {
+ extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+ return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+ }
+ }
+
+ // start the induction manager
+ p = Ssw_ManCreate( pAig, pPars );
+ // compute candidate equivalence classes
+// p->pPars->nConstrs = 1;
+ if ( p->pPars->fConstrs )
+ {
+ // create trivial equivalence classes with all nodes being candidates for constant 1
+ p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+ Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
+ // derive phase bits to satisfy the constraints
+ if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
+ {
+ printf( "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
+ p->pPars->fVerbose = 0;
+ Ssw_ManStop( p );
+ return NULL;
+ }
+ // perform simulation of the first timeframes
+ Ssw_ManRefineByConstrSim( p );
+ }
+ else
+ {
+ // perform one round of seq simulation and generate candidate equivalence classes
+ p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
+// p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
+ 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, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
+ }
+ // allocate storage
+ if ( p->pPars->fLocalSim )
+ p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
+ // perform refinement of classes
+ pAigNew = Ssw_SignalCorrespondenceRefine( p );
+// Ssw_ReportOutputs( pAigNew );
+ if ( pPars->fConstrs && pPars->fVerbose )
+ Ssw_ReportConeReductions( p, pAig, pAigNew );
+ // cleanup
+ Ssw_ManStop( p );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs computation of latch correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+ Aig_Man_t * pRes;
+ Ssw_Pars_t Pars;
+ if ( pPars == NULL )
+ Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
+ pRes = Ssw_SignalCorrespondence( pAig, pPars );
+// if ( pPars->fConstrs && pPars->fVerbose )
+// Ssw_ReportConeReductions( pAig, pRes );
+ return pRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:48:49 +0000