summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-03-02 15:26:29 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-03-02 15:26:29 -0800
commit96a399568d1c3e54e27d3a560cab3745f0d8ee06 (patch)
tree06d504990e9d2fb61487f9e713fe036717187722
parentd8505990202576e06db2c0c9a24a652fc66b2bd3 (diff)
downloadabc-96a399568d1c3e54e27d3a560cab3745f0d8ee06.tar.gz
abc-96a399568d1c3e54e27d3a560cab3745f0d8ee06.tar.bz2
abc-96a399568d1c3e54e27d3a560cab3745f0d8ee06.zip
Adding experimental command.
-rw-r--r--abclib.dsp4
-rw-r--r--src/base/abci/abc.c46
-rw-r--r--src/base/abci/abcEco.c58
-rw-r--r--src/base/abci/module.make1
4 files changed, 109 insertions, 0 deletions
diff --git a/abclib.dsp b/abclib.dsp
index b852551d..6df9c79d 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -271,6 +271,10 @@ SOURCE=.\src\base\abci\abcDsd.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abci\abcEco.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abci\abcExact.c
# End Source File
# Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8fa870a1..7fc45f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -317,6 +317,7 @@ static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -968,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "eco", Abc_CommandEco, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc2", Abc_CommandBmc2, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc3", Abc_CommandBmc3, 1 );
@@ -23949,6 +23951,50 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_NtkEco( char * pFileNames[3] );
+ char * pFileNames[3] = {NULL}; int c;
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( globalUtilOptind + 3 != argc )
+ {
+ Abc_Print( -1, "Expecting three file names on the command line.\n" );
+ return 1;
+ }
+ for ( c = 0; c < 3; c++ )
+ pFileNames[c] = argv[globalUtilOptind+c];
+ Abc_NtkEco( pFileNames );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: eco [-h]\n" );
+ Abc_Print( -2, "\t performs experimental ECO computation\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c
new file mode 100644
index 00000000..70a76729
--- /dev/null
+++ b/src/base/abci/abcEco.c
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+ FileName [abcEco.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Experimental procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "map/mio/mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkEco( char * pFileNames[3] )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b97f526f..abf56716 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDress2.c \
src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcEco.c \
src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFraig.c \