diff options
| -rw-r--r-- | Makefile | 27 | ||||
| -rw-r--r-- | lib/x64/pthreadVC2.dll | bin | 0 -> 82944 bytes | |||
| -rw-r--r-- | lib/x64/pthreadVC2.lib | bin | 0 -> 29738 bytes | |||
| -rw-r--r-- | lib/x86/pthreadVC2.dll (renamed from lib/pthreadVC2.dll) | bin | 86070 -> 86070 bytes | |||
| -rw-r--r-- | lib/x86/pthreadVC2.lib (renamed from lib/pthreadVC2.lib) | bin | 29280 -> 29280 bytes | |||
| -rw-r--r-- | readme | 112 | ||||
| -rw-r--r-- | readme.md | 103 | ||||
| -rw-r--r-- | src/base/cmd/cmdStarter.c | 5 | ||||
| -rw-r--r-- | src/base/main/mainUtils.c | 5 | ||||
| -rw-r--r-- | src/proof/abs/absPth.c | 7 |
10 files changed, 126 insertions, 133 deletions
@@ -37,11 +37,26 @@ arch_flags : arch_flags.c ARCHFLAGS := $(shell $(CC) arch_flags.c -o arch_flags && ./arch_flags) OPTFLAGS := -g -O #-DABC_NAMESPACE=xxx -CFLAGS += -Wall -Wno-unused-function -Wno-unused-but-set-variable $(OPTFLAGS) $(ARCHFLAGS) -I$(PWD)/src -CXXFLAGS += $(CFLAGS) +CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(ARCHFLAGS) -I$(PWD)/src + +ifeq ($(shell $(CC) -dumpversion | awk '{FS="."; print ($$1>=4 && $$2>=6)}'),1) +# Set -Wno-unused-bug-set-variable for GCC 4.6.0 and greater only +CFLAGS += -Wno-unused-but-set-variable +endif + +LIBS := -ldl -#LIBS := -m32 -ldl -rdynamic -lreadline -ltermcap -LIBS := -ldl -lreadline -lpthread +ifneq ($(READLINE),0) +CFLAGS += -DABC_USE_READLINE +LIBS += -lreadline +endif + +ifneq ($(PTHREADS),0) +CFLAGS += -DABC_USE_PTHREADS +LIBS += -lpthread +endif + +CXXFLAGS += $(CFLAGS) SRC := GARBAGE := core core.* *.stackdump ./tags $(PROG) arch_flags @@ -65,7 +80,7 @@ DEP := $(OBJ:.o=.d) %.o: %.cc @echo "\`\` Compiling:" $(LOCAL_PATH)/$< - @$(CC) -c $(CXXFLAGS) $< -o $@ + @$(CXX) -c $(CXXFLAGS) $< -o $@ %.d: %.c @echo "\`\` Dependency:" $(LOCAL_PATH)/$< @@ -73,7 +88,7 @@ DEP := $(OBJ:.o=.d) %.d: %.cc @echo "\`\` Generating dependency:" $(LOCAL_PATH)/$< - @./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $(CFLAGS) $*.cc > $@ + @./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $*.cc > $@ -include $(DEP) diff --git a/lib/x64/pthreadVC2.dll b/lib/x64/pthreadVC2.dll Binary files differnew file mode 100644 index 00000000..165b4d26 --- /dev/null +++ b/lib/x64/pthreadVC2.dll diff --git a/lib/x64/pthreadVC2.lib b/lib/x64/pthreadVC2.lib Binary files differnew file mode 100644 index 00000000..1b07e0e9 --- /dev/null +++ b/lib/x64/pthreadVC2.lib diff --git a/lib/pthreadVC2.dll b/lib/x86/pthreadVC2.dll Binary files differindex 93f562ba..93f562ba 100644 --- a/lib/pthreadVC2.dll +++ b/lib/x86/pthreadVC2.dll diff --git a/lib/pthreadVC2.lib b/lib/x86/pthreadVC2.lib Binary files differindex 58733254..58733254 100644 --- a/lib/pthreadVC2.lib +++ b/lib/x86/pthreadVC2.lib diff --git a/readme b/readme deleted file mode 100644 index c1f3fc39..00000000 --- a/readme +++ /dev/null @@ -1,112 +0,0 @@ -ABC: System for Sequential Logic Synthesis and Formal Verification - -ABC is always changing but the current snapshot is believed to be stable. - -Compiling: - -To compile ABC as a binary, download and unzip the code, then type "make". - -To compile ABC as a static library, comment out #define _LIB in file -"src/base/main/main.c", then type "make libabc.a". - -When ABC is used as a static library, two additional procedures, Abc_Start() -and Abc_Stop(), are provided for starting and quitting the ABC framework in -the calling application. A simple demo program (file src/demo.c) shows how to -create a stand-alone program performing DAG-aware AIG rewriting, by calling -APIs of ABC compiled as a static library. - -To build the demo program -- Copy demo.cc and libabc.a to the working directory -- Run "gcc -Wall -g -c demo.c -o demo.o" -- Run "gcc -g -o demo demo.o libabc.a -lm -ldl -rdynamic -lreadline -ltermcap -lpthread" - -To run the demo program, give it a file with the logic network in AIGER or BLIF. For example: - -> [alanmi@mima] ~/abc> demo i10.aig -> i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 -> i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 -> Networks are equivalent. -> Reading = 0.00 sec Rewriting = 0.18 sec Verification = 0.41 sec - -The same can be produced by running the binary in the command-line mode: - -> [alanmi@mima] ~/abc> ./abc -> UC Berkeley, ABC 1.01 (compiled Oct 6 2012 19:05:18) -> abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec -> i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 -> i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 -> Networks are equivalent. - -or in the batch mode: - -> [alanmi@mima] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" -> ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec". -> i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 -> i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 -> Networks are equivalent. - - - -Compiling as C or C++ - -The current version of ABC can be compiled with C compiler or C++ compiler. - -To compile as C code (default): make sure that CC=gcc and ABC_NAMESPACE is not defined. -To compile as C++ code without namespaces: make sure that CC=g++ and ABC_NAMESPACE is not defined. -To compile as C++ code with namespaces: make sure that CC=g++ and ABC_NAMESPACE is set to -the name of the requested namespace. For example, add to OPTFLAGS -DABC_NAMESPACE=xxx - - -Bug reporting: - -Please try to reproduce all the reported bugs and unexpected features using the latest -version of ABC available from https://bitbucket.org/alanmi/abc/ - -If the bug still persists, please provide the following information: -1. ABC version (when it was downloaded from BitBucket) -2. Linux distribution and version (32-bit or 64-bit) -3. The exact command-line and error message when trying to run the tool -4. The output of the 'ldd' command run on the exeutable (e.g. 'ldd abc'). -5. Versions of relevant tools or packages used. - - -Trouble shooting: - -(1) If compilation does not start because of the cyclic dependency check, -try touching all files as follows: find ./ -type f -exec touch "{}" \; - -(2) If compilation fails because readline is missing, install 'readline' library or -comment out line 26 "#define ABC_USE_READLINE" in file "src/base/main/mainUtils.c" - -(4) If compilation fails because pthreads are missing, install 'pthread' library or -comment out line 29 "#define ABC_USE_PTHREADS" in file "src/base/cmd/cmdStarter.c" -and in file "src/proof/abs/absPth.c" - -(5) If compilation fails in file "src/base/main/libSupport.c", try the following: -- Remove "src/base/main/libSupport.c" from "src/base/main/module.make" -- Comment out calls to Libs_Init() and Libs_End() in "src/base/main/mainInit.c" - -(6) On some systems, readline requires adding '-lcurses' to Makefile. - - -The following comment was added by Krish Sundaresan: - -"I found that the code does compile correctly on Solaris if gcc is used (instead of -g++ that I was using for some reason). Also readline which is not available by default -on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package -from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local -include files for readline and LIBS to add the local libreadline.a. Perhaps you can -add these steps in the readme to help folks compiling this on Solaris." - -The following tutorial is kindly offered by Ana Petkovska from EPFL: -https://www.dropbox.com/s/qrl9svlf0ylxy8p/ABC_GettingStarted.pdf - -Final remarks: - -Unfortunately, there is no comprehensive regression test. Good luck! - - -This system is maintained by Alan Mishchenko <alanmi@eecs.berkeley.edu>. Consider also -using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz - -This file was last modified on Oct 6, 2012 diff --git a/readme.md b/readme.md new file mode 100644 index 00000000..7c3481fc --- /dev/null +++ b/readme.md @@ -0,0 +1,103 @@ +# ABC: System for Sequential Logic Synthesis and Formal Verification + +ABC is always changing but the current snapshot is believed to be stable. + +## Compiling: + +To compile ABC as a binary, download and unzip the code, then type `make`. + +To compile ABC as a static library, comment out `#define ABC_LIB` in file +"src/base/main/main.c", then type `make libabc.a`. + +When ABC is used as a static library, two additional procedures, `Abc_Start()` +and `Abc_Stop()`, are provided for starting and quitting the ABC framework in +the calling application. A simple demo program (file src/demo.c) shows how to +create a stand-alone program performing DAG-aware AIG rewriting, by calling +APIs of ABC compiled as a static library. + +To build the demo program + + * Copy demo.cc and libabc.a to the working directory + * Run `gcc -Wall -g -c demo.c -o demo.o` + * Run `gcc -g -o demo demo.o libabc.a -lm -ldl -rdynamic -lreadline -ltermcap -lpthread` + +To run the demo program, give it a file with the logic network in AIGER or BLIF. For example: + + [alanmi@mima] ~/abc> demo i10.aig + i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 + i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 + Networks are equivalent. + Reading = 0.00 sec Rewriting = 0.18 sec Verification = 0.41 sec + +The same can be produced by running the binary in the command-line mode: + + [alanmi@mima] ~/abc> ./abc + UC Berkeley, ABC 1.01 (compiled Oct 6 2012 19:05:18) + abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec + i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 + i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 + Networks are equivalent. + +or in the batch mode: + + [alanmi@mima] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec". + i10 : i/o = 257/ 224 lat = 0 and = 2396 lev = 37 + i10 : i/o = 257/ 224 lat = 0 and = 1851 lev = 35 + Networks are equivalent. + +## Compiling as C or C++ + +The current version of ABC can be compiled with C compiler or C++ compiler. + + * To compile as C code (default): make sure that `CC=gcc` and `ABC_NAMESPACE` is not defined. + * To compile as C++ code without namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is not defined. + * To compile as C++ code with namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is set to + the name of the requested namespace. For example, add `-DABC_NAMESPACE=xxx` to OPTFLAGS. + +## Bug reporting: + +Please try to reproduce all the reported bugs and unexpected features using the latest +version of ABC available from https://bitbucket.org/alanmi/abc/ + +If the bug still persists, please provide the following information: + + 1. ABC version (when it was downloaded from BitBucket) + 1. Linux distribution and version (32-bit or 64-bit) + 1. The exact command-line and error message when trying to run the tool + 1. The output of the `ldd` command run on the exeutable (e.g. `ldd abc`). + 1. Versions of relevant tools or packages used. + + +## Troubleshooting: + + 1. If compilation does not start because of the cyclic dependency check, +try touching all files as follows: `find ./ -type f -exec touch "{}" \;` + 1. If compilation fails because readline is missing, install 'readline' library or +compile with `make READLINE=0` + 1. If compilation fails because pthreads are missing, install 'pthread' library or +compile with `make PTHREADS=0` + * See http://sourceware.org/pthreads-win32/ for pthreads on Windows + * Precompiled DLLs are available from ftp://sourceware.org/pub/pthreads-win32/dll-latest + 1. If compilation fails in file "src/base/main/libSupport.c", try the following: + * Remove "src/base/main/libSupport.c" from "src/base/main/module.make" + * Comment out calls to `Libs_Init()` and `Libs_End()` in "src/base/main/mainInit.c" + 1. On some systems, readline requires adding '-lcurses' to Makefile. + +The following comment was added by Krish Sundaresan: + +"I found that the code does compile correctly on Solaris if gcc is used (instead of +g++ that I was using for some reason). Also readline which is not available by default +on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package +from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local +include files for readline and LIBS to add the local libreadline.a. Perhaps you can +add these steps in the readme to help folks compiling this on Solaris." + +## Final remarks: + +Unfortunately, there is no comprehensive regression test. Good luck! + +This system is maintained by Alan Mishchenko <alanmi@eecs.berkeley.edu>. Consider also +using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz + +This file was last modified on April 25, 2013 diff --git a/src/base/cmd/cmdStarter.c b/src/base/cmd/cmdStarter.c index 21384930..bfdd480c 100644 --- a/src/base/cmd/cmdStarter.c +++ b/src/base/cmd/cmdStarter.c @@ -25,12 +25,9 @@ #include "misc/util/abc_global.h" #include "misc/extra/extra.h" -// comment out this line to disable pthreads -#define ABC_USE_PTHREADS - #ifdef ABC_USE_PTHREADS -#ifdef WIN32 +#ifdef _WIN32 #include "../lib/pthread.h" #else #include <pthread.h> diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index 8d24a123..2b4e682b 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -21,11 +21,6 @@ #include "base/abc/abc.h" #include "mainInt.h" -#if !defined(_WIN32) && !defined(AIX) -// comment out the following line if 'readline' is not available -#define ABC_USE_READLINE -#endif - #ifdef ABC_USE_READLINE #include <readline/readline.h> #include <readline/history.h> diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index ef38369c..bd3f2dcb 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -23,14 +23,9 @@ #include "proof/ssw/ssw.h" - - -// comment out this line to disable pthreads -#define ABC_USE_PTHREADS - #ifdef ABC_USE_PTHREADS -#ifdef WIN32 +#ifdef _WIN32 #include "../lib/pthread.h" #else #include <pthread.h> |