Initial import.

This commit is contained in:
Jerry James 2014-12-16 08:17:25 -07:00
commit 575c8c745f
6 changed files with 387 additions and 0 deletions

1
.gitignore vendored
View file

@ -0,0 +1 @@
/9d6335cdb362.zip

89
abc-bundlelib.patch Normal file
View file

@ -0,0 +1,89 @@
--- ./Makefile.orig 2014-11-30 17:18:13.000000000 -0700
+++ ./Makefile 2014-12-01 12:00:00.000000000 -0700
@@ -20,7 +20,7 @@ MODULES := \
src/map/mapper src/map/mio src/map/super src/map/if \
src/map/amap src/map/cov src/map/scl src/map/mpm \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
- src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
+ src/misc/vec src/misc/hash src/misc/tim \
src/misc/mem src/misc/bar src/misc/bbl \
src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
@@ -67,7 +67,7 @@ endif
endif
# LIBS := -ldl -lrt
-LIBS += -ldl
+LIBS += -Wl,--as-needed -lbz2 -lz -ldl
ifneq ($(findstring Darwin, $(shell uname)), Darwin)
LIBS += -lrt
endif
@@ -104,15 +104,15 @@ DEP := $(OBJ:.o=.d)
%.o: %.c
@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
- @$(CC) -c $(CFLAGS) $< -o $@
+ $(CC) -c $(CFLAGS) $< -o $@
%.o: %.cc
@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
- @$(CXX) -c $(CXXFLAGS) $< -o $@
+ $(CXX) -c $(CXXFLAGS) $< -o $@
%.o: %.cpp
@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
- @$(CXX) -c $(CXXFLAGS) $< -o $@
+ $(CXX) -c $(CXXFLAGS) $< -o $@
%.d: %.c
@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
--- ./src/base/io/ioReadAiger.c.orig 2014-11-30 17:18:13.000000000 -0700
+++ ./src/base/io/ioReadAiger.c 2014-12-01 12:00:00.000000000 -0700
@@ -26,8 +26,8 @@
#include <string.h>
#include <assert.h>
-#include "misc/bzlib/bzlib.h"
-#include "misc/zlib/zlib.h"
+#include <bzlib.h>
+#include <zlib.h>
#include "ioAbc.h"
ABC_NAMESPACE_IMPL_START
--- ./src/base/io/ioReadBlifMv.c.orig 2014-11-30 17:18:13.000000000 -0700
+++ ./src/base/io/ioReadBlifMv.c 2014-12-01 12:00:00.000000000 -0700
@@ -18,8 +18,8 @@
***********************************************************************/
-#include "misc/zlib/zlib.h"
-#include "misc/bzlib/bzlib.h"
+#include <zlib.h>
+#include <bzlib.h>
#include "base/abc/abc.h"
#include "misc/vec/vecPtr.h"
#include "ioAbc.h"
--- ./src/base/io/ioWriteAiger.c.orig 2014-11-30 17:18:13.000000000 -0700
+++ ./src/base/io/ioWriteAiger.c 2014-12-01 12:00:00.000000000 -0700
@@ -26,8 +26,8 @@
#include <string.h>
#include <assert.h>
-#include "misc/bzlib/bzlib.h"
-#include "misc/zlib/zlib.h"
+#include <bzlib.h>
+#include <zlib.h>
#include "ioAbc.h"
--- ./src/sat/cnf/cnfMan.c.orig 2014-11-30 17:18:13.000000000 -0700
+++ ./src/sat/cnf/cnfMan.c 2014-12-01 12:00:00.000000000 -0700
@@ -21,7 +21,7 @@
#include "cnf.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satSolver2.h"
-#include "misc/zlib/zlib.h"
+#include <zlib.h>
ABC_NAMESPACE_IMPL_START

24
abc-sharedlib.patch Normal file
View file

@ -0,0 +1,24 @@
--- ./Makefile.orig 2014-12-01 12:00:00.000000000 -0700
+++ ./Makefile 2014-12-01 12:00:00.000000000 -0700
@@ -44,7 +44,7 @@ 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-write-strings -Wno-sign-compare $(OPTFLAGS) $(ARCHFLAGS) -Isrc
+CFLAGS += -Wno-unused-function $(OPTFLAGS) $(ARCHFLAGS) -Isrc
# Set -Wno-unused-bug-set-variable for GCC 4.6.0 and greater only
ifneq ($(or $(findstring gcc,$(CC)),$(findstring g++,$(CC))),)
@@ -143,6 +143,12 @@ $(PROG): $(OBJ)
@echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@)
@$(LD) -o $@ $^ $(LIBS)
+lib$(PROG).so: $(OBJ)
+ @echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
+ $(LD) -shared -Wl,-h,lib$(PROG).so.0 -o lib$(PROG).so.0.0.0 $^ $(LIBS)
+ @ln -s lib$(PROG).so.0.0.0 lib$(PROG).so.0
+ @ln -s lib$(PROG).so.0 $@
+
lib$(PROG).a: $(OBJ)
@echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
@ar rv $@ $?

99
abc.1 Normal file
View file

@ -0,0 +1,99 @@
.TH "ABC" "1" "@VERSION@" "ABC" "User Commands"
.SH "NAME"
abc \- sequential logic synthesis and formal verification
.SH "SYNOPSIS"
.B abc
[\fIOPTIONS\fP] \fIFILE\fP
.SH "DESCRIPTION"
.PP
ABC is a growing software system for synthesis and verification of binary
sequential logic circuits appearing in synchronous hardware designs. ABC
combines scalable logic optimization based on And-Inverter Graphs (AIGs),
optimal-delay DAG-based technology mapping for look-up tables and standard
cells, and innovative algorithms for sequential synthesis and verification.
.PP
ABC provides an experimental implementation of these algorithms and a
programming environment for building similar applications. Future development
will focus on improving the algorithms and making most of the packages
stand-alone. This will allow the user to customize ABC for their needs as if
it were a toolbox rather than a complete tool.
.SH "OPTIONS"
.TP
\fB\-c\fP \fICMD\fP
Execute commands \fICMD\fP.
.TP
\fB\-q\fP \fICMD\fP
Execute commands \fICMD\fP quietly.
.TP
\fB\-C\fP \fICMD\fP
Execute commands \fICMD\fP, then continue in interactive mode.
.TP
\fB\-F\fP \fISCRIPT\fP
Execute commands from script file \fISCRIPT\fP and echo commands.
.TP
\fB\-f\fP \fISCRIPT\fP
Execute commands from script file \fISCRIPT\fP.
.TP
\fB\-h\fP
Print command usage.
.TP
\fB\-o\fP \fIFILE\fP
Store the result in \fIFILE\fP.
.TP
\fB\-s\fP
Do not read any initialization file.
.TP
\fB\-t\fP \fITYPE\fP
Specify the input type, one of \fIblif_mv\fP, \fIblif_mvs\fP, \fIblif\fP, or
\fInone\fP. The default is \fIblif_mv\fP.
.TP
\fB\-T\fP \fITYPE\fP
Specify the output type, one of \fIblif_mv\fP, \fIblif_mvs\fP, \fIblif\fP, or
\fInone\fP. The default is \fIblif_mv\fP.
.TP
\fB\-x\fP
Equivalent to \fI-t none -T none\fP.
.TP
\fB\-b\fP
Run in bridge mode.
.SH "INTRODUCTION"
.PP
Data structures and algorithms at the heart of a software system determine its
capabilities in processing data and its efficiency as a programming
environment for building new applications. Extensive experience of developing
and using SIS, VIS, and MVSIS, makes it clear that these systems do not
provide a flexible programming environment to implement recent innovations,
such as integration of technology mapping and retiming. Specifically, the SIS
environment is outdated and rather inefficient when handling large circuits.
VIS, designed as a formal verification tool for multi-valued specifications,
does not provide enough flexibility for binary synthesis. MVSIS was developed
and extensively used by us in the recent years for implementing new synthesis
algorithms for both multi-valued and binary networks. Finally, we became
convinced that (a) the basic data structures and algorithms of MVSIS can be
made considerably simpler and easier to use by assuming binary networks, and
(b) a central place in the new system should be given to a new data structure,
AIGs (multi-level logic networks composed of two-input ANDs and inverters),
which promises improvements in quality and runtime of synthesis and
verification.
.PP
This understanding motivates us to redevelop the core packages of MVSIS
resulting in a new programming environment named ABC. As the name suggests,
the primary goal is to keep data structures simple and flexible for a wide
range of applications. The “philosophy of ABC” has several basic premises.
One of them is allowing for a variety of functional representations, such as
BDDs and SOPs, to solve specialized tasks, while defaulting to AIGs for the
mainstream network manipulation. Representing logic using AIGs leads to a
remarkable uniformity in computation and efficient interfacing with CNF-based
SAT solvers for handing Boolean reasoning problems. Another fundamental
premise of ABC is the synergy between synthesis and verification using
efficient SAT-based Boolean reasoning on the AIG for combinational and
sequential equivalence checking.
.PP
The goal of the ABC project is to provide a public-domain implementation of
the state-of-the-art combinational and sequential synthesis algorithms and, at
the same time, create an open-source environment, in which such applications
can be developed and compared. The current version of ABC can
optimize/map/retime industrial gate-level designs with 100K gates and 10K
sequential elements for optimal delay and heuristically minimized area in
about one minute of CPU time on a modern computer. The runtime of the
combinational synthesis, mapping, and verification is typically faster.

173
abc.spec Normal file
View file

@ -0,0 +1,173 @@
# Python packaging notes:
# 1. Upstream does not yet support python 3, so we build for python 2 only.
# 2. The python build does not link against the library stored in _libdir,
# because it has to be built differently. Look for instances of
# "#ifdef ABC_PYTHON_EMBED ... #endif" in the source code. Hence, the
# python2 subpackage is indepedent of the -libs subpackage.
# Upstream doesn't make releases. We have to check the code out of Mercurial.
%global owner alanmi
%global commit 9d6335cdb362
%global hgdate 20141130
Name: abc
Version: 1.01
Release: 2.hg%{hgdate}%{?dist}
Summary: Sequential logic synthesis and formal verification
# This would be MIT, but we link with readline
License: GPLv3+
URL: http://www.eecs.berkeley.edu/~alanmi/abc/abc.htm
Source0: https://bitbucket.org/%{owner}/%{name}/get/%{commit}.zip
# Man page created by Jerry James using upstream text; hence, it is covered by
# the same copyright and license as the code.
Source1: %{name}.1
# Fedora-specific patch: do not use the bundled libraries
Patch0: %{name}-bundlelib.patch
# Fedora-specific patch: build a shared library instead of a static library
Patch1: %{name}-sharedlib.patch
BuildRequires: bzip2-devel
BuildRequires: python2-devel
BuildRequires: readline-devel
BuildRequires: swig
BuildRequires: zlib-devel
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
%description
ABC is a growing software system for synthesis and verification of
binary sequential logic circuits appearing in synchronous hardware
designs. ABC combines scalable logic optimization based on And-Inverter
Graphs (AIGs), optimal-delay DAG-based technology mapping for look-up
tables and standard cells, and innovative algorithms for sequential
synthesis and verification.
ABC provides an experimental implementation of these algorithms and a
programming environment for building similar applications. Future
development will focus on improving the algorithms and making most of
the packages stand-alone. This will allow the user to customize ABC for
their needs as if it were a toolbox rather than a complete tool.
%package libs
Summary: Library for sequential synthesis and verification
%description libs
This package contains the core functionality of ABC as a shared library.
%package devel
Summary: Headers and libraries for developing with ABC
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
%description devel
Headers and libraries for developing applications that use ABC.
%package python2
Summary: Python 2 interface to ABC
%description python2
Python 2 interface to ABC
%prep
%setup -q -c
pushd %{owner}-%{name}-%{commit}
%patch0
%patch1
# Do not use the bundled libraries
rm -fr lib src/misc/{bzlib,zlib} src/sat/bsat2
# Fix end of line encodings
for fil in readme.md readmeaig; do
sed -i.orig 's/\r//' ${fil}
touch -r ${fil}.orig ${fil}
rm -f ${fil}.orig
done
popd
# Prepare for the python 2 build
cp -a %{owner}-%{name}-%{commit} %{name}-python2
# Set the version number in the man page
sed 's/@VERSION@/%{version} (%{hgdate})/' %{SOURCE1} > %{name}.1
touch -r %{SOURCE1} %{name}.1
%build
# Build the library and binary
pushd %{owner}-%{name}-%{commit}
make %{?_smp_mflags} libabc.so OPTFLAGS="%{optflags} -fPIC -DNDEBUG" \
LD="g++ $RPM_LD_FLAGS"
g++ src/base/main/main.o -o %{name} -L. -labc
popd
# Build for python 2
pushd %{name}-python2
make libabc.a %{?_smp_mflags} OPTFLAGS="%{optflags} -fPIC -DNDEBUG" \
LD="g++ $RPM_LD_FLAGS" ABC_PYTHON="%{__python2}"
cd src/python
%{__python2} setup.py build
popd
%install
pushd %{owner}-%{name}-%{commit}
# Install the library
mkdir -p %{buildroot}%{_libdir}
install -p -m 0755 lib%{name}.so.0.0.0 %{buildroot}%{_libdir}
ln -s lib%{name}.so.0.0.0 %{buildroot}%{_libdir}/lib%{name}.so.0
ln -s lib%{name}.so.0 %{buildroot}%{_libdir}/lib%{name}.so
# Install the header files
mkdir -p %{buildroot}%{_includedir}/%{name}
for fil in $(find -O3 src -name \*.h); do
dir=$(dirname $fil | cut -d/ -f3-)
mkdir -p %{buildroot}%{_includedir}/%{name}/$dir
install -p -m 0644 $fil %{buildroot}%{_includedir}/%{name}/$dir
done
# Install the binary
mkdir -p %{buildroot}%{_bindir}
install -p -m 0755 %{name} %{buildroot}%{_bindir}
popd
# Install the man page
mkdir -p %{buildroot}%{_mandir}/man1
install -p -m 0644 %{name}.1 %{buildroot}%{_mandir}/man1
# Install the python2 interface
pushd %{name}-python2
cd src/python
%{__python2} setup.py install -O1 --skip-build --root %{buildroot}
mkdir %{buildroot}%{python2_sitearch}/%{name}
mv %{buildroot}%{python2_sitearch}/*.py* %{buildroot}%{python2_sitearch}/*.so \
%{buildroot}%{python2_sitearch}/%{name}
chmod 0755 %{buildroot}%{python2_sitearch}/%{name}/*.so
popd
%post libs -p /sbin/ldconfig
%postun libs -p /sbin/ldconfig
%files
%doc %{owner}-%{name}-%{commit}/readme.md %{owner}-%{name}-%{commit}/readmeaig
%{_bindir}/%{name}
%{_mandir}/man1/%{name}*
%files libs
%license %{owner}-%{name}-%{commit}/copyright.txt
%{_libdir}/lib%{name}.so.*
%files devel
%{_includedir}/%{name}/
%{_libdir}/lib%{name}.so
%files python2
%license %{owner}-%{name}-%{commit}/copyright.txt
%{python2_sitearch}/*
%changelog
* Wed Dec 3 2014 Jerry James <loganjerry@gmail.com> - 1.01-2.hg20141130
- Drop unnecessary jquery Provides
- Fix file permissions
* Mon Dec 1 2014 Jerry James <loganjerry@gmail.com> - 1.01-1.hg20141130
- Initial RPM

View file

@ -0,0 +1 @@
b72d459105cfdd98f3db7ec8c17225d3 9d6335cdb362.zip