/**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) )
Abc_Print( 1, "1" );
else if ( pObj == Aig_ManConst0(p) )
Abc_Print( 1, "0" );
else
Abc_Print( 1, "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) )
Abc_Print( 1, "o" );
else
Abc_Print( 1, "c" );
Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
}
Abc_Print( 1, "\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->vCos);
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_ObjIsCi(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_ManCiNum(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;
clock_t 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 )
{
Abc_Print( 1, "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 )
{
Abc_Print( 1, "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 )
{
Abc_Print( 1, "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 )
{
Abc_Print( 1, "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 );
Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
Abc_Print( 1, "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 )
{
Abc_Print( 1, "%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 )
{
Abc_Print( 1, "%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 )
{
Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
Abc_Print( 1, "R =%4d. ", p->nRecycles-nRecycles );
}
Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
(Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
ABC_PRT( "T", clock() - clk );
}
// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
// p->pPars->nBTLimit = 10000;
if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
{
printf( "Iterative refinement is stopped after iteration %d\n", nIter );
printf( "because the property output is no longer a candidate constant.\n" );
// prepare to quite
p->nLitsEnd = p->nLitsBeg;
p->nNodesEnd = p->nNodesBeg;
p->nRegsEnd = p->nRegsBeg;
// cleanup
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );
// cleanup
Aig_ManSetPhase( p->pAig );
Aig_ManCleanMarkB( p->pAig );
return Aig_ManDupSimple( p->pAig );
}
}
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 )
{
Abc_Print( 1, "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