mirror of https://github.com/YosysHQ/abc.git
141 lines
4.6 KiB
C
141 lines
4.6 KiB
C
/**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"
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// 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->nConstrs = 0; // treat the last nConstrs POs as seq constraints
|
|
p->nBTLimit = 1000; // conflict limit at a node
|
|
p->fPolarFlip = 0; // uses polarity adjustment
|
|
p->fLatchCorr = 0; // performs register correspondence
|
|
p->fVerbose = 0; // verbose stats
|
|
p->nIters = 0; // the number of iterations performed
|
|
}
|
|
|
|
/**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 )
|
|
{
|
|
Aig_Man_t * pAigNew;
|
|
Ssw_Man_t * p;
|
|
int RetValue, nIter, clk, clkTotal = clock();
|
|
// reset random numbers
|
|
Aig_ManRandom( 1 );
|
|
// start the choicing manager
|
|
p = Ssw_ManCreate( pAig, pPars );
|
|
// compute candidate equivalence classes
|
|
if ( p->pPars->nConstrs == 0 )
|
|
{
|
|
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
|
|
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 );
|
|
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
|
|
}
|
|
else
|
|
{
|
|
assert( 0 );
|
|
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
|
|
}
|
|
// Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
|
|
|
|
// get the starting stats
|
|
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
|
|
p->nNodesBeg = Aig_ManNodeNum(pAig);
|
|
p->nRegsBeg = Aig_ManRegNum(pAig);
|
|
// refine classes using BMC
|
|
if ( pPars->fVerbose )
|
|
{
|
|
printf( "Before BMC: " );
|
|
Ssw_ClassesPrint( p->ppClasses, 0 );
|
|
}
|
|
Ssw_ManSweepBmc( p );
|
|
Ssw_ManCleanup( p );
|
|
if ( pPars->fVerbose )
|
|
{
|
|
printf( "After BMC: " );
|
|
Ssw_ClassesPrint( p->ppClasses, 0 );
|
|
}
|
|
// refine classes using induction
|
|
for ( nIter = 0; ; nIter++ )
|
|
{
|
|
clk = clock();
|
|
RetValue = Ssw_ManSweep( p );
|
|
if ( pPars->fVerbose )
|
|
{
|
|
printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ",
|
|
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
|
|
p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
|
|
PRT( "T", clock() - clk );
|
|
}
|
|
Ssw_ManCleanup( p );
|
|
if ( !RetValue )
|
|
break;
|
|
}
|
|
p->pPars->nIters = nIter + 1;
|
|
p->timeTotal = clock() - clkTotal;
|
|
pAigNew = Aig_ManDupRepr( pAig, 0 );
|
|
Aig_ManSeqCleanup( pAigNew );
|
|
// get the final stats
|
|
p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses );
|
|
p->nNodesEnd = Aig_ManNodeNum(pAigNew);
|
|
p->nRegsEnd = Aig_ManRegNum(pAigNew);
|
|
// cleanup
|
|
Ssw_ManStop( p );
|
|
return pAigNew;
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|