mirror of https://github.com/YosysHQ/abc.git
Making changes suggested by Mark Jarvin.
This commit is contained in:
parent
95571be503
commit
36d5ef4e62
27
Makefile
27
Makefile
|
|
@ -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
|
||||
|
||||
#LIBS := -m32 -ldl -rdynamic -lreadline -ltermcap
|
||||
LIBS := -ldl -lreadline -lpthread
|
||||
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
|
||||
|
||||
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)
|
||||
|
||||
|
|
|
|||
Binary file not shown.
Binary file not shown.
112
readme
112
readme
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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>
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
Loading…
Reference in New Issue