Skip to content

A
abc
Commit a4bca405 by Alan Mishchenko
Options

Version abc81014

parent e917dda1
Showing with 916 additions and 233 deletions
abc.dsp
......@@ -3474,6 +3474,10 @@ SOURCE=.\src\aig\ssw\sswCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswDyn.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswInt.h
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -634,6 +634,7 @@ extern int Aig_ManLevels( Aig_Man_t * p );
extern void Aig_ManResetRefs( Aig_Man_t * p );
extern void Aig_ManCleanMarkA( Aig_Man_t * p );
extern void Aig_ManCleanMarkB( Aig_Man_t * p );
extern void Aig_ManCleanMarkAB( Aig_Man_t * p );
extern void Aig_ManCleanData( Aig_Man_t * p );
extern void Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
......
src/aig/aig/aigDfs.c
......@@ -699,6 +699,8 @@ 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_ObjIsConst1(pObj) )
return;
if ( Aig_ObjIsPi(pObj) )
{
Vec_PtrPush( vSupp, pObj );
......
src/aig/aig/aigUtil.c
......@@ -168,6 +168,25 @@ void Aig_ManCleanMarkB( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Cleans fMarkB.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCleanMarkAB( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
Aig_ManForEachObj( p, pObj, i )
pObj->fMarkA = pObj->fMarkB = 0;
}
/**Function*************************************************************
Synopsis [Cleans the data pointers for the nodes.]
Description []
......
src/aig/fra/fra.h
......@@ -118,6 +118,8 @@ struct Fra_Sec_t_
int nFramesMax; // the max number of frames used for induction
int nBTLimit; // the conflict limit at a node
int nBTLimitGlobal; // the global conflict limit
int nBTLimitInter; // the conflict limit for interpolation
int nBddVarsMax; // the state space limit for BDD reachability
int nBddMax; // the max number of BDD nodes
int nBddIterMax; // the limit on the number of BDD iterations
int fPhaseAbstract; // enables phase abstraction
......@@ -361,7 +363,7 @@ extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld,
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec );
extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
/*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
......
src/aig/fra/fraInd.c
......@@ -32,7 +32,7 @@
/**Function*************************************************************
Synopsis [Performs AIG rewriting on the constaint manager.]
Synopsis [Performs AIG rewriting on the constraint manager.]
Description []
......@@ -536,7 +536,7 @@ p->timeTrav += clock() - clk2;
// report the intermediate results
if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. ",
printf( "%3d : C = %6d. Cl = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
......
src/aig/fra/fraSec.c
......@@ -51,6 +51,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->nFramesMax = 4; // the max number of frames used for induction
p->nBTLimit = 1000; // conflict limit at a node during induction
p->nBTLimitGlobal = 5000000; // global conflict limit during induction
p->nBTLimitInter = 10000; // conflict limit during interpolation
p->nBddVarsMax = 150; // the limit on the number of registers in BDD reachability
p->nBddMax = 50000; // the limit on the number of BDD nodes
p->nBddIterMax = 1000000; // the limit on the number of BDD iterations
p->fPhaseAbstract = 0; // enables phase abstraction
......@@ -81,7 +83,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
{
Ssw_Pars_t Pars2, * pPars2 = &Pars2;
Fra_Ssw_t Pars, * pPars = &Pars;
......@@ -461,6 +463,7 @@ clk = clock();
int Depth;
Inter_ManSetDefaultParams( pPars );
pPars->nBTLimit = pParSec->nBTLimitInter;
pPars->fVerbose = pParSec->fVeryVerbose;
if ( Saig_ManPoNum(pNew) == 1 )
{
......@@ -495,7 +498,7 @@ PRT( "Time", clock() - clk );
}
// try reachability analysis
if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
......@@ -563,6 +566,8 @@ PRT( "Time", clock() - clkTotal );
FREE( pNew->pSeqModel );
}
}
if ( ppResult != NULL )
*ppResult = Aig_ManDupSimpleDfs( pNew );
if ( pNew )
Aig_ManStop( pNew );
return RetValue;
......
src/aig/mfx/mfxResub.c
......@@ -463,6 +463,9 @@ int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode )
}
if ( Nwk_ObjFaninNum(pNode) == p->nFaninMax )
return 0;
return 0; /// !!!!! temporary workaround
// try replacing area critical fanins while adding two new fanins
Nwk_ObjForEachFanin( pNode, pFanin, i )
if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
......
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 \
......
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
......
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;
}
......
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 );
......
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 );
......
src/aig/ssw/sswDyn.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
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
......
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 );
......
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 );
......
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 );
......
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;
......
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*************************************************************
......
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 );
......
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 )
......
src/base/abci/abc.c
......@@ -8335,7 +8335,7 @@ int Abc_CommandSenseInput( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: senseinput [-C num] [-vh]\n" );
fprintf( pErr, "\t computes sensitivity of POs to PIs under constaint\n" );
fprintf( pErr, "\t computes sensitivity of POs to PIs under constraint\n" );
fprintf( pErr, "\t constraint should be represented as the last PO" );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfLim );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
......@@ -13559,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIplfuvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIVMplfudvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -13651,6 +13651,28 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nItersStop < 0 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
pPars->nSatVarMax2 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nSatVarMax2 < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRecycleCalls2 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRecycleCalls2 < 0 )
goto usage;
break;
case 'p':
pPars->fPolarFlip ^= 1;
break;
......@@ -13663,6 +13685,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'u':
pPars->fUniqueness ^= 1;
break;
case 'd':
pPars->fDynamic ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -13693,19 +13718,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
/*
if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
{
printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
return 0;
}
if ( pPars->nFramesP && pPars->fUse1Hot )
{
printf( "Currrently can only use one-hotness without prefix.\n" );
return 0;
}
*/
// get the new network
pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars );
if ( pNtkRes == NULL )
......@@ -13718,7 +13731,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: scorr [-PQFCLNSI <num>] [-plfuvwh]\n" );
fprintf( pErr, "usage: scorr [-PQFCLNSIVM <num>] [-pludvwh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
......@@ -13728,12 +13741,15 @@ usage:
fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
fprintf( pErr, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
fprintf( pErr, "\t-I num : iteration number to stop and output SR-model (0=none) [default = %d]\n", pPars->nItersStop );
fprintf( pErr, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
fprintf( pErr, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
// fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
// fprintf( pErr, "\t-f : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
......@@ -15213,7 +15229,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Fra_SecSetDefaultParams( pSecPar );
// pSecPar->TimeLimit = 300;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGBRarmfijwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -15256,6 +15272,28 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pSecPar->nBTLimitGlobal < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pSecPar->nBTLimitInter = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pSecPar->nBTLimitInter < 0 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
pSecPar->nBddVarsMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pSecPar->nBddVarsMax < 0 )
goto usage;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
......@@ -15321,11 +15359,13 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dprove [-FCGBR num] [-cbarmfijwvh]\n" );
fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
fprintf( pErr, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal );
fprintf( pErr, "\t-D num : the conflict limit during interpolation [default = %d]\n", pSecPar->nBTLimitInter );
fprintf( pErr, "\t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax );
fprintf( pErr, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax );
fprintf( pErr, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax );
fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" );
......@@ -19221,12 +19261,37 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nMinDomSize < 0 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
pPars->nSatVarMax2 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nSatVarMax2 < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRecycleCalls2 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRecycleCalls2 < 0 )
goto usage;
break;
case 'p':
pPars->fPolarFlip ^= 1;
break;
case 'l':
pPars->fLatchCorr ^= 1;
break;
case 'd':
pPars->fDynamic ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -19249,6 +19314,13 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( pPars->fDynamic && (pPars->nPartSize || pPars->nOverSize) )
{
pPars->nPartSize = 0;
pPars->nOverSize = 0;
printf( "With dynamic partitioning (-d) enabled, static one (-P <num> -Q <num>) is ignored.\n" );
}
// get the input file name
pNtlNew = Ntl_ManScorr( pAbc->pAbc8Ntl, pPars );
if ( pNtlNew == NULL )
......@@ -19273,7 +19345,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plvh]\n" );
fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-plvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
......@@ -19283,8 +19355,11 @@ usage:
fprintf( stdout, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
fprintf( stdout, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
fprintf( stdout, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
fprintf( stdout, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( stdout, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
......@@ -19619,7 +19694,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern void Fra_SecSetDefaultParams( Fra_Sec_t * pSecPar );
extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar );
extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar, Aig_Man_t ** ppResult );
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
// set defaults
......@@ -19678,7 +19753,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
if ( pAig == NULL )
return 0;
Fra_FraigSec( pAig, pSecPar );
Fra_FraigSec( pAig, pSecPar, NULL );
Aig_ManStop( pAig );
return 0;
......
src/base/abci/abcDar.c
......@@ -1694,7 +1694,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
}
else
{
RetValue = Fra_FraigSec( pMan, pSecPar );
RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
......@@ -1793,7 +1793,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, pSecPar );
RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
Aig_ManStop( pMan );
return RetValue;
}
......
src/base/abci/abcSense.c
......@@ -140,7 +140,7 @@ Abc_Ntk_t * Abc_NtkSensitivityMiter( Abc_Ntk_t * pNtk, int iVar )
/**Function*************************************************************
Synopsis [Computing sensitivity of POs to POs under constaints.]
Synopsis [Computing sensitivity of POs to POs under constraints.]
Description [The input network is a combinatonal AIG. The last output
is a constraint. The procedure returns the list of number of PIs,
......
src/base/abci/abcSweep.c
......@@ -88,6 +88,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
// perform fraiging of the AIG
Fraig_ParamsSetDefault( &Params );
Params.fInternal = 1;
pMan = Abc_NtkToFraig( pNtkAig, &Params, 0, 0 );
// cannot use EXDC with FRAIG because it can create classes of equivalent FRAIG nodes
// with representative nodes that do not correspond to the nodes with the current network
......
src/base/main/mainMC.c
......@@ -107,7 +107,7 @@ int main( int argc, char * argv[] )
pSecPar->fSilent = 1; // disable phase-abstraction
Dar_LibStart();
RetValue = Fra_FraigSec( pAig, pSecPar );
RetValue = Fra_FraigSec( pAig, pSecPar, NULL );
Dar_LibStop();
Cnf_ClearMemory();
}
......
src/map/mapper/mapperMatch.c
......@@ -226,7 +226,7 @@ int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase )
Area2 = Map_SwitchCutRef( pNode, pNode->pCutBest[fPhase], fPhase );
else
assert( 0 );
assert( Area2 < Area1 + p->fEpsilon );
// assert( Area2 < Area1 + p->fEpsilon );
}
// make sure that the requited times are met
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment