summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-04-27 16:26:41 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-04-27 16:26:41 +0700
commita4baba2c832f9e99dbe9b980757cdf8bb2869c3a (patch)
tree6967824c0c92d3dbe8ac8459cb7debee9f7de9d4 /src
parent590202e327852b35032fbbfff0389d71badffd7f (diff)
downloadabc-a4baba2c832f9e99dbe9b980757cdf8bb2869c3a.tar.gz
abc-a4baba2c832f9e99dbe9b980757cdf8bb2869c3a.tar.bz2
abc-a4baba2c832f9e99dbe9b980757cdf8bb2869c3a.zip
Misc changes.
Diffstat (limited to 'src')
-rw-r--r--src/base/main/mainInit.c11
-rw-r--r--src/base/main/mainInt.h71
2 files changed, 44 insertions, 38 deletions
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index 8e34857e..2b2a93e8 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -23,7 +23,8 @@
ABC_NAMESPACE_IMPL_START
-//#define USE_ABC2
+#define USE_ABC2
+#define USE_ABC85
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -51,6 +52,8 @@ extern void Test_Init( Abc_Frame_t * pAbc );
extern void Test_End( Abc_Frame_t * pAbc );
extern void Abc2_Init( Abc_Frame_t * pAbc );
extern void Abc2_End ( Abc_Frame_t * pAbc );
+extern void Abc85_Init( Abc_Frame_t * pAbc );
+extern void Abc85_End( Abc_Frame_t * pAbc );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -83,6 +86,9 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
#ifdef USE_ABC2
Abc2_Init( pAbc );
#endif
+#ifdef USE_ABC85
+ Abc85_Init( pAbc );
+#endif
EXT_ABC_INIT(pAbc) // plugin for external functionality
}
@@ -113,6 +119,9 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
#ifdef USE_ABC2
Abc2_End( pAbc );
#endif
+#ifdef USE_ABC85
+ Abc85_End( pAbc );
+#endif
EXT_ABC_END(pAbc) // plugin for external functionality
}
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d8a6c93e..a16d7f2e 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -57,63 +57,60 @@ ABC_NAMESPACE_HEADER_START
struct Abc_Frame_t_
{
// general info
- char * sVersion; // the name of the current version
+ char * sVersion; // the name of the current version
// commands, aliases, etc
- st_table * tCommands; // the command table
- st_table * tAliases; // the alias table
- st_table * tFlags; // the flag table
- Vec_Ptr_t * aHistory; // the command history
+ st_table * tCommands; // the command table
+ st_table * tAliases; // the alias table
+ st_table * tFlags; // the flag table
+ Vec_Ptr_t * aHistory; // the command history
// the functionality
Abc_Ntk_t * pNtkCur; // the current network
Abc_Ntk_t * pNtkBestDelay; // the current network
Abc_Ntk_t * pNtkBestArea; // the current network
- int nSteps; // the counter of different network processed
- int fAutoexac; // marks the autoexec mode
- int fBatchMode; // are we invoked in batch mode?
- int fBridgeMode; // are we invoked in bridge mode?
+ int nSteps; // the counter of different network processed
+ int fAutoexac; // marks the autoexec mode
+ int fBatchMode; // are we invoked in batch mode?
+ int fBridgeMode; // are we invoked in bridge mode?
// output streams
FILE * Out;
FILE * Err;
FILE * Hst;
// used for runtime measurement
- double TimeCommand; // the runtime of the last command
- double TimeTotal; // the total runtime of all commands
+ double TimeCommand; // the runtime of the last command
+ double TimeTotal; // the total runtime of all commands
// temporary storage for structural choices
- Vec_Ptr_t * vStore; // networks to be used by choice
+ Vec_Ptr_t * vStore; // networks to be used by choice
// decomposition package
- void * pManDec; // decomposition manager
- DdManager * dd; // temporary BDD package
+ void * pManDec; // decomposition manager
+ DdManager * dd; // temporary BDD package
// libraries for mapping
- void * pLibLut; // the current LUT library
- void * pLibGen; // the current genlib
- void * pLibGen2; // the current genlib
- void * pLibSuper; // the current supergate library
- void * pLibVer; // the current Verilog library
+ void * pLibLut; // the current LUT library
+ void * pLibGen; // the current genlib
+ void * pLibGen2; // the current genlib
+ void * pLibSuper; // the current supergate library
+ void * pLibVer; // the current Verilog library
// new code
- Gia_Man_t * pGia; // alternative current network as a light-weight AIG
- Gia_Man_t * pGia2; // copy of the above
- Abc_Cex_t * pCex; // a counter-example to fail the current network
- Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails
- Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs
-
+ Gia_Man_t * pGia; // alternative current network as a light-weight AIG
+ Gia_Man_t * pGia2; // copy of the above
+ Abc_Cex_t * pCex; // a counter-example to fail the current network
+ Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails
+ Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs
+ int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1)
+ int nFrames; // the number of time frames completed by BMC
+ Vec_Ptr_t * vPlugInComBinPairs; // pairs of command and its binary name
+ Vec_Ptr_t * vLTLProperties_global; // related to LTL
void * pSave1;
void * pSave2;
void * pSave3;
void * pSave4;
+ void * pAbc85Ntl;
+ void * pAbc85Ntl2;
+ void * pAbc85Best;
+ void * pAbc85Delay;
+ If_Lib_t * pAbc85Lib;
- // related to LTL
- Vec_Ptr_t * vLTLProperties_global;
-
- // the addition to keep the best Ntl that can be used to restore
- void * pAbc8NtlBestDelay; // the best delay, Ntl
- void * pAbc8NtlBestArea; // the best area
- int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1)
- int nFrames; // the number of time frames completed by BMC
-
- Vec_Ptr_t * vPlugInComBinPairs; // pairs of command and its binary name
-
- EXT_ABC_FRAME // plugin for external functionality
+ EXT_ABC_FRAME // plugin for external functionality
};
////////////////////////////////////////////////////////////////////////