summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile2
-rw-r--r--abc.dsp36
-rw-r--r--src/aig/aig/aig.h3
-rw-r--r--src/aig/aig/aigUtil.c19
-rw-r--r--src/aig/cgt/cgt.h81
-rw-r--r--src/aig/cgt/cgtAig.c311
-rw-r--r--src/aig/cgt/cgtCore.c254
-rw-r--r--src/aig/cgt/cgtDecide.c102
-rw-r--r--src/aig/cgt/cgtInt.h107
-rw-r--r--src/aig/cgt/cgtMan.c168
-rw-r--r--src/aig/cgt/cgtSat.c92
-rw-r--r--src/aig/cgt/module.make5
-rw-r--r--src/aig/fra/fraCec.c2
-rw-r--r--src/aig/fra/fraSec.c7
-rw-r--r--src/aig/kit/kit.h13
-rw-r--r--src/aig/ntl/ntl.h13
-rw-r--r--src/aig/ntl/ntlCheck.c6
-rw-r--r--src/aig/ntl/ntlReadBlif.c2
-rw-r--r--src/aig/ntl/ntlSweep.c23
-rw-r--r--src/aig/ntl/ntlTable.c28
-rw-r--r--src/aig/nwk/nwkMan.c4
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigAbs.c515
-rw-r--r--src/aig/saig/saigBmc.c4
-rw-r--r--src/aig/saig/saigMiter.c8
-rw-r--r--src/aig/ssw/ssw.h2
-rw-r--r--src/aig/ssw/sswClass.c174
-rw-r--r--src/aig/ssw/sswCore.c8
-rw-r--r--src/aig/ssw/sswMan.c2
-rw-r--r--src/aig/ssw/sswSim.c64
-rw-r--r--src/base/abci/abc.c195
-rw-r--r--src/base/abci/abcDar.c53
-rw-r--r--src/base/main/mainInt.h4
-rw-r--r--src/map/if/ifTime.c2
-rw-r--r--src/misc/util/util_hack.h4
-rw-r--r--src/misc/vec/vecStr.h63
-rw-r--r--src/sat/bsat/satSolver.h8
37 files changed, 2219 insertions, 167 deletions
diff --git a/Makefile b/Makefile
index 598c0abb..cfa819f4 100644
--- a/Makefile
+++ b/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)
diff --git a/abc.dsp b/abc.dsp
index 6a32d900..9c87c7ee 100644
--- a/abc.dsp
+++ b/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"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 2e409312..0cdd5b1a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -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 );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index e5b4d2c7..2668bbb2 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -206,6 +206,25 @@ void Aig_ManCleanData( Aig_Man_t * p )
/**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.]
Description [Applicable to small AIGs only because no caching is performed.]
diff --git a/src/aig/cgt/cgt.h b/src/aig/cgt/cgt.h
new file mode 100644
index 00000000..b9997d56
--- /dev/null
+++ b/src/aig/cgt/cgt.h
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cgt/cgtAig.c b/src/aig/cgt/cgtAig.c
new file mode 100644
index 00000000..b30d3f16
--- /dev/null
+++ b/src/aig/cgt/cgtAig.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtCore.c b/src/aig/cgt/cgtCore.c
new file mode 100644
index 00000000..a06820b4
--- /dev/null
+++ b/src/aig/cgt/cgtCore.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtDecide.c b/src/aig/cgt/cgtDecide.c
new file mode 100644
index 00000000..8f57bd4a
--- /dev/null
+++ b/src/aig/cgt/cgtDecide.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtInt.h b/src/aig/cgt/cgtInt.h
new file mode 100644
index 00000000..7b4b6e63
--- /dev/null
+++ b/src/aig/cgt/cgtInt.h
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c
new file mode 100644
index 00000000..9615d2e6
--- /dev/null
+++ b/src/aig/cgt/cgtMan.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtSat.c b/src/aig/cgt/cgtSat.c
new file mode 100644
index 00000000..094fb47d
--- /dev/null
+++ b/src/aig/cgt/cgtSat.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/module.make b/src/aig/cgt/module.make
new file mode 100644
index 00000000..911d8d1f
--- /dev/null
+++ b/src/aig/cgt/module.make
@@ -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
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 190281c9..2cdf203d 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.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) );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index cae37f85..ca73b17d 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -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;
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index a0fca09d..101cf2eb 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -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 );
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index a82157c0..54db901f 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -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 ==========================================================*/
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index 03e9e898..47f14525 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.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 );
}
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 800b711c..d1a1b99d 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -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 $]
***********************************************************************/
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index 991d701a..fc95415d 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -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 ) )
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index 208b4491..aa122900 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -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 );
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index 252546e8..55cdf42b 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -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;
}
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 02db900b..d96996cf 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -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 );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index cfbba7e1..8498f59a 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -28,12 +28,315 @@
/// 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.]
Description []
@@ -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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 2248fb37..a5235042 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -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 )
{
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index cc71f371..84c8a4fe 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -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 );
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 4bb2356a..5d70812d 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -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 ==========================================================*/
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 3dfee28b..771fd530 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -482,75 +482,34 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Creates initial simulation classes.]
+ Synopsis [Takes the set of const1 cands and rehashes them using sim info.]
- Description [Assumes that simulation info is assigned.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
+int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
{
-// int nFrames = 4;
-// int nWords = 1;
-// int nIters = 16;
-
-// int nFrames = 32;
-// int nWords = 4;
-// int nIters = 0;
-
- int nFrames = 4;
- int nWords = 2;
- int nIters = 16;
- Ssw_Cla_t * p;
- Ssw_Sml_t * pSml;
+ Aig_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, RetValue;
- int clk;
-
- // start the classes
- p = Ssw_ClassesStart( pAig );
-
- // perform sequential simulation
-clk = clock();
- pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
-if ( fVerbose )
-{
- printf( "Allocated %.2f Mb for simulation information.\n",
- 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
- printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords );
- PRT( "Time", clock() - clk );
-}
-
- // set comparison procedures
-clk = clock();
- Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+ int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
// allocate the hash table hashing simulation info into nodes
- nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
+ nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 );
ppTable = CALLOC( Aig_Obj_t *, nTableSize );
ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
- // add all the nodes to the hash table
+ // sort through the candidates
nEntries = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
+ p->nCands1 = 0;
+ Vec_PtrForEachEntry( vCands, pObj, i )
{
- if ( fLatchCorr )
- {
- if ( !Saig_ObjIsLo(p->pAig, pObj) )
- continue;
- }
- else
- {
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
- continue;
- // skip the node with more that the given number of levels
- if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
- continue;
- }
+ 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 ) )
{
@@ -562,7 +521,9 @@ clk = clock();
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
@@ -581,24 +542,18 @@ clk = clock();
nEntries++;
}
}
-
- // 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 )
+ Vec_PtrForEachEntry( vCands, 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 = p->pMemClassesFree + nEntries2;
ppClassNew[0] = pObj;
for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
@@ -611,12 +566,88 @@ clk = clock();
// 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.]
+
+ Description [Assumes that simulation info is assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
+{
+// int nFrames = 4;
+// int nWords = 1;
+// int nIters = 16;
+
+// int nFrames = 32;
+// int nWords = 4;
+// int nIters = 0;
+
+ int nFrames = 4;
+ int nWords = 2;
+ int nIters = 16;
+ Ssw_Cla_t * p;
+ Ssw_Sml_t * pSml;
+ Vec_Ptr_t * vCands;
+ Aig_Obj_t * pObj;
+ int i, k, RetValue, clk;
+
+ // start the classes
+ p = Ssw_ClassesStart( pAig );
+
+ // perform sequential simulation
+clk = clock();
+ pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
+if ( fVerbose )
+{
+ 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 );
+}
+
+ // set comparison procedures
+clk = clock();
+ Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+
+ // collect nodes to be considered as candidates
+ vCands = Vec_PtrAlloc( 1000 );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( fLatchCorr )
+ {
+ if ( !Saig_ObjIsLo(p->pAig, pObj) )
+ continue;
+ }
+ else
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ // skip the node with more that the given number of levels
+ if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
+ continue;
+ }
+ Vec_PtrPush( vCands, pObj );
+ }
+
+ // allocate room for classes
+ 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 );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 6db8cc3a..68c00a0e 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -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;
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 91f6e713..913f7518 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -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;
}
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index ce6ca38c..836b75e3 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -187,6 +187,70 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
/**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.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ac417d14..2ad8dc75 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 22f4b45c..dcc7f4c1 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -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;
@@ -2563,6 +2562,44 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i
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.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
@@ -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;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index b03a00fa..becbfd6b 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -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
};
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index 59322cad..20521805 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -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*************************************************************
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index 71c77321..3fdb7ffb 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -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
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 863be8bb..a00aaa68 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -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*************************************************************
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 00ac60ca..7bb4bd6c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -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