Skip to content

A
abc
Commit 4db86550 by Alan Mishchenko
Options

Version abc80910

parent a30c08bb
Showing with 718 additions and 134 deletions
Makefile
......@@ -25,7 +25,7 @@ MODULES := \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr \
src/aig/int src/aig/dch
src/aig/int src/aig/dch src/aig/ssw
default: $(PROG)
......
abc.dsp
......@@ -3442,6 +3442,10 @@ SOURCE=.\src\aig\ssw\sswMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswPart.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswSat.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -470,6 +470,7 @@ extern int Aig_ManLevelNum( Aig_Man_t * p );
extern int Aig_ManChoiceLevel( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
......@@ -562,6 +563,7 @@ extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize,
extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
/*=== aigPartReg.c =========================================================*/
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
extern void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
extern Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
......
src/aig/aig/aigDfs.c
......@@ -685,6 +685,55 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
Synopsis [Counts the support size of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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_ObjIsPi(pObj) )
{
Vec_PtrPush( vSupp, pObj );
return;
}
assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
Aig_Support_rec( p, Aig_ObjFanin0(pObj), vSupp );
if ( Aig_ObjFanin1(pObj) )
Aig_Support_rec( p, Aig_ObjFanin1(pObj), vSupp );
}
/**Function*************************************************************
Synopsis [Counts the support size of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Vec_Ptr_t * vSupp;
assert( !Aig_IsComplement(pObj) );
assert( !Aig_ObjIsPo(pObj) );
Aig_ManIncrementTravId( p );
vSupp = Vec_PtrAlloc( 100 );
Aig_Support_rec( p, pObj, vSupp );
return vSupp;
}
/**Function*************************************************************
Synopsis [Transfers the AIG from one manager into another.]
Description []
......
src/aig/aig/aigPartReg.c
......@@ -498,6 +498,42 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOve
/**Function*************************************************************
Synopsis [Divides a large partition into several ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
{
Vec_Int_t * vPart;
int i, Counter;
assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
if ( nOverSize >= nPartSize )
{
printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
printf( "Adjusting it to be equal to half of the partition size.\n" );
nOverSize = nPartSize/2;
}
assert( nOverSize < nPartSize );
for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
{
vPart = Vec_IntAlloc( nPartSize );
for ( i = 0; i < nPartSize; i++, Counter++ )
if ( Counter < Vec_IntSize(vDomain) )
Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
if ( Vec_IntSize(vPart) <= nOverSize )
Vec_IntFree(vPart);
else
Vec_PtrPush( vResult, vPart );
}
}
/**Function*************************************************************
Synopsis [Computes partitioning of registers.]
Description []
......
src/aig/fra/fra.h
......@@ -283,8 +283,8 @@ static inline int Fra_ImpCreate( int Left, int Right )
/*=== fraCec.c ========================================================*/
extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
......
src/aig/fra/fraCec.c
......@@ -157,11 +157,11 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
SeeAlso []
***********************************************************************/
int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
{
int nBTLimitStart = 300; // starting SAT run
int nBTLimitFirst = 2; // first fraiging iteration
int nBTLimitLast = 1000000; // the last-gasp SAT run
int nBTLimitLast = nConfLimit; // the last-gasp SAT run
Fra_Par_t Params, * pParams = &Params;
Aig_Man_t * pAig = *ppAig, * pTemp;
......@@ -270,7 +270,7 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
{
Aig_Man_t * pAig;
Vec_Ptr_t * vParts;
......@@ -294,7 +294,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
continue;
if ( RetValue == 0 )
break;
RetValue = Fra_FraigCec( &pAig, 0 );
RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
Vec_PtrWriteEntry( vParts, i, pAig );
if ( RetValue == 1 )
continue;
......@@ -361,9 +361,9 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
if ( nPartSize )
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
else // no partitioning
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
// report the miter
if ( RetValue == 1 )
......
src/aig/fra/fraInd.c
......@@ -233,42 +233,6 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
free( pLatches );
}
/**Function*************************************************************
Synopsis [Divides a large partition into several ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_FraigInductionPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
{
Vec_Int_t * vPart;
int i, Counter;
assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
if ( nOverSize >= nPartSize )
{
printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
printf( "Adjusting it to be equal to half of the partition size.\n" );
nOverSize = nPartSize/2;
}
assert( nOverSize < nPartSize );
for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
{
vPart = Vec_IntAlloc( nPartSize );
for ( i = 0; i < nPartSize; i++, Counter++ )
if ( Counter < Vec_IntSize(vDomain) )
Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
if ( Vec_IntSize(vPart) <= nOverSize )
Vec_IntFree(vPart);
else
Vec_PtrPush( vResult, vPart );
}
}
/**Function*************************************************************
......@@ -304,7 +268,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Fra_FraigInductionPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
......
src/aig/fra/fraSec.c
......@@ -230,7 +230,7 @@ PRT( "Time", clock() - clk );
}
if ( pNew->nRegs == 0 )
RetValue = Fra_FraigCec( &pNew, 0 );
RetValue = Fra_FraigCec( &pNew, 100000, 0 );
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue >= 0 )
......
src/aig/ntl/ntlFraig.c
......@@ -20,6 +20,7 @@
#include "ntl.h"
#include "fra.h"
#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -494,7 +495,43 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
return pNew;
}
/**Function*************************************************************
Synopsis [Returns AIG with WB after fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
{
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
// collapse the AIG
pAig = Ntl_ManExtract( p );
pNew = Ntl_ManInsertAig( p, pAig );
pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
if ( pAigCol == NULL )
{
Aig_ManStop( pAig );
return pNew;
}
// perform SCL for the given design
pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
// finalize the transformation
pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
Ntl_ManFree( pAux );
Aig_ManStop( pAig );
Aig_ManStop( pAigCol );
return pNew;
}
/**Function*************************************************************
......
src/aig/ssw/module.make
......@@ -3,6 +3,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \
src/aig/ssw/sswSat.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
......
src/aig/ssw/ssw.h
......@@ -44,11 +44,14 @@ struct Ssw_Pars_t_
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
int nConstrs; // treat the last nConstrs POs as seq constraints
int nMaxLevs; // the max number of levels of nodes to consider
int nBTLimit; // conflict limit at a node
int nMinDomSize; // min clock domain considered for optimization
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
int fSkipCheck; // does not run equivalence check for unaffected cones
int fVerbose; // verbose stats
// internal parameters
int nIters; // the number of iterations performed
......@@ -77,6 +80,8 @@ struct Ssw_Cex_t_
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
#ifdef __cplusplus
......
src/aig/ssw/sswClass.c
......@@ -46,6 +46,7 @@ struct Ssw_Cla_t_
// temporary data
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
Vec_Ptr_t * vRefined; // the nodes refined since the last iteration
// procedures used for class refinement
void * pManData;
unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
......@@ -141,6 +142,7 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) );
p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 );
p->vRefined = Vec_PtrAlloc( 1000 );
assert( pAig->pReprs == NULL );
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
return p;
......@@ -183,6 +185,7 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
{
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
Vec_PtrFree( p->vRefined );
FREE( p->pId2Class );
FREE( p->pClassSizes );
FREE( p->pMemClasses );
......@@ -191,6 +194,38 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
{
return p->vRefined;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
{
Vec_PtrClear( p->vRefined );
}
/**Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
......@@ -368,12 +403,14 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
Aig_ObjSetRepr( p->pAig, pObj, NULL );
p->nCands1--;
return;
}
Vec_PtrPush( p->vRefined, pRepr );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
assert( p->pId2Class[pRepr->Id][0] == pRepr );
assert( p->pClassSizes[pRepr->Id] >= 2 );
......@@ -409,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
{
Ssw_Cla_t * p;
Ssw_Sml_t * pSml;
......@@ -424,7 +461,10 @@ 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 );
if ( fVerbose )
{
PRT( "Simulation of 32 frames with 4 words", clock() - clk );
}
// set comparison procedures
clk = clock();
......@@ -441,7 +481,7 @@ clk = clock();
{
if ( fLatchCorr )
{
if ( !Saig_ObjIsPi(p->pAig, pObj) )
if ( !Saig_ObjIsLo(p->pAig, pObj) )
continue;
}
else
......@@ -521,7 +561,10 @@ clk = clock();
Ssw_ClassesCheck( p );
Ssw_SmlStop( pSml );
// Ssw_ClassesPrint( p, 0 );
if ( fVerbose )
{
PRT( "Collecting candidate equival classes", clock() - clk );
}
return p;
}
......@@ -597,8 +640,6 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
}
// allocate room for classes
p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
// set comparison procedures
Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
// Ssw_ClassesPrint( p, 0 );
return p;
}
......@@ -631,6 +672,9 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
// check if splitting happened
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
// remember that this class is refined
Ssw_ClassForEachNode( p, pReprOld, pObj, i )
Vec_PtrPush( p->vRefined, pObj );
// get the new representative
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
......@@ -751,7 +795,10 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
{
pObj = Aig_ManObj( p->pAig, i );
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
{
Vec_PtrPush( p->vClassNew, pObj );
Vec_PtrPush( p->vRefined, pObj );
}
}
// check if there is a new class
if ( Vec_PtrSize(p->vClassNew) == 0 )
......
src/aig/ssw/sswCore.c
......@@ -45,8 +45,10 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
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->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->nMinDomSize = 100; // min clock domain considered for optimization
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
p->fVerbose = 0; // verbose stats
......@@ -71,21 +73,44 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
int RetValue, nIter, clk, clkTotal = clock();
// reset random numbers
Aig_ManRandom( 1 );
// 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
assert( Aig_ManRegNum(pAig) > 0 );
assert( pPars->nFramesK > 0 );
if ( pPars->nFramesK > 1 )
pPars->fSkipCheck = 0;
// perform partitioning
if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
return Ssw_SignalCorrespondencePart( pAig, pPars );
// start the choicing manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes
// p->pPars->nConstrs = 1;
if ( p->pPars->nConstrs == 0 )
{
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 );
// perform one round of seq simulation and generate candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
}
else
{
assert( 0 );
// 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_NodeIsConstCex, Ssw_NodesAreEqualCex );
}
// Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
// get the starting stats
p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
......@@ -111,9 +136,11 @@ clk = clock();
RetValue = Ssw_ManSweep( p );
if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ",
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk );
}
Ssw_ManCleanup( p );
......@@ -133,6 +160,8 @@ p->timeTotal = clock() - clkTotal;
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswInt.h
......@@ -57,6 +57,8 @@ struct Ssw_Man_t_
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
int nRefUse;
int nRefSkip;
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
......@@ -77,8 +79,8 @@ struct Ssw_Man_t_
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
int nSatFails; // the number of timeouts
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
......@@ -91,6 +93,7 @@ struct Ssw_Man_t_
// runtime stats
int timeBmc; // bounded model checking
int timeReduce; // speculative reduction
int timeMarkCones; // marking the cones not to be refined
int timeSimSat; // simulation of the counter-examples
int timeSat; // solving SAT
int timeSatSat; // sat
......@@ -136,6 +139,8 @@ extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void Ssw_ClassesStop( Ssw_Cla_t * p );
extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
......@@ -143,7 +148,7 @@ extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
......@@ -171,6 +176,7 @@ extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
......
src/aig/ssw/sswMan.c
......@@ -99,20 +99,21 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d. Max lev = %d. Mem = %0.2f Mb.\n",
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
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),
p->nSatVarsTotal/p->pPars->nIters );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Equivs = %d. Str = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStrangers );
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( "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) );
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
PRTP( "BMC ", p->timeBmc, p->timeTotal );
PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
PRTP( "SAT solving", p->timeSat, p->timeTotal );
PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
......@@ -167,6 +168,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManStop( Ssw_Man_t * p )
{
Aig_ManCleanMarkA( p->pAig );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
......
src/aig/ssw/sswPart.c 0 → 100644
/**CFile****************************************************************
FileName [sswPart.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Partitioned signal correspondence.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweepingG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 0;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
int clk = clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
}
else
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
if ( fPrintParts )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
}
// perform SSW with partitions
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
Aig_ManSetRegNum( pTemp, pTemp->nRegs );
// create the projection of 1-hot registers
if ( pAig->vOnehots )
pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
// run SSW
pNew = Ssw_SignalCorrespondence( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
if ( fVerbose )
printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
Aig_ManStop( pTemp );
free( pMapBack );
}
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
PRT( "Total time", clock() - clk );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw/sswSimSat.c
......@@ -234,7 +234,8 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
// set the PI simulation information
Aig_ManConst1(p->pAig)->fMarkB = 1;
Aig_ManForEachPi( p->pAig, pObj, i )
pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
// pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
// simulate internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
......@@ -253,27 +254,6 @@ p->timeSimSat += clock() - clk;
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 ( Ssw_ManOriginalPiValue( p, pObj, f ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
......@@ -287,7 +267,7 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
{
int RetValue1, RetValue2, clk = clock();
// save the counter-example
Ssw_SmlSavePatternAig( p, f );
// Ssw_SmlSavePatternAig( p, f );
// set the PI simulation information
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
// simulate internal nodes
......
src/aig/ssw/sswSweep.c
......@@ -31,6 +31,95 @@
/**Function*************************************************************
Synopsis [Mark nodes affected by sweep in the previous iteration.]
Description [Assumes that affected nodes are in p->ppClasses->vRefined.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
{
Vec_Ptr_t * vRefined, * vSupp;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i, k;
vRefined = Ssw_ClassesGetRefined( p->ppClasses );
if ( Vec_PtrSize(vRefined) == 0 )
{
Aig_ManForEachObj( p->pAig, pObj, i )
pObj->fMarkA = 1;
return;
}
// mark the nodes to be refined
Aig_ManCleanMarkA( p->pAig );
Vec_PtrForEachEntry( vRefined, pObj, i )
{
if ( Aig_ObjIsPi(pObj) )
{
pObj->fMarkA = 1;
continue;
}
assert( Aig_ObjIsNode(pObj) );
vSupp = Aig_Support( p->pAig, pObj );
Vec_PtrForEachEntry( vSupp, pObjLo, k )
pObjLo->fMarkA = 1;
Vec_PtrFree( vSupp );
}
// mark refinement
Aig_ManForEachNode( p->pAig, pObj, i )
pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
Saig_ManForEachLi( p->pAig, pObj, i )
pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA;
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
pObjLo->fMarkA |= pObjLi->fMarkA;
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 ( Ssw_ManOriginalPiValue( p, pObj, f ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
Aig_InfoSetBit( p->pPatWords, i );
}
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
......@@ -40,7 +129,7 @@
SeeAlso []
***********************************************************************/
void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
......@@ -50,59 +139,58 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
// get the fraiged node
pObjFraig = Ssw_ObjFraig( p, pObj, f );
assert( pObjFraig != NULL );
// get the fraiged representative
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
assert( pObjReprFraig != NULL );
// check if constant 0 pattern distinquishes these nodes
assert( pObjFraig != NULL && pObjReprFraig != NULL );
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
{
Aig_Obj_t * pObj;
int i;
if ( p->pSat->model.cap < p->pSat->size )
{
veci_resize(&p->pSat->model, 0);
for ( i = 0; i < p->pSat->size; i++ )
veci_push( &p->pSat->model, (int)l_False );
}
// set the values of SAT vars to be equal to the phase of the nodes
Aig_ManForEachObj( p->pFrames, pObj, i )
if ( Ssw_ObjSatNum( p, pObj ) )
{
int iVar = Ssw_ObjSatNum( p, pObj );
assert( iVar < p->pSat->size );
p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
p->pSat->model.size = p->pSat->size;
}
p->nStrangers++;
return;
Ssw_SmlSavePatternAigPhase( p, f );
}
else
{
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return;
// assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
// count the number of skipped calls
if ( !pObj->fMarkA && !pObjRepr->fMarkA )
p->nRefSkip++;
else
p->nRefUse++;
// call equivalence checking
if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
RetValue = 1;
else 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_ObjSetFraig( p, pObj, f, pObjFraig2 );
return;
}
if ( RetValue == -1 ) // timed out
{
// assert( 0 );
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
p->fRefined = 1;
return;
}
if ( RetValue == 1 ) // proved equivalent
// check if skipping calls works correctly
if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
return;
assert( 0 );
printf( "\nMistake!!!\n" );
}
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
// Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
else
Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
......@@ -147,7 +235,7 @@ clk = clock();
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
Ssw_ManSweepNode( p, pObj, f, 1 );
}
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
......@@ -205,6 +293,12 @@ clk = clock();
sat_solver_simplify( p->pSat );
p->timeReduce += clock() - clk;
// mark nodes that do not have to be refined
clk = clock();
if ( p->pPars->fSkipCheck )
Ssw_ManSweepMarkRefinement( p );
p->timeMarkCones += clock() - clk;
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
......@@ -215,6 +309,9 @@ p->timeReduce += clock() - clk;
assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
p->nRefUse = p->nRefSkip = 0;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
......@@ -222,14 +319,16 @@ p->timeReduce += clock() - clk;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
Ssw_ManSweepNode( p, pObj, f );
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_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
Ssw_ManSweepNode( p, pObj, f, 0 );
}
}
p->nSatFailsTotal += p->nSatFailsReal;
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
......
src/base/abci/abc.c
......@@ -245,6 +245,7 @@ static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Ssw ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Zero ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -506,6 +507,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*lcorr", Abc_CommandAbc8Lcorr, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*ssw", Abc_CommandAbc8Ssw, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*scorr", Abc_CommandAbc8Scorr, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*sw", Abc_CommandAbc8Sweep, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*zero", Abc_CommandAbc8Zero, 0 );
......@@ -7681,7 +7683,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtkRes;
// Abc_Ntk_t * pNtkRes;
int c;
int fBmc;
int nFrames;
......@@ -7700,7 +7702,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
// extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
......@@ -7869,7 +7871,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
/*
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
// pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
......@@ -7883,7 +7885,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
*/
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
......@@ -13483,7 +13485,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" );
fprintf( pErr, "usage: ssweep [-PQNFL <num>] [-lrfetvh]\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 );
......@@ -13528,7 +13530,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, "PQFCLNplvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF )
{
switch ( c )
{
......@@ -13595,7 +13597,18 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->nConstrs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConstrs <= 0 )
if ( pPars->nConstrs < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesAddSim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesAddSim < 0 )
goto usage;
break;
case 'p':
......@@ -13604,6 +13617,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
pPars->fLatchCorr ^= 1;
break;
case 's':
pPars->fSkipCheck ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -13656,7 +13672,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: scorr [-PQFCLN num] [-plvh]\n" );
fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsvh]\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 );
......@@ -13664,8 +13680,10 @@ usage:
fprintf( pErr, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
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-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-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "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;
......@@ -14586,7 +14604,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fMiter;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -14687,7 +14705,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fSat && fMiter )
Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
else
Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
......@@ -18764,6 +18782,182 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
void * pNtlNew;
Ssw_Pars_t Pars, * pPars = &Pars;
int c;
extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManScorr( void * p, Ssw_Pars_t * pPars );
extern int Ntl_ManIsComb( void * p );
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPartSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPartSize < 2 )
goto usage;
break;
case 'Q':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
goto usage;
}
pPars->nOverSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nOverSize < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesK = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesK <= 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit <= 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMaxLevs <= 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConstrs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConstrs < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesAddSim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesAddSim < 0 )
goto usage;
break;
case 'p':
pPars->fPolarFlip ^= 1;
break;
case 'l':
pPars->fLatchCorr ^= 1;
break;
case 's':
pPars->fSkipCheck ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
return 1;
}
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
return 0;
}
// get the input file name
pNtlNew = Ntl_ManScorr( pAbc->pAbc8Ntl, pPars );
if ( pNtlNew == NULL )
{
printf( "Abc_CommandAbc8Scorr(): Tranformation of the AIG has failed.\n" );
return 1;
}
Abc_FrameClearDesign();
pAbc->pAbc8Ntl = pNtlNew;
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Scorr(): Reading BLIF has failed.\n" );
return 1;
}
pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Scorr(): AIG extraction has failed.\n" );
return 1;
}
return 0;
usage:
fprintf( stdout, "usage: *scorr [-PQFCLNS <num>] [-plsvh]\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 );
fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
fprintf( stdout, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
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-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-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
{
void * pNtlTemp;
......@@ -18956,7 +19150,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
// set defaults
nConfLimit = 10000;
nConfLimit = 100000;
nPartSize = 100;
fSmart = 0;
fVerbose = 0;
......
src/base/abci/abcDar.c
......@@ -1084,7 +1084,7 @@ int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConf
SeeAlso []
***********************************************************************/
int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose )
int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose )
{
Aig_Man_t * pMan, * pMan1, * pMan2;
Abc_Ntk_t * pMiter;
......@@ -1102,7 +1102,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
{
pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, 1, fVerbose );
RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, 100, 1, fVerbose );
Aig_ManStop( pMan1 );
Aig_ManStop( pMan2 );
goto finish;
......@@ -1152,7 +1152,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
return -1;
}
// perform verification
RetValue = Fra_FraigCec( &pMan, fVerbose );
RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
// transfer model if given
if ( pNtk2 == NULL )
pNtk1->pModel = pMan->pData, pMan->pData = NULL;
......
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