mirror of https://github.com/YosysHQ/abc.git
Version abc81029
This commit is contained in:
Alan Mishchenko
parent
d80ee832f3
commit
c9ad5880cc
2
Makefile
2
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/ssw
|
||||
src/aig/int src/aig/dch src/aig/ssw src/aig/cgt
|
||||
|
||||
default: $(PROG)
|
||||
|
||||
|
|
|
|||
36
abc.dsp
36
abc.dsp
|
|
@ -42,7 +42,7 @@ RSC=rc.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
|
||||
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
||||
# ADD RSC /l 0x409 /d "NDEBUG"
|
||||
BSC32=bscmake.exe
|
||||
|
|
@ -66,7 +66,7 @@ LINK32=link.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
|
||||
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||
# SUBTRACT CPP /X
|
||||
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
||||
# ADD RSC /l 0x409 /d "_DEBUG"
|
||||
|
|
@ -3533,6 +3533,38 @@ SOURCE=.\src\aig\ssw\sswUnique.c
|
|||
|
||||
# PROP Default_Filter ""
|
||||
# End Group
|
||||
# Begin Group "cgt"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtAig.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtCore.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtDecide.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\cgt\cgtSat.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "Header Files"
|
||||
|
|
|
|||
|
|
@ -328,6 +328,8 @@ static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj-
|
|||
static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; }
|
||||
static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
|
||||
static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
|
||||
static inline Aig_Obj_t * Aig_ObjChild0Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pNext, Aig_ObjFaninC0(pObj)) : NULL; }
|
||||
static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pNext, Aig_ObjFaninC1(pObj)) : NULL; }
|
||||
static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); }
|
||||
static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); }
|
||||
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; }
|
||||
|
|
@ -637,6 +639,7 @@ 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_ManCleanNext( Aig_Man_t * p );
|
||||
extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
|
||||
extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj );
|
||||
extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
|
||||
|
|
|
|||
|
|
@ -204,6 +204,25 @@ void Aig_ManCleanData( Aig_Man_t * p )
|
|||
pObj->pData = NULL;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Cleans the data pointers for the nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Aig_ManCleanNext( Aig_Man_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
Aig_ManForEachObj( p, pObj, i )
|
||||
pObj->pNext = NULL;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Recursively cleans the data pointers in the cone of the node.]
|
||||
|
|
|
|||
|
|
@ -0,0 +1,81 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __CGT_H__
|
||||
#define __CGT_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
/*
|
||||
The algorithm implemented in this package is based on the paper:
|
||||
A. Hurst. "Automatic synthesis of clock gating logic with controlled
|
||||
netlist perturbation", DAC 2008.
|
||||
*/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Cgt_Par_t_ Cgt_Par_t;
|
||||
struct Cgt_Par_t_
|
||||
{
|
||||
int nLevelMax; // the max number of levels to look for clock-gates
|
||||
int nCandMax; // the max number of candidates at each node
|
||||
int nOdcMax; // the max number of ODC levels to consider
|
||||
int nConfMax; // the max number of conflicts at a node
|
||||
int nVarsMin; // the min number of variables to recycle the SAT solver
|
||||
int nFlopsMin; // the min number of flops needed to recycle the SAT solver
|
||||
int fVerbose; // verbosity flag
|
||||
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== cgtCore.c ==========================================================*/
|
||||
extern void Cgt_SetDefaultParams( Cgt_Par_t * p );
|
||||
extern Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
|
||||
extern Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,311 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtAig.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [Creates AIG to compute clock-gating.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cgtInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes transitive fanout cone of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
|
||||
{
|
||||
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(pAig, pObj);
|
||||
if ( Aig_ObjIsNode(pObj) )
|
||||
{
|
||||
Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin0(pObj), nLevelMax, vCands );
|
||||
Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin1(pObj), nLevelMax, vCands );
|
||||
}
|
||||
if ( Aig_ObjLevel(pObj) <= nLevelMax )
|
||||
Vec_PtrPush( vCands, pObj );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes transitive fanout cone of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
|
||||
{
|
||||
Vec_PtrClear( vCands );
|
||||
if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
|
||||
return;
|
||||
Aig_ManIncrementTravId( pAig );
|
||||
Cgt_ManDetectCandidates_rec( pAig, pObj, nLevelMax, vCands );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes transitive fanout cone of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManDetectFanout_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
|
||||
{
|
||||
Aig_Obj_t * pFanout;
|
||||
int f, iFanout;
|
||||
if ( Aig_ObjIsPo(pObj) || Aig_ObjLevel(pObj) > nOdcMax )
|
||||
return;
|
||||
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(pAig, pObj);
|
||||
Vec_PtrPush( vFanout, pObj );
|
||||
Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f )
|
||||
Cgt_ManDetectFanout_rec( pAig, pFanout, nOdcMax, vFanout );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes transitive fanout cone of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
|
||||
{
|
||||
Aig_Obj_t * pFanout;
|
||||
int i, k, f, iFanout;
|
||||
// collect visited nodes
|
||||
Vec_PtrClear( vFanout );
|
||||
Aig_ManIncrementTravId( pAig );
|
||||
Cgt_ManDetectFanout_rec( pAig, pObj, nOdcMax, vFanout );
|
||||
// remove those nodes whose fanout is included
|
||||
k = 0;
|
||||
Vec_PtrForEachEntry( vFanout, pObj, i )
|
||||
{
|
||||
// go through the fanouts of this node
|
||||
Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f )
|
||||
if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
|
||||
break;
|
||||
if ( f == Aig_ObjRefs(pObj) ) // all fanouts are included
|
||||
continue;
|
||||
Vec_PtrWriteEntry( vFanout, k++, pObj );
|
||||
}
|
||||
Vec_PtrShrink( vFanout, k );
|
||||
Vec_PtrSort( vFanout, Aig_ObjCompareIdIncrease );
|
||||
assert( Vec_PtrSize(vFanout) > 0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives miter for clock-gating.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo )
|
||||
{
|
||||
Aig_Obj_t * pMiter, * pRoot;
|
||||
int i;
|
||||
assert( Aig_ObjIsPi(pObjLo) );
|
||||
pMiter = Aig_ManConst0( pNew );
|
||||
Cgt_ManDetectFanout( p->pAig, pObjLo, p->pPars->nOdcMax, p->vFanout );
|
||||
Vec_PtrForEachEntry( p->vFanout, pRoot, i )
|
||||
pMiter = Aig_Or( pNew, pMiter, Aig_Exor(pNew, pRoot->pData, pRoot->pNext) );
|
||||
return pMiter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives AIG for clock-gating.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
|
||||
{
|
||||
Aig_Man_t * pNew;
|
||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||
int i;
|
||||
assert( Aig_ManRegNum(p->pAig) );
|
||||
Aig_ManCleanNext( p->pAig );
|
||||
pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
|
||||
// build the first frame
|
||||
Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
|
||||
Aig_ManForEachPi( p->pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
// Saig_ManForEachPo( p->pAig, pObj, i )
|
||||
// pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
// build the second frame
|
||||
Aig_ManConst1(p->pAig)->pNext = Aig_ManConst1(pNew);
|
||||
Saig_ManForEachPi( p->pAig, pObj, i )
|
||||
pObj->pNext = Aig_ObjCreatePi( pNew );
|
||||
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
|
||||
pObjLo->pNext = Aig_ObjChild0Copy(pObjLi);
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
if ( Aig_ObjLevel(pObj) <= p->pPars->nOdcMax )
|
||||
pObj->pNext = Aig_And( pNew, Aig_ObjChild0Next(pObj), Aig_ObjChild1Next(pObj) );
|
||||
// construct clock-gating miters for each register input
|
||||
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
|
||||
pObjLi->pData = Aig_ObjCreatePo( pNew, Cgt_ManConstructMiter(p, pNew, pObjLo) );
|
||||
Aig_ManCleanNext( p->pAig );
|
||||
Aig_ManSetPioNumbers( p->pAig );
|
||||
Aig_ManCleanup( pNew );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates the AIG recursively.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
|
||||
return pObj->pData;
|
||||
Aig_ObjSetTravIdCurrent(pAig, pObj);
|
||||
if ( Aig_ObjIsPi(pObj) )
|
||||
return pObj->pData = Aig_ObjCreatePi( pNew );
|
||||
Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
|
||||
Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
|
||||
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates register outputs starting from the given one.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart )
|
||||
{
|
||||
Aig_Man_t * pNew;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
assert( Aig_ManRegNum(pAig) == 0 );
|
||||
pNew = Aig_ManStart( nVarsMin );
|
||||
Aig_ManIncrementTravId( pAig );
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
|
||||
Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
|
||||
for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pAig); i++ )
|
||||
{
|
||||
pObj = Aig_ManPo( pAig, i );
|
||||
Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
}
|
||||
for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pAig); i++ )
|
||||
{
|
||||
pObj = Aig_ManPo( pAig, i );
|
||||
Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
}
|
||||
assert( nFlopsMin >= Aig_ManPoNum(pAig) || Aig_ManPoNum(pNew) >= nFlopsMin );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives AIG after clock-gating.]
|
||||
|
||||
Description [The array contains, for each flop, its gate if present.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates )
|
||||
{
|
||||
Aig_Man_t * pNew;
|
||||
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGate, * pGateNew;
|
||||
int i;
|
||||
assert( Aig_ManRegNum(pAig) );
|
||||
pNew = Aig_ManStart( Aig_ManObjNumMax(pAig) );
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
Saig_ManForEachPo( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
{
|
||||
pGate = Vec_PtrEntry( vGates, i );
|
||||
if ( pGate == NULL )
|
||||
pObjNew = Aig_ObjChild0Copy(pObjLi);
|
||||
else
|
||||
{
|
||||
pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) );
|
||||
pObjNew = Aig_Mux( pNew, pGateNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
|
||||
}
|
||||
pObjLi->pData = Aig_ObjCreatePo( pNew, pObjNew );
|
||||
}
|
||||
Aig_ManCleanup( pNew );
|
||||
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,254 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtCore.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cgtInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_SetDefaultParams( Cgt_Par_t * p )
|
||||
{
|
||||
memset( p, 0, sizeof(Cgt_Par_t) );
|
||||
p->nLevelMax = 1000; // the max number of levels to look for clock-gates
|
||||
p->nCandMax = 1000; // the max number of candidates at each node
|
||||
p->nOdcMax = 0; // the max number of ODC levels to consider
|
||||
p->nConfMax = 1000; // the max number of conflicts at a node
|
||||
p->nVarsMin = 5000; // the min number of vars to recycle the SAT solver
|
||||
p->nFlopsMin = 25; // the min number of flops to recycle the SAT solver
|
||||
p->fVerbose = 0; // verbosity flag
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if simulation does not filter out this candidate.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandFrame, Aig_Obj_t * pMiterFrame )
|
||||
{
|
||||
unsigned * pInfoCand, * pInfoMiter;
|
||||
int w, nWords = Aig_BitWordNum( p->nPatts );
|
||||
pInfoCand = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandFrame)) );
|
||||
pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterFrame) );
|
||||
// C => !M -- true is the same as C & M -- false
|
||||
if ( !Aig_IsComplement(pCandFrame) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( pInfoCand[w] & pInfoMiter[w] )
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( ~pInfoCand[w] & pInfoMiter[w] )
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Saves one simulation pattern.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_SimulationRecord( Cgt_Man_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
Aig_ManForEachObj( p->pPart, pObj, i )
|
||||
if ( sat_solver_var_value( p->pSat, p->pCnf->pVarNums[i] ) )
|
||||
Aig_InfoSetBit( Vec_PtrEntry(p->vPatts, i), p->nPatts );
|
||||
p->nPatts++;
|
||||
if ( p->nPatts == 32 * p->nPattWords )
|
||||
{
|
||||
Vec_PtrReallocSimInfo( p->vPatts );
|
||||
p->nPattWords *= 2;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs clock-gating for the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
|
||||
{
|
||||
Vec_Ptr_t * vNodes = p->vFanout;
|
||||
Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart;
|
||||
int i, k, RetValue;
|
||||
assert( Vec_VecSize(p->vGatesAll) == Aig_ManPoNum(p->pFrame) );
|
||||
// go through all the registers inputs of this range
|
||||
for ( i = iStart; i < iStart + Aig_ManPoNum(p->pPart); i++ )
|
||||
{
|
||||
pMiter = Saig_ManLi( p->pAig, i );
|
||||
Cgt_ManDetectCandidates( p->pAig, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes );
|
||||
// go through the candidates of this PO
|
||||
Vec_PtrForEachEntry( vNodes, pCand, k )
|
||||
{
|
||||
// get the corresponding nodes from the frames
|
||||
pCandFrame = pCand->pData;
|
||||
pMiterFrame = pMiter->pData;
|
||||
// get the corresponding nodes from the part
|
||||
pCandPart = pCandFrame->pData;
|
||||
pMiterPart = pMiterFrame->pData;
|
||||
// try direct polarity
|
||||
if ( Cgt_SimulationFilter( p, pCandPart, pMiterPart ) )
|
||||
{
|
||||
RetValue = Cgt_CheckImplication( p, pCandPart, pMiterPart );
|
||||
if ( RetValue == 1 )
|
||||
{
|
||||
Vec_VecPush( p->vGatesAll, i, pCand );
|
||||
continue;
|
||||
}
|
||||
if ( RetValue == 0 )
|
||||
Cgt_SimulationRecord( p );
|
||||
}
|
||||
// try reverse polarity
|
||||
if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) )
|
||||
{
|
||||
RetValue = Cgt_CheckImplication( p, Aig_Not(pCandPart), pMiterPart );
|
||||
if ( RetValue == 1 )
|
||||
{
|
||||
Vec_VecPush( p->vGatesAll, i, Aig_Not(pCand) );
|
||||
continue;
|
||||
}
|
||||
if ( RetValue == 0 )
|
||||
Cgt_SimulationRecord( p );
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs clock-gating for the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
|
||||
{
|
||||
int iStop;
|
||||
p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart );
|
||||
p->pCnf = Cnf_DeriveSimple( p->pPart, Aig_ManPoNum(p->pPart) );
|
||||
p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
|
||||
sat_solver_compress( p->pSat );
|
||||
p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), 16 );
|
||||
Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords );
|
||||
Cgt_ClockGatingRangeCheck( p, iStart );
|
||||
iStop = iStart + Aig_ManPoNum(p->pPart);
|
||||
Cgt_ManClean( p );
|
||||
return iStop;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs clock-gating for the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
|
||||
{
|
||||
Cgt_Par_t Pars;
|
||||
Cgt_Man_t * p;
|
||||
Vec_Vec_t * vGatesAll;
|
||||
int iStart;
|
||||
if ( pPars == NULL )
|
||||
Cgt_SetDefaultParams( pPars = &Pars );
|
||||
p = Cgt_ManCreate( pAig, pCare, pPars );
|
||||
p->pFrame = Cgt_ManDeriveAigForGating( p );
|
||||
assert( Aig_ManPoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
|
||||
for ( iStart = 0; iStart < Aig_ManPoNum(p->pFrame); )
|
||||
iStart = Cgt_ClockGatingRange( p, iStart );
|
||||
vGatesAll = p->vGatesAll;
|
||||
return vGatesAll;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs clock-gating for the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
|
||||
{
|
||||
Aig_Man_t * pGated;
|
||||
Vec_Vec_t * vGatesAll;
|
||||
Vec_Ptr_t * vGates;
|
||||
vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
|
||||
vGates = Cgt_ManDecideSimple( pAig, vGatesAll );
|
||||
pGated = Cgt_ManDeriveGatedAig( pAig, vGates );
|
||||
Vec_PtrFree( vGates );
|
||||
Vec_VecFree( vGatesAll );
|
||||
return pGated;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,102 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtMan.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [Decide what gate to use for what flop.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cgtInt.h"
|
||||
#include "sswInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand );
|
||||
extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Chooses what clock-gate to use for each register.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
|
||||
{
|
||||
Vec_Ptr_t * vGates;
|
||||
vGates = Vec_PtrStart( Saig_ManRegNum(pAig) );
|
||||
return vGates;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Chooses what clock-gate to use for this register.]
|
||||
|
||||
Description [Currently uses the naive approach: For each register,
|
||||
choose the clock gate, which covers most of the transitions.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
|
||||
{
|
||||
Ssw_Sml_t * pSml;
|
||||
Vec_Ptr_t * vGates, * vCands;
|
||||
Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest;
|
||||
int i, k, nHitsCur, nHitsMax;
|
||||
vGates = Vec_PtrStart( Saig_ManRegNum(pAig) );
|
||||
pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 1 );
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
{
|
||||
nHitsMax = 0;
|
||||
pCandBest = NULL;
|
||||
vCands = Vec_VecEntry( vGatesAll, i );
|
||||
Vec_PtrForEachEntry( vCands, pCand, k )
|
||||
{
|
||||
// check if this is indeed a clock-gate
|
||||
if ( !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) )
|
||||
printf( "Clock gate candidate is invalid!\n" );
|
||||
// find its characteristic number
|
||||
nHitsCur = Ssw_SmlCountXorImplication( pSml, pObjLi, pObjLo, pCand );
|
||||
if ( nHitsMax < nHitsCur )
|
||||
{
|
||||
nHitsMax = nHitsCur;
|
||||
pCandBest = pCand;
|
||||
}
|
||||
}
|
||||
if ( pCandBest != NULL )
|
||||
Vec_PtrWriteEntry( vGates, i, pCandBest );
|
||||
}
|
||||
Ssw_SmlStop( pSml );
|
||||
return vGates;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,107 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtInt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [Internal declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __CGT_INT_H__
|
||||
#define __CGT_INT_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "saig.h"
|
||||
#include "satSolver.h"
|
||||
#include "cnf.h"
|
||||
#include "cgt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Cgt_Man_t_ Cgt_Man_t;
|
||||
struct Cgt_Man_t_
|
||||
{
|
||||
// user's data
|
||||
Cgt_Par_t * pPars; // user's parameters
|
||||
Aig_Man_t * pAig; // user's AIG manager
|
||||
Aig_Man_t * pCare; // user's constraints
|
||||
Vec_Vec_t * vGatesAll; // the computed clock-gates
|
||||
Vec_Ptr_t * vGates; // the selected clock-gates
|
||||
// internal data
|
||||
Aig_Man_t * pFrame; // clock gate AIG manager
|
||||
Vec_Ptr_t * vFanout; // temporary storage for fanouts
|
||||
// SAT solving
|
||||
Aig_Man_t * pPart; // partition
|
||||
Cnf_Dat_t * pCnf; // CNF of the partition
|
||||
sat_solver * pSat; // SAT solver
|
||||
Vec_Ptr_t * vPatts; // simulation patterns
|
||||
int nPatts; // the number of patterns accumulated
|
||||
int nPattWords; // the number of pattern words
|
||||
// statistics
|
||||
int nCalls; // total calls
|
||||
int nCallsSat; // satisfiable calls
|
||||
int nCallsUnsat; // unsatisfiable calls
|
||||
int nCallsUndec; // undecided calls
|
||||
int timeSat; // total runtime
|
||||
int timeSatSat; // satisfiable runtime
|
||||
int timeSatUnsat; // unsatisfiable runtime
|
||||
int timeSatUndec; // undecided runtime
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== cgtAig.c ==========================================================*/
|
||||
extern void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands );
|
||||
extern Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p );
|
||||
extern Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart );
|
||||
extern Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates );
|
||||
/*=== cgtDecide.c ==========================================================*/
|
||||
extern Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll );
|
||||
extern Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll );
|
||||
/*=== cgtMan.c ==========================================================*/
|
||||
extern Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
|
||||
extern void Cgt_ManClean( Cgt_Man_t * p );
|
||||
extern void Cgt_ManStop( Cgt_Man_t * p );
|
||||
/*=== cgtSat.c ==========================================================*/
|
||||
extern int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pFlop );
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,168 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtMan.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [Manipulation of clock gating manager.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cgtInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
|
||||
{
|
||||
Cgt_Man_t * p;
|
||||
// prepare the sequential AIG
|
||||
assert( Saig_ManRegNum(pAig) > 0 );
|
||||
Aig_ManFanoutStart( pAig );
|
||||
Aig_ManSetPioNumbers( pAig );
|
||||
// create interpolation manager
|
||||
p = ALLOC( Cgt_Man_t, 1 );
|
||||
memset( p, 0, sizeof(Cgt_Man_t) );
|
||||
p->pPars = pPars;
|
||||
p->pAig = pAig;
|
||||
p->vGatesAll = Vec_VecStart( Saig_ManRegNum(pAig) );
|
||||
p->vFanout = Vec_PtrAlloc( 1000 );
|
||||
p->nPattWords = 16;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManClean( Cgt_Man_t * p )
|
||||
{
|
||||
if ( p->pPart )
|
||||
{
|
||||
Aig_ManStop( p->pPart );
|
||||
p->pPart = NULL;
|
||||
}
|
||||
if ( p->pCnf )
|
||||
{
|
||||
Cnf_DataFree( p->pCnf );
|
||||
p->pCnf = NULL;
|
||||
}
|
||||
if ( p->pSat )
|
||||
{
|
||||
sat_solver_delete( p->pSat );
|
||||
p->pSat = NULL;
|
||||
}
|
||||
if ( p->vPatts )
|
||||
{
|
||||
Vec_PtrFree( p->vPatts );
|
||||
p->vPatts = NULL;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints stats of the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManPrintStats( Cgt_Man_t * p )
|
||||
{
|
||||
/*
|
||||
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
|
||||
|
||||
printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
|
||||
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, 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),
|
||||
0/p->pPars->nIters );
|
||||
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
|
||||
p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Cgt_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) );
|
||||
|
||||
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 );
|
||||
PRTP( " sat ", p->timeSatSat, p->timeTotal );
|
||||
PRTP( " undecided", p->timeSatUndec, p->timeTotal );
|
||||
PRTP( "Other ", p->timeOther, p->timeTotal );
|
||||
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
|
||||
*/
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cgt_ManStop( Cgt_Man_t * p )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Cgt_ManPrintStats( p );
|
||||
if ( p->pFrame )
|
||||
Aig_ManStop( p->pFrame );
|
||||
Cgt_ManClean( p );
|
||||
Vec_PtrFree( p->vFanout );
|
||||
Vec_PtrFree( p->vGates );
|
||||
Vec_VecFree( p->vGatesAll );
|
||||
free( p );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,92 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cgtSat.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Clock gating package.]
|
||||
|
||||
Synopsis [Checking implications using SAT.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: cgtSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cgtInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Runs equivalence test for the two nodes.]
|
||||
|
||||
Description [Both nodes should be regular and different from each other.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
|
||||
{
|
||||
int nBTLimit = p->pPars->nConfMax;
|
||||
int pLits[2], RetValue, clk;
|
||||
p->nCalls++;
|
||||
|
||||
// sanity checks
|
||||
assert( p->pSat && p->pCnf );
|
||||
assert( !Aig_IsComplement(pMiter) );
|
||||
assert( Aig_Regular(pGate) != pMiter );
|
||||
|
||||
// solve under assumptions
|
||||
// G => !M -- true G & M -- false
|
||||
pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) );
|
||||
pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 );
|
||||
|
||||
clk = clock();
|
||||
RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
|
||||
p->timeSat += clock() - clk;
|
||||
if ( RetValue == l_False )
|
||||
{
|
||||
p->timeSatUnsat += clock() - clk;
|
||||
pLits[0] = lit_neg( pLits[0] );
|
||||
pLits[1] = lit_neg( pLits[1] );
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
sat_solver_compress( p->pSat );
|
||||
p->nCallsUnsat++;
|
||||
return 1;
|
||||
}
|
||||
else if ( RetValue == l_True )
|
||||
{
|
||||
p->timeSatSat += clock() - clk;
|
||||
p->nCallsSat++;
|
||||
return 0;
|
||||
}
|
||||
else // if ( RetValue1 == l_Undef )
|
||||
{
|
||||
p->timeSatUndec += clock() - clk;
|
||||
p->nCallsUndec++;
|
||||
return -1;
|
||||
}
|
||||
return -2;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
SRC += src/aig/cgt/cgtAig.c \
|
||||
src/aig/cgt/cgtCore.c \
|
||||
src/aig/cgt/cgtDecide.c \
|
||||
src/aig/cgt/cgtMan.c \
|
||||
src/aig/cgt/cgtSat.c
|
||||
|
|
@ -174,7 +174,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
|
|||
}
|
||||
RetValue = Fra_FraigMiterStatus( pAig );
|
||||
// assert( RetValue == -1 );
|
||||
if ( RetValue >= 0 )
|
||||
if ( RetValue == 0 )
|
||||
{
|
||||
pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) );
|
||||
memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
|
||||
|
|
|
|||
|
|
@ -348,7 +348,12 @@ clk = clock();
|
|||
}
|
||||
|
||||
Aig_ManSetRegNum( pNew, pNew->nRegs );
|
||||
pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
|
||||
// pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
|
||||
if ( Aig_ManRegNum(pNew) > 0 )
|
||||
pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
|
||||
else
|
||||
pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
|
||||
|
||||
if ( pNew == NULL )
|
||||
{
|
||||
pNew = pTemp;
|
||||
|
|
|
|||
|
|
@ -140,6 +140,17 @@ struct Kit_DsdMan_t_
|
|||
Vec_Int_t * vNodes; // temporary array for BDD nodes
|
||||
};
|
||||
|
||||
#ifdef WIN32
|
||||
#define DLLEXPORT __declspec(dllexport)
|
||||
#define DLLIMPORT __declspec(dllimport)
|
||||
#else /* defined(WIN32) */
|
||||
#define DLLIMPORT
|
||||
#endif /* defined(WIN32) */
|
||||
|
||||
#ifndef ABC_DLL
|
||||
#define ABC_DLL DLLIMPORT
|
||||
#endif
|
||||
|
||||
static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
|
||||
static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; }
|
||||
static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; }
|
||||
|
|
@ -558,7 +569,7 @@ extern char * Kit_PlaStart( void * p, int nCubes, int nVars );
|
|||
extern char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover );
|
||||
extern void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover );
|
||||
extern char * Kit_PlaStoreSop( void * p, char * pSop );
|
||||
extern char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
|
||||
extern ABC_DLL char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
|
||||
/*=== kitSop.c ==========================================================*/
|
||||
extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
|
||||
extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: ntl.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
|
||||
Revision [$Id: ntl.h,v 1.3 2008/10/24 14:18:44 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
@ -308,6 +308,7 @@ extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
|
|||
extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
|
||||
extern ABC_DLL Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p );
|
||||
extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize );
|
||||
extern ABC_DLL Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
|
||||
/*=== ntlInsert.c ==========================================================*/
|
||||
extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
|
||||
extern ABC_DLL Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
|
||||
|
|
@ -323,7 +324,6 @@ extern ABC_DLL void Ntl_ManCleanup( Ntl_Man_t * p );
|
|||
extern ABC_DLL Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
|
||||
extern ABC_DLL Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
|
||||
extern ABC_DLL void Ntl_ManFree( Ntl_Man_t * p );
|
||||
extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
|
||||
extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p );
|
||||
extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
|
||||
extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p );
|
||||
|
|
@ -351,16 +351,17 @@ extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFile
|
|||
/*=== ntlSweep.c ==========================================================*/
|
||||
extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
|
||||
/*=== ntlTable.c ==========================================================*/
|
||||
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
|
||||
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
|
||||
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName );
|
||||
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName );
|
||||
extern ABC_DLL Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName );
|
||||
extern ABC_DLL void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p );
|
||||
extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber );
|
||||
extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber );
|
||||
extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
|
||||
extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
|
||||
extern ABC_DLL void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
|
||||
extern ABC_DLL int Ntl_ModelCountNets( Ntl_Mod_t * p );
|
||||
extern ABC_DLL int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel );
|
||||
extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
|
||||
extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, const char * pName );
|
||||
/*=== ntlTime.c ==========================================================*/
|
||||
extern ABC_DLL Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
|
||||
/*=== ntlReadBlif.c ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: ntlCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
Revision [$Id: ntlCheck.c,v 1.1 2008/10/10 14:09:29 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
@ -312,10 +312,11 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
|
|||
Vec_PtrPush( vNets, pNet );
|
||||
}
|
||||
|
||||
#if 0 // sjang
|
||||
// print the warning
|
||||
if ( Vec_PtrSize(vNets) > 0 )
|
||||
{
|
||||
printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pModel->pName );
|
||||
printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\": ", Vec_PtrSize(vNets), pModel->pName );
|
||||
Vec_PtrForEachEntry( vNets, pNet, i )
|
||||
{
|
||||
printf( "%s%s", (i? ", ": ""), pNet->pName );
|
||||
|
|
@ -328,6 +329,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
|
|||
}
|
||||
printf( "\n" );
|
||||
}
|
||||
#endif
|
||||
Vec_PtrFree( vNets );
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - January 8, 2007.]
|
||||
|
||||
Revision [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $]
|
||||
Revision [$Id: ntlReadBlif.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
Revision [$Id: ntlSweep.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
@ -154,8 +154,10 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
|
|||
|
||||
|
||||
// print detailed statistics of sweeping
|
||||
if ( fVerbose )
|
||||
if ( fVerbose && Counter > 0)
|
||||
{
|
||||
int numLutBox = 0;
|
||||
|
||||
printf( "Swept away:" );
|
||||
printf( " Node = %d (%4.1f %%)",
|
||||
nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE],
|
||||
|
|
@ -175,8 +177,21 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
|
|||
printf( "Sweep removed %d boxed of %d types (out of %d types):\n",
|
||||
nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], ModelCounter, Vec_PtrSize(p->vModels)-1 );
|
||||
Ntl_ManForEachModel( p, pMod, i )
|
||||
if ( i )
|
||||
printf( "Model %3d : %-40s Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems );
|
||||
{
|
||||
if ( i && (pMod->nRems + pMod->nUsed-pMod->nRems) > 0)
|
||||
{
|
||||
|
||||
if (strncmp(pMod->pName, "LUT", 3) != 0)
|
||||
{
|
||||
//printf( "( M%d: %s, S=%d, L=%d ) ", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems );
|
||||
//printf( "Model %3d : %-40s Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems );
|
||||
} else
|
||||
{
|
||||
numLutBox++;
|
||||
}
|
||||
}
|
||||
}
|
||||
printf("\nLUTboxType =%d\n", numLutBox);
|
||||
}
|
||||
}
|
||||
if ( !Ntl_ManCheck( p ) )
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: ntlTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
Revision [$Id: ntlTable.c,v 1.3 2008/10/24 14:18:44 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// hashing for strings
|
||||
static unsigned Ntl_HashString( char * pName, int TableSize )
|
||||
static unsigned Ntl_HashString( const char * pName, int TableSize )
|
||||
{
|
||||
static int s_Primes[10] = {
|
||||
1291, 1699, 2357, 4177, 5147,
|
||||
|
|
@ -52,7 +52,7 @@ static unsigned Ntl_HashString( char * pName, int TableSize )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, char * pName )
|
||||
Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, const char * pName )
|
||||
{
|
||||
Ntl_Net_t * pNet;
|
||||
pNet = (Ntl_Net_t *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, sizeof(Ntl_Net_t) + strlen(pName) + 1 );
|
||||
|
|
@ -113,7 +113,7 @@ clk = clock();
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName )
|
||||
Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName )
|
||||
{
|
||||
Ntl_Net_t * pEnt;
|
||||
unsigned Key = Ntl_HashString( pName, p->nTableSize );
|
||||
|
|
@ -163,7 +163,7 @@ void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
|
||||
Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName )
|
||||
{
|
||||
Ntl_Net_t * pEnt;
|
||||
unsigned Key = Ntl_HashString( pName, p->nTableSize );
|
||||
|
|
@ -178,6 +178,18 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
|
|||
return pEnt;
|
||||
}
|
||||
|
||||
Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName )
|
||||
{
|
||||
Ntl_Net_t * pEnt;
|
||||
unsigned Key = Ntl_HashString( pName, p->nTableSize );
|
||||
pEnt = Ntl_ModelCreateNet( p, pName );
|
||||
pEnt->pNext = p->pTable[Key];
|
||||
p->pTable[Key] = pEnt;
|
||||
if ( ++p->nEntries > 2 * p->nTableSize )
|
||||
Ntl_ModelTableResize( p );
|
||||
return pEnt;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Assigns numbers to PIs and POs.]
|
||||
|
|
@ -210,7 +222,7 @@ void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
|
||||
int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber )
|
||||
{
|
||||
Ntl_Net_t * pNet;
|
||||
Ntl_Obj_t * pObj;
|
||||
|
|
@ -273,7 +285,7 @@ int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char *
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
|
||||
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber )
|
||||
{
|
||||
Ntl_Net_t * pNet;
|
||||
Ntl_Obj_t * pTerm;
|
||||
|
|
@ -461,7 +473,7 @@ int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
|
||||
Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, const char * pName )
|
||||
{
|
||||
Ntl_Mod_t * pEnt;
|
||||
unsigned Key = Ntl_HashString( pName, p->nModTableSize );
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: nwkMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
Revision [$Id: nwkMan.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
|
@ -154,7 +154,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
|
|||
ParsBest.nPis = ParsNew.nPis;
|
||||
ParsBest.nPos = ParsNew.nPos;
|
||||
// write the network
|
||||
Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
|
||||
// Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
|
||||
// Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL );
|
||||
return 1;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -78,6 +78,8 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
|
|||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sswAbs.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose );
|
||||
/*=== saigBmc.c ==========================================================*/
|
||||
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
|
||||
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
|
||||
|
|
|
|||
|
|
@ -28,10 +28,313 @@
|
|||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { return Vec_StrGetEntry( p, nObjs*i+pObj->Id ); }
|
||||
static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 ); }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Finds the set of clauses involved in the UNSAT core.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
|
||||
{
|
||||
Vec_Int_t * vCore;
|
||||
void * pSatCnf;
|
||||
Intp_Man_t * pManProof;
|
||||
int RetValue, clk = clock();
|
||||
// solve the problem
|
||||
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
|
||||
if ( RetValue == l_Undef )
|
||||
{
|
||||
printf( "Conflict limit is reached.\n" );
|
||||
return NULL;
|
||||
}
|
||||
if ( RetValue == l_True )
|
||||
{
|
||||
printf( "The BMC problem is SAT.\n" );
|
||||
return NULL;
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
assert( RetValue == l_False );
|
||||
pSatCnf = sat_solver_store_release( pSat );
|
||||
// derive the UNSAT core
|
||||
clk = clock();
|
||||
pManProof = Intp_ManAlloc();
|
||||
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 );
|
||||
Intp_ManFree( pManProof );
|
||||
Sto_ManFree( pSatCnf );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
return vCore;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Mark visited nodes recursively.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i )
|
||||
{
|
||||
if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) )
|
||||
return 1;
|
||||
Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i );
|
||||
if ( Saig_ObjIsPi( p, pObj ) )
|
||||
return 1;
|
||||
if ( Saig_ObjIsLo( p, pObj ) )
|
||||
return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 );
|
||||
if ( Aig_ObjIsPo( pObj ) )
|
||||
return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
|
||||
Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
|
||||
Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i );
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Mark visited nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax )
|
||||
{
|
||||
Vec_Str_t * vObj2Visit;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, f;
|
||||
vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax );
|
||||
Saig_ManForEachLo( p, pObj, i )
|
||||
Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 );
|
||||
for ( f = 0; f < nFramesMax; f++ )
|
||||
{
|
||||
Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f );
|
||||
Saig_ManForEachPo( p, pObj, i )
|
||||
Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f );
|
||||
}
|
||||
return vObj2Visit;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs the actual construction of the output.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj->pData )
|
||||
return pObj->pData;
|
||||
assert( Aig_ObjIsNode(pObj) );
|
||||
Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
|
||||
Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) );
|
||||
return pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives a vector of AIG managers, one for each frame.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose )
|
||||
{
|
||||
Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs;
|
||||
Vec_Str_t * vObj2Visit;
|
||||
Aig_Man_t * pFrame;
|
||||
Aig_Obj_t * pObj;
|
||||
int f, i;
|
||||
vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax );
|
||||
vFrames = Vec_PtrAlloc( nFramesMax );
|
||||
vLoObjs = Vec_PtrAlloc( 100 );
|
||||
vLiObjs = Vec_PtrAlloc( 100 );
|
||||
for ( f = 0; f < nFramesMax; f++ )
|
||||
{
|
||||
Aig_ManCleanData( p );
|
||||
pFrame = Aig_ManStart( 1000 );
|
||||
Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame);
|
||||
// create PIs
|
||||
Vec_PtrClear( vLoObjs );
|
||||
Vec_PtrClear( vLiObjs );
|
||||
Aig_ManForEachPi( p, pObj, i )
|
||||
{
|
||||
if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
|
||||
{
|
||||
pObj->pData = Aig_ObjCreatePi(pFrame);
|
||||
if ( i >= Saig_ManPiNum(p) )
|
||||
Vec_PtrPush( vLoObjs, pObj );
|
||||
}
|
||||
}
|
||||
// remember the number of (implicit) registers in this frame
|
||||
pFrame->nAsserts = Vec_PtrSize(vLoObjs);
|
||||
// create POs
|
||||
Aig_ManForEachPo( p, pObj, i )
|
||||
if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
|
||||
{
|
||||
Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
|
||||
pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) );
|
||||
if ( i >= Saig_ManPoNum(p) )
|
||||
Vec_PtrPush( vLiObjs, pObj );
|
||||
}
|
||||
Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) );
|
||||
// set the new PIs to point to the recorresponding registers
|
||||
Aig_ManCleanData( pFrame );
|
||||
Vec_PtrForEachEntry( vLoObjs, pObj, i )
|
||||
((Aig_Obj_t *)pObj->pData)->pData = pObj;
|
||||
Vec_PtrForEachEntry( vLiObjs, pObj, i )
|
||||
((Aig_Obj_t *)pObj->pData)->pData = pObj;
|
||||
if ( fVerbose )
|
||||
printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n",
|
||||
f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) );
|
||||
}
|
||||
Vec_PtrFree( vLoObjs );
|
||||
Vec_PtrFree( vLiObjs );
|
||||
Vec_StrFree( vObj2Visit );
|
||||
return vFrames;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives a vector of AIG managers, one for each frame.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Cnf_Dat_t * pCnf, * pCnfPrev;
|
||||
Vec_Int_t * vPoLits;
|
||||
Aig_Obj_t * pObjPo, * pObjLi, * pObjLo;
|
||||
int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters;
|
||||
// start array of output literals
|
||||
vPoLits = Vec_IntAlloc( 100 );
|
||||
// count the number of CNF variables
|
||||
nSatVars = 0;
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, f )
|
||||
nSatVars += pCnf->nVars;
|
||||
|
||||
// create the SAT solver
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_store_alloc( pSat );
|
||||
sat_solver_setnvars( pSat, nSatVars );
|
||||
|
||||
// add clauses for the timeframes
|
||||
nSatVars = 0;
|
||||
// Vec_PtrForEachEntryReverse( vFrames, pCnf, f )
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, f )
|
||||
{
|
||||
// lift clauses of this CNF
|
||||
Cnf_DataLift( pCnf, nSatVars );
|
||||
nSatVars += pCnf->nVars;
|
||||
// copy clauses into the manager
|
||||
for ( i = 0; i < pCnf->nClauses; i++ )
|
||||
{
|
||||
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
|
||||
{
|
||||
printf( "The BMC problem is trivially UNSAT.\n" );
|
||||
sat_solver_delete( pSat );
|
||||
Vec_IntFree( vPoLits );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
// remember output literal
|
||||
Aig_ManForEachPo( pCnf->pMan, pObjPo, i )
|
||||
{
|
||||
if ( i == Saig_ManPoNum(p) )
|
||||
break;
|
||||
Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) );
|
||||
}
|
||||
}
|
||||
|
||||
// add auxiliary clauses (output, connectors, initial)
|
||||
// add output clause
|
||||
if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
|
||||
assert( 0 );
|
||||
Vec_IntFree( vPoLits );
|
||||
|
||||
// add connecting clauses
|
||||
pCnfPrev = Vec_PtrEntry( vFrames, 0 );
|
||||
Vec_PtrForEachEntryStart( vFrames, pCnf, f, 1 )
|
||||
{
|
||||
nRegisters = pCnf->pMan->nAsserts;
|
||||
assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) );
|
||||
assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) );
|
||||
for ( i = 0; i < nRegisters; i++ )
|
||||
{
|
||||
pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i );
|
||||
pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i );
|
||||
// get variable numbers
|
||||
iVarOld = pCnfPrev->pVarNums[pObjLi->Id];
|
||||
iVarNew = pCnf->pVarNums[pObjLo->Id];
|
||||
// add clauses connecting existing variables
|
||||
Lits[0] = toLitCond( iVarOld, 0 );
|
||||
Lits[1] = toLitCond( iVarNew, 1 );
|
||||
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||
assert( 0 );
|
||||
Lits[0] = toLitCond( iVarOld, 1 );
|
||||
Lits[1] = toLitCond( iVarNew, 0 );
|
||||
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||
assert( 0 );
|
||||
}
|
||||
pCnfPrev = pCnf;
|
||||
}
|
||||
// add unit clauses
|
||||
pCnf = Vec_PtrEntry( vFrames, 0 );
|
||||
nRegisters = pCnf->pMan->nAsserts;
|
||||
for ( i = 0; i < nRegisters; i++ )
|
||||
{
|
||||
pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i );
|
||||
assert( pCnf->pVarNums[pObjLo->Id] >= 0 );
|
||||
Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 );
|
||||
if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
|
||||
assert( 0 );
|
||||
}
|
||||
sat_solver_store_mark_roots( pSat );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates SAT solver for BMC.]
|
||||
|
|
@ -123,7 +426,7 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
|
|||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Finds the set of clauses involved in the UNSAT core.]
|
||||
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
|
||||
|
||||
Description []
|
||||
|
||||
|
|
@ -132,37 +435,78 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
|
||||
Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore )
|
||||
{
|
||||
Vec_Int_t * vCore;
|
||||
void * pSatCnf;
|
||||
Intp_Man_t * pManProof;
|
||||
int RetValue;
|
||||
// solve the problem
|
||||
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
|
||||
if ( RetValue == l_Undef )
|
||||
Aig_Obj_t * pObj;
|
||||
Cnf_Dat_t * pCnf;
|
||||
Vec_Int_t * vFlops;
|
||||
int * pVars, * pFlops;
|
||||
int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses;
|
||||
// count the number of CNF variables
|
||||
nSatVars = 0;
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, f )
|
||||
nSatVars += pCnf->nVars;
|
||||
// mark register variables
|
||||
pVars = ALLOC( int, nSatVars );
|
||||
for ( i = 0; i < nSatVars; i++ )
|
||||
pVars[i] = -1;
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, f )
|
||||
{
|
||||
printf( "Conflict limit is reached.\n" );
|
||||
return NULL;
|
||||
Aig_ManForEachPi( pCnf->pMan, pObj, i )
|
||||
{
|
||||
assert( pCnf->pVarNums[pObj->Id] >= 0 );
|
||||
assert( pCnf->pVarNums[pObj->Id] < nSatVars );
|
||||
if ( pObj->pData == NULL )
|
||||
continue;
|
||||
iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPiNum(p);
|
||||
assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
|
||||
pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
|
||||
}
|
||||
Aig_ManForEachPo( pCnf->pMan, pObj, i )
|
||||
{
|
||||
assert( pCnf->pVarNums[pObj->Id] >= 0 );
|
||||
assert( pCnf->pVarNums[pObj->Id] < nSatVars );
|
||||
if ( pObj->pData == NULL )
|
||||
continue;
|
||||
iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPoNum(p);
|
||||
assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
|
||||
pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
|
||||
}
|
||||
}
|
||||
if ( RetValue == l_True )
|
||||
// mark used registers
|
||||
pFlops = CALLOC( int, Aig_ManRegNum(p) );
|
||||
Vec_IntForEachEntry( vCore, iClause, i )
|
||||
{
|
||||
printf( "The BMC problem is SAT.\n" );
|
||||
return NULL;
|
||||
nSatClauses = 0;
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, f )
|
||||
{
|
||||
if ( iClause < nSatClauses + pCnf->nClauses )
|
||||
break;
|
||||
nSatClauses += pCnf->nClauses;
|
||||
}
|
||||
if ( f == Vec_PtrSize(vFrames) )
|
||||
continue;
|
||||
iClause = iClause - nSatClauses;
|
||||
assert( iClause >= 0 );
|
||||
assert( iClause < pCnf->nClauses );
|
||||
// consider the clause
|
||||
for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ )
|
||||
{
|
||||
iReg = pVars[ lit_var(*piLit) ];
|
||||
if ( iReg >= 0 )
|
||||
pFlops[iReg] = 1;
|
||||
}
|
||||
}
|
||||
if ( fVerbose )
|
||||
printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
|
||||
assert( RetValue == l_False );
|
||||
pSatCnf = sat_solver_store_release( pSat );
|
||||
// derive the UNSAT core
|
||||
pManProof = Intp_ManAlloc();
|
||||
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
|
||||
Intp_ManFree( pManProof );
|
||||
Sto_ManFree( pSatCnf );
|
||||
return vCore;
|
||||
// collect registers
|
||||
vFlops = Vec_IntAlloc( Aig_ManRegNum(p) );
|
||||
for ( i = 0; i < Aig_ManRegNum(p); i++ )
|
||||
if ( pFlops[i] )
|
||||
Vec_IntPush( vFlops, i );
|
||||
free( pFlops );
|
||||
free( pVars );
|
||||
return vFlops;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
|
||||
|
|
@ -225,39 +569,139 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t *
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
|
||||
void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames )
|
||||
{
|
||||
Cnf_Dat_t * pCnf;
|
||||
int i;
|
||||
Vec_PtrForEachEntry( vFrames, pCnf, i )
|
||||
{
|
||||
Aig_ManStop( pCnf->pMan );
|
||||
Cnf_DataFree( pCnf );
|
||||
}
|
||||
Vec_PtrFree( vFrames );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops )
|
||||
{
|
||||
Vec_Ptr_t * vFlopPtrs, * vSupp;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, Entry;
|
||||
// collect latch inputs
|
||||
vFlopPtrs = Vec_PtrAlloc( 1000 );
|
||||
Vec_IntForEachEntry( vFlops, Entry, i )
|
||||
{
|
||||
Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) );
|
||||
pObj = Saig_ManLo(p, Entry);
|
||||
pObj->fMarkA = 1;
|
||||
}
|
||||
// collect latch outputs
|
||||
vSupp = Vec_PtrAlloc( 1000 );
|
||||
Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp );
|
||||
Vec_PtrFree( vFlopPtrs );
|
||||
// mark influencing flops
|
||||
Vec_PtrForEachEntry( vSupp, pObj, i )
|
||||
pObj->fMarkA = 1;
|
||||
Vec_PtrFree( vSupp );
|
||||
// reload flops
|
||||
Vec_IntClear( vFlops );
|
||||
Aig_ManForEachPi( p, pObj, i )
|
||||
{
|
||||
if ( pObj->fMarkA == 0 )
|
||||
continue;
|
||||
pObj->fMarkA = 0;
|
||||
if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 )
|
||||
Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pResult;
|
||||
Cnf_Dat_t * pCnf;
|
||||
Vec_Ptr_t * vFrames;
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vCore;
|
||||
Vec_Int_t * vFlops;
|
||||
int clk = clock();
|
||||
int clk = clock(), clk2 = clock();
|
||||
assert( Aig_ManRegNum(p) > 0 );
|
||||
Aig_ManSetPioNumbers( p );
|
||||
if ( fVerbose )
|
||||
printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
|
||||
// create CNF for the AIG
|
||||
pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
|
||||
// create SAT solver for the unrolled AIG
|
||||
pSat = Saig_AbsCreateSolver( pCnf, nFrames );
|
||||
if ( fDynamic )
|
||||
{
|
||||
// create CNF for the frames
|
||||
vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose );
|
||||
// create dynamic solver
|
||||
pSat = Saig_AbsCreateSolverDyn( p, vFrames );
|
||||
}
|
||||
else
|
||||
{
|
||||
// create CNF for the AIG
|
||||
pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
|
||||
// create SAT solver for the unrolled AIG
|
||||
pSat = Saig_AbsCreateSolver( pCnf, nFrames );
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses );
|
||||
PRT( "Time", clock() - clk2 );
|
||||
}
|
||||
// compute UNSAT core
|
||||
vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
|
||||
sat_solver_delete( pSat );
|
||||
if ( vCore == NULL )
|
||||
{
|
||||
Cnf_DataFree( pCnf );
|
||||
Saig_AbsFreeCnfs( vFrames );
|
||||
return NULL;
|
||||
}
|
||||
// collect registers
|
||||
vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
|
||||
Cnf_DataFree( pCnf );
|
||||
if ( fDynamic )
|
||||
{
|
||||
vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
|
||||
Saig_AbsFreeCnfs( vFrames );
|
||||
}
|
||||
else
|
||||
{
|
||||
vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
|
||||
Cnf_DataFree( pCnf );
|
||||
}
|
||||
Vec_IntFree( vCore );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
|
||||
printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
// extend the abstraction
|
||||
if ( fExtend )
|
||||
{
|
||||
if ( fVerbose )
|
||||
printf( "Support extended from %d flops to", Vec_IntSize(vFlops) );
|
||||
Saig_AbsExtendOneStep( p, vFlops );
|
||||
if ( fVerbose )
|
||||
printf( " %d flops.\n", Vec_IntSize(vFlops) );
|
||||
}
|
||||
// create the resulting AIG
|
||||
pResult = Saig_ManAbstraction( p, vFlops );
|
||||
Vec_IntFree( vFlops );
|
||||
|
|
@ -265,6 +709,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
|
|||
}
|
||||
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ struct Saig_Bmc_t_
|
|||
Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
|
||||
// subproblems
|
||||
Vec_Ptr_t * vTargets; // targets to be solved in this interval
|
||||
int iFramePrev; // previous frame
|
||||
int iFrameLast; // last frame
|
||||
int iOutputLast; // last output
|
||||
int iFrameFail; // failed frame
|
||||
|
|
@ -251,6 +252,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
|
|||
// int i;
|
||||
int nNodes = Aig_ManObjNum( p->pFrm );
|
||||
Vec_PtrClear( p->vTargets );
|
||||
p->iFramePrev = p->iFrameLast;
|
||||
for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
|
||||
{
|
||||
if ( p->iOutputLast == 0 )
|
||||
|
|
@ -573,7 +575,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
|
|||
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
|
||||
p->iOutputFail, p->iFrameFail );
|
||||
else // if ( RetValue == l_False || RetValue == l_Undef )
|
||||
printf( "No output was asserted in %d frames. ", p->iFrameLast );
|
||||
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
|
||||
PRT( "Time", clock() - clk );
|
||||
if ( RetValue != l_True )
|
||||
{
|
||||
|
|
|
|||
|
|
@ -635,7 +635,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
|
|||
Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames )
|
||||
{
|
||||
Aig_Man_t * pFrames0, * pFrames1, * pMiter;
|
||||
assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
|
||||
// assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
|
||||
pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames );
|
||||
pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames );
|
||||
pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 );
|
||||
|
|
@ -790,9 +790,9 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
|
|||
{
|
||||
Aig_ManPrintStats( pPart0 );
|
||||
Aig_ManPrintStats( pPart1 );
|
||||
// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
|
||||
// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
|
||||
// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
|
||||
Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
|
||||
Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
|
||||
printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
|
||||
}
|
||||
RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
|
||||
Aig_ManStop( pPart0 );
|
||||
|
|
|
|||
|
|
@ -90,8 +90,6 @@ struct Ssw_Cex_t_
|
|||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== sswAbs.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
|
||||
/*=== sswBmc.c ==========================================================*/
|
||||
extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
|
||||
/*=== sswCore.c ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -480,6 +480,100 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
|
|||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Takes the set of const1 cands and rehashes them using sim info.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
|
||||
{
|
||||
Aig_Man_t * pAig = p->pAig;
|
||||
Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
|
||||
Aig_Obj_t * pObj, * pTemp, * pRepr;
|
||||
int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
|
||||
|
||||
// allocate the hash table hashing simulation info into nodes
|
||||
nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 );
|
||||
ppTable = CALLOC( Aig_Obj_t *, nTableSize );
|
||||
ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
|
||||
|
||||
// sort through the candidates
|
||||
nEntries = 0;
|
||||
p->nCands1 = 0;
|
||||
Vec_PtrForEachEntry( vCands, pObj, i )
|
||||
{
|
||||
assert( p->pClassSizes[pObj->Id] == 0 );
|
||||
Aig_ObjSetRepr( p->pAig, pObj, NULL );
|
||||
// check if the node belongs to the class of constant 1
|
||||
if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
|
||||
{
|
||||
Ssw_ObjSetConst1Cand( p->pAig, pObj );
|
||||
p->nCands1++;
|
||||
continue;
|
||||
}
|
||||
// hash the node by its simulation info
|
||||
iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
|
||||
// add the node to the class
|
||||
if ( ppTable[iEntry] == NULL )
|
||||
{
|
||||
ppTable[iEntry] = pObj;
|
||||
}
|
||||
else
|
||||
{
|
||||
// set the representative of this node
|
||||
pRepr = ppTable[iEntry];
|
||||
Aig_ObjSetRepr( p->pAig, pObj, pRepr );
|
||||
// add node to the table
|
||||
if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
|
||||
{ // this will be the second entry
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
// add the entry to the list
|
||||
Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
|
||||
Ssw_ObjSetNext( ppNexts, pRepr, pObj );
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
}
|
||||
|
||||
// copy the entries into storage in the topological order
|
||||
nEntries2 = 0;
|
||||
Vec_PtrForEachEntry( vCands, pObj, i )
|
||||
{
|
||||
nNodes = p->pClassSizes[pObj->Id];
|
||||
// skip the nodes that are not representatives of non-trivial classes
|
||||
if ( nNodes == 0 )
|
||||
continue;
|
||||
assert( nNodes > 1 );
|
||||
// add the nodes to the class in the topological order
|
||||
ppClassNew = p->pMemClassesFree + nEntries2;
|
||||
ppClassNew[0] = pObj;
|
||||
for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
|
||||
pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
|
||||
{
|
||||
ppClassNew[nNodes-k] = pTemp;
|
||||
}
|
||||
// add the class of nodes
|
||||
p->pClassSizes[pObj->Id] = 0;
|
||||
Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
|
||||
// increment the number of entries
|
||||
nEntries2 += nNodes;
|
||||
}
|
||||
p->pMemClassesFree += nEntries2;
|
||||
assert( nEntries == nEntries2 );
|
||||
free( ppTable );
|
||||
free( ppNexts );
|
||||
// now it is time to refine the classes
|
||||
return Ssw_ClassesRefine( p, 1 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates initial simulation classes.]
|
||||
|
|
@ -506,10 +600,9 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs,
|
|||
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, RetValue;
|
||||
int clk;
|
||||
Vec_Ptr_t * vCands;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, k, RetValue, clk;
|
||||
|
||||
// start the classes
|
||||
p = Ssw_ClassesStart( pAig );
|
||||
|
|
@ -519,7 +612,7 @@ clk = clock();
|
|||
pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Allocated %.2f Mb for simulation information.\n",
|
||||
printf( "Allocated %.2f Mb to store 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 );
|
||||
|
|
@ -529,13 +622,8 @@ if ( fVerbose )
|
|||
clk = clock();
|
||||
Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
|
||||
|
||||
// allocate the hash table hashing simulation info into nodes
|
||||
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
|
||||
ppTable = CALLOC( Aig_Obj_t *, nTableSize );
|
||||
ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
|
||||
|
||||
// add all the nodes to the hash table
|
||||
nEntries = 0;
|
||||
// collect nodes to be considered as candidates
|
||||
vCands = Vec_PtrAlloc( 1000 );
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
{
|
||||
if ( fLatchCorr )
|
||||
|
|
@ -551,72 +639,15 @@ clk = clock();
|
|||
if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
|
||||
continue;
|
||||
}
|
||||
// check if the node belongs to the class of constant 1
|
||||
if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
|
||||
{
|
||||
Ssw_ObjSetConst1Cand( p->pAig, pObj );
|
||||
p->nCands1++;
|
||||
continue;
|
||||
}
|
||||
// hash the node by its simulation info
|
||||
iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
|
||||
// add the node to the class
|
||||
if ( ppTable[iEntry] == NULL )
|
||||
ppTable[iEntry] = pObj;
|
||||
else
|
||||
{
|
||||
// set the representative of this node
|
||||
pRepr = ppTable[iEntry];
|
||||
Aig_ObjSetRepr( p->pAig, pObj, pRepr );
|
||||
// add node to the table
|
||||
if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
|
||||
{ // this will be the second entry
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
// add the entry to the list
|
||||
Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
|
||||
Ssw_ObjSetNext( ppNexts, pRepr, pObj );
|
||||
p->pClassSizes[pRepr->Id]++;
|
||||
nEntries++;
|
||||
}
|
||||
Vec_PtrPush( vCands, pObj );
|
||||
}
|
||||
|
||||
// allocate room for classes
|
||||
p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
|
||||
p->pMemClassesFree = p->pMemClasses + nEntries;
|
||||
|
||||
// copy the entries into storage in the topological order
|
||||
nEntries2 = 0;
|
||||
Aig_ManForEachObj( p->pAig, pObj, i )
|
||||
{
|
||||
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
|
||||
continue;
|
||||
nNodes = p->pClassSizes[pObj->Id];
|
||||
// skip the nodes that are not representatives of non-trivial classes
|
||||
if ( nNodes == 0 )
|
||||
continue;
|
||||
assert( nNodes > 1 );
|
||||
// add the nodes to the class in the topological order
|
||||
ppClassNew = p->pMemClasses + nEntries2;
|
||||
ppClassNew[0] = pObj;
|
||||
for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
|
||||
pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
|
||||
{
|
||||
ppClassNew[nNodes-k] = pTemp;
|
||||
}
|
||||
// add the class of nodes
|
||||
p->pClassSizes[pObj->Id] = 0;
|
||||
Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
|
||||
// increment the number of entries
|
||||
nEntries2 += nNodes;
|
||||
}
|
||||
assert( nEntries == nEntries2 );
|
||||
free( ppTable );
|
||||
free( ppNexts );
|
||||
p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
|
||||
p->pMemClassesFree = p->pMemClasses;
|
||||
|
||||
// now it is time to refine the classes
|
||||
Ssw_ClassesRefine( p, 1 );
|
||||
Ssw_ClassesPrepareRehash( p, vCands );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Collecting candidate equivalence classes. " );
|
||||
|
|
@ -625,27 +656,30 @@ PRT( "Time", clock() - clk );
|
|||
|
||||
clk = clock();
|
||||
// perform iterative refinement using simulation
|
||||
k = 0;
|
||||
for ( i = 1; i < nIters; i++ )
|
||||
{
|
||||
// collect const1 candidates
|
||||
Vec_PtrClear( vCands );
|
||||
Aig_ManForEachObj( p->pAig, pObj, k )
|
||||
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
|
||||
Vec_PtrPush( vCands, pObj );
|
||||
assert( Vec_PtrSize(vCands) == p->nCands1 );
|
||||
// perform new round of simulation
|
||||
Ssw_SmlResimulateSeq( pSml );
|
||||
// simulate internal nodes
|
||||
Ssw_SmlSimulateOne( pSml );
|
||||
// check equivalence classes
|
||||
RetValue = Ssw_ClassesRefineConst1( p, 1 );
|
||||
RetValue += Ssw_ClassesRefine( p, 1 );
|
||||
k++;
|
||||
RetValue = Ssw_ClassesPrepareRehash( p, vCands );
|
||||
if ( RetValue == 0 )
|
||||
break;
|
||||
}
|
||||
Ssw_ClassesCheck( p );
|
||||
Ssw_SmlStop( pSml );
|
||||
Vec_PtrFree( vCands );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Simulation of %d frames with %d words (%2d rounds). ",
|
||||
nFrames, nWords, k );
|
||||
nFrames, nWords, i-1 );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
Ssw_ClassesCheck( p );
|
||||
// Ssw_ClassesPrint( p, 0 );
|
||||
return p;
|
||||
}
|
||||
|
|
@ -848,7 +882,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
|
|||
{
|
||||
Aig_Obj_t ** pClassOld, ** pClassNew;
|
||||
Aig_Obj_t * pObj, * pReprNew;
|
||||
int i;
|
||||
int i;
|
||||
|
||||
// split the class
|
||||
Vec_PtrClear( p->vClassOld );
|
||||
|
|
|
|||
|
|
@ -150,7 +150,7 @@ clk = clock();
|
|||
RetValue = Ssw_ManSweepLatch( p );
|
||||
if ( p->pPars->fVerbose )
|
||||
{
|
||||
printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ",
|
||||
printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
|
||||
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
|
||||
p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
|
||||
p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
|
||||
|
|
@ -174,11 +174,13 @@ clk = clock();
|
|||
else if ( p->pPars->fDynamic )
|
||||
{
|
||||
printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
|
||||
printf( "R =%3d. ", p->nRecycles-nRecycles );
|
||||
printf( "R =%4d. ", p->nRecycles-nRecycles );
|
||||
}
|
||||
printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal );
|
||||
printf( "F =%5d. ", p->nSatFailsReal-nSatFailsReal );
|
||||
PRT( "T", clock() - clk );
|
||||
}
|
||||
// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
|
||||
// p->pPars->nBTLimit = 10000;
|
||||
}
|
||||
nSatProof = p->nSatProof;
|
||||
nSatCallsSat = p->nSatCallsSat;
|
||||
|
|
|
|||
|
|
@ -61,6 +61,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|
|||
// other
|
||||
p->vNewLos = Vec_PtrAlloc( 100 );
|
||||
p->vNewPos = Vec_IntAlloc( 100 );
|
||||
|
||||
// p->pPars->fVerbose = 1;
|
||||
return p;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -185,6 +185,70 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
|
|||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks implication.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand )
|
||||
{
|
||||
unsigned * pSimLi, * pSimLo, * pSimCand;
|
||||
int k;
|
||||
pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
|
||||
pSimLi = Ssw_ObjSim( p, pObjLi->Id );
|
||||
pSimLo = Ssw_ObjSim( p, pObjLo->Id );
|
||||
if ( !Aig_IsComplement(pCand) )
|
||||
{
|
||||
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
|
||||
if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
|
||||
if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts the number of 1s in the implication.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand )
|
||||
{
|
||||
unsigned * pSimLi, * pSimLo, * pSimCand;
|
||||
int k, Counter = 0;
|
||||
pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
|
||||
pSimLi = Ssw_ObjSim( p, pObjLi->Id );
|
||||
pSimLo = Ssw_ObjSim( p, pObjLo->Id );
|
||||
if ( !Aig_IsComplement(pCand) )
|
||||
{
|
||||
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
|
||||
Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
|
||||
Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
|
||||
}
|
||||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if simulation info is composed of all zeros.]
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@
|
|||
#include "int.h"
|
||||
#include "dch.h"
|
||||
#include "ssw.h"
|
||||
#include "cgt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -200,6 +201,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg
|
|||
static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -470,6 +472,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
|
||||
|
|
@ -7941,7 +7944,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
*/
|
||||
|
||||
|
||||
/*
|
||||
pNtkRes = Abc_NtkDarTestNtk( pNtk );
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
|
|
@ -7950,9 +7953,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
*/
|
||||
|
||||
|
||||
// Abc_NtkDarTest( pNtk );
|
||||
Abc_NtkDarTest( pNtk );
|
||||
|
||||
return 0;
|
||||
usage:
|
||||
|
|
@ -14634,6 +14637,162 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
FILE * pOut, * pErr;
|
||||
Cgt_Par_t Pars, * pPars = &Pars;
|
||||
Abc_Ntk_t * pNtkRes, * pNtk, * pNtkCare;
|
||||
int c;
|
||||
|
||||
extern Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
Cgt_SetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "LNDCVKvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'L':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nLevelMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nLevelMax <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'N':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nCandMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nCandMax <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'D':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nOdcMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nOdcMax <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nConfMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nConfMax <= 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->nVarsMin = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nVarsMin <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'K':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nFlopsMin = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nFlopsMin <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pErr, "Empty network.\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
if ( argc == globalUtilOptind + 1 )
|
||||
{
|
||||
pNtkCare = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 );
|
||||
if ( pNtkCare == NULL )
|
||||
{
|
||||
printf( "Reading care network has failed.\n" );
|
||||
return 1;
|
||||
}
|
||||
// modify the current network
|
||||
pNtkRes = Abc_NtkDarClockGate( pNtk, pNtkCare, pPars );
|
||||
Abc_NtkDelete( pNtkCare );
|
||||
}
|
||||
else if ( argc == globalUtilOptind )
|
||||
{
|
||||
pNtkRes = Abc_NtkDarClockGate( pNtk, NULL, pPars );
|
||||
}
|
||||
else
|
||||
{
|
||||
fprintf( pErr, "Wrong number of arguments.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Clock gating has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: clockgate [-LNDCVK <num>] [-vh] <file>\n" );
|
||||
fprintf( pErr, "\t sequential clock gating with observability don't-cares\n" );
|
||||
fprintf( pErr, "\t-L num : max level number of a clock gate [default = %d]\n", pPars->nLevelMax );
|
||||
fprintf( pErr, "\t-N num : max number of candidates for a flop [default = %d]\n", pPars->nCandMax );
|
||||
fprintf( pErr, "\t-D num : max number of ODC levels to consider [default = %d]\n", pPars->nOdcMax );
|
||||
fprintf( pErr, "\t-C num : max number of conflicts at a node [default = %d]\n", pPars->nConfMax );
|
||||
fprintf( pErr, "\t-V num : min number of vars to recycle SAT solver [default = %d]\n", pPars->nVarsMin );
|
||||
fprintf( pErr, "\t-K num : min number of flops to recycle SAT solver [default = %d]\n", pPars->nFlopsMin );
|
||||
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
fprintf( pErr, "\tfile : (optional) constraints for primary inputs and register outputs\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
@ -16239,11 +16398,11 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
nFrames = 1000;
|
||||
nFrames = 2000;
|
||||
nSizeMax = 200000;
|
||||
nBTLimit = 10000;
|
||||
nBTLimitAll = 10000000;
|
||||
nNodeDelta = 1000;
|
||||
nBTLimit = 2000;
|
||||
nBTLimitAll = 2000000;
|
||||
nNodeDelta = 2000;
|
||||
fRewrite = 0;
|
||||
fNewAlgo = 0;
|
||||
fVerbose = 0;
|
||||
|
|
@ -16896,9 +17055,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Ntk_t * pNtk, * pNtkRes;
|
||||
int nFramesMax;
|
||||
int nConfMax;
|
||||
int fDynamic;
|
||||
int fExtend;
|
||||
int fVerbose;
|
||||
int c;
|
||||
extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
|
||||
extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
|
|
@ -16907,9 +17068,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
// set defaults
|
||||
nFramesMax = 10;
|
||||
nConfMax = 10000;
|
||||
fVerbose = 1;
|
||||
fDynamic = 1;
|
||||
fExtend = 0;
|
||||
fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -16935,6 +17098,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( nConfMax < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'd':
|
||||
fDynamic ^= 1;
|
||||
break;
|
||||
case 'e':
|
||||
fExtend ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
|
|
@ -16961,7 +17130,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
|
||||
// modify the current network
|
||||
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fVerbose );
|
||||
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Target enlargement has failed.\n" );
|
||||
|
|
@ -16971,10 +17140,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
usage:
|
||||
fprintf( pErr, "usage: abs [-FC num] [-vh]\n" );
|
||||
fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
|
||||
fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" );
|
||||
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
|
||||
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
|
||||
fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
|
||||
fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
|
||||
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@
|
|||
#include "int.h"
|
||||
#include "dch.h"
|
||||
#include "ssw.h"
|
||||
#include "cgt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -2189,10 +2190,8 @@ PRT( "Time", clock() - clkTotal );
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
|
||||
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
|
||||
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
|
|
@ -2201,7 +2200,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
|
|||
return NULL;
|
||||
|
||||
Aig_ManSetRegNum( pMan, pMan->nRegs );
|
||||
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
|
||||
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
|
|
@ -2552,6 +2551,44 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i
|
|||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs phase abstraction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars )
|
||||
{
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
|
||||
pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
if ( pMan1 == NULL )
|
||||
return NULL;
|
||||
if ( pCare )
|
||||
{
|
||||
pMan2 = Abc_NtkToDar( pCare, 0, 0 );
|
||||
if ( pMan2 == NULL )
|
||||
{
|
||||
Aig_ManStop( pMan1 );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
pMan = Cgt_ClockGating( pMan1, pMan2, pPars );
|
||||
Aig_ManStop( pMan1 );
|
||||
if ( pMan2 )
|
||||
Aig_ManStop( pMan2 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
|
||||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs phase abstraction.]
|
||||
|
|
@ -2677,7 +2714,7 @@ Aig_ManPrintStats( pMan );
|
|||
pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
|
||||
Aig_ManStop( pTemp );
|
||||
*/
|
||||
Ssw_SecSpecialMiter( pMan, 0 );
|
||||
Ssw_SecSpecialMiter( pMan, 1 );
|
||||
|
||||
Aig_ManStop( pMan );
|
||||
}
|
||||
|
|
@ -2708,6 +2745,8 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
|
|||
Aig_ManSetRegNum( pMan, pMan->nRegs );
|
||||
pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
|
||||
pNtkAig = Abc_NtkFromAigPhase( pMan );
|
||||
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
|
||||
|
|
@ -2715,8 +2754,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
|
|||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
*/
|
||||
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
|
||||
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
|
|
@ -2725,7 +2762,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
|
|||
return NULL;
|
||||
|
||||
Aig_ManSetRegNum( pMan, pMan->nRegs );
|
||||
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 1 );
|
||||
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 1 );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
|
|
|
|||
|
|
@ -79,6 +79,10 @@ struct Abc_Frame_t_
|
|||
void * pAbc8Nwk; // the current mapped network
|
||||
void * pAbc8Aig; // the current AIG
|
||||
void * pAbc8Lib; // the current LUT library
|
||||
|
||||
// the addition to keep the best Ntl that can be used to restore
|
||||
void * pAbc8NtlBestDelay; // the best delay, Ntl
|
||||
void * pAbc8NtlBestArea; // the best area
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -212,6 +212,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
|
|||
pPinPerm[i] = pPinPerm[best_i];
|
||||
pPinPerm[best_i] = temp;
|
||||
}
|
||||
/*
|
||||
// verify
|
||||
assert( pPinPerm[0] < (int)pCut->nLeaves );
|
||||
for ( i = 1; i < (int)pCut->nLeaves; i++ )
|
||||
|
|
@ -219,6 +220,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
|
|||
assert( pPinPerm[i] < (int)pCut->nLeaves );
|
||||
assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
|
|||
|
|
@ -32,7 +32,9 @@ extern "C" {
|
|||
#include <time.h>
|
||||
#include <math.h>
|
||||
|
||||
#define EXTERN extern
|
||||
#ifndef EXTERN
|
||||
#define EXTERN extern
|
||||
#endif
|
||||
#define NIL(type) ((type *) 0)
|
||||
#define random rand
|
||||
#define srandom srand
|
||||
|
|
|
|||
|
|
@ -336,13 +336,72 @@ static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry )
|
||||
static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Fill )
|
||||
{
|
||||
int i;
|
||||
Vec_StrGrow( p, nSize );
|
||||
p->nSize = nSize;
|
||||
for ( i = 0; i < p->nSize; i++ )
|
||||
p->pArray[i] = Entry;
|
||||
p->pArray[i] = Fill;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Fills the vector with given number of entries.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_StrFillExtra( Vec_Str_t * p, int nSize, char Fill )
|
||||
{
|
||||
int i;
|
||||
if ( p->nSize >= nSize )
|
||||
return;
|
||||
if ( 2 * p->nSize > nSize )
|
||||
Vec_StrGrow( p, 2 * nSize );
|
||||
else
|
||||
Vec_StrGrow( p, nSize );
|
||||
for ( i = p->nSize; i < nSize; i++ )
|
||||
p->pArray[i] = Fill;
|
||||
p->nSize = nSize;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the entry even if the place not exist.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline char Vec_StrGetEntry( Vec_Str_t * p, int i )
|
||||
{
|
||||
Vec_StrFillExtra( p, i + 1, 0 );
|
||||
return Vec_StrEntry( p, i );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Inserts the entry even if the place does not exist.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_StrSetEntry( Vec_Str_t * p, int i, char Entry )
|
||||
{
|
||||
Vec_StrFillExtra( p, i + 1, 0 );
|
||||
Vec_StrWriteEntry( p, i, Entry );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
|
|||
|
|
@ -210,5 +210,13 @@ static void sat_solver_act_var_clear(sat_solver* s)
|
|||
s->activity[i] = 0.0;
|
||||
s->var_inc = 1.0;
|
||||
}
|
||||
static void sat_solver_compress(sat_solver* s)
|
||||
{
|
||||
if ( s->qtail != s->qhead )
|
||||
{
|
||||
int RetValue = sat_solver_simplify(s);
|
||||
assert( RetValue != 0 );
|
||||
}
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Reference in New Issue