10 changed files with 616 additions and 1 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,2 @@
+/*.zip
+/abc-*.tar.gz
--- a/abc-build.patch
+++ b/abc-build.patch
@ -0,0 +1,26 @@
+--- CMakeLists.txt.orig	2019-05-30 20:27:31.000000000 -0600
+++ CMakeLists.txt	2019-06-04 09:41:14.524445396 -0600
+@@ -53,7 +53,7 @@ execute_process(
+     make
+         ${ABC_READLINE_FLAGS}
+         ${ABC_USE_NAMESPACE_FLAGS}
+-        ARCHFLAGS_EXE=${CMAKE_CURRENT_BINARY_DIR}/abc_arch_flags_program.exe
+	ABC_USE_STDINT_H=1
+         ABC_MAKE_NO_DEPS=1
+         CC=${CMAKE_C_COMPILER}
+         CXX=${CMAKE_CXX_COMPILER}
+@@ -94,6 +94,8 @@ list(REMOVE_ITEM ABC_SRC ${ABC_MAIN_SRC}
+ add_library(libabc EXCLUDE_FROM_ALL ${ABC_SRC})
+ abc_properties(libabc PUBLIC)
+ set_property(TARGET libabc PROPERTY OUTPUT_NAME abc)
+set_property(TARGET libabc PROPERTY VERSION "0.0.0")
+set_property(TARGET libabc PROPERTY SOVERSION 0)
+ 
+ add_executable(abc ${ABC_MAIN_SRC})
+ target_link_libraries(abc PRIVATE libabc)
+@@ -103,3 +105,5 @@ add_library(libabc-pic EXCLUDE_FROM_ALL
+ abc_properties(libabc-pic PUBLIC)
+ set_property(TARGET libabc-pic PROPERTY POSITION_INDEPENDENT_CODE ON)
+ set_property(TARGET libabc-pic PROPERTY OUTPUT_NAME abc-pic)
+set_property(TARGET libabc-pic PROPERTY VERSION "0.0.0")
+set_property(TARGET libabc-pic PROPERTY SOVERSION 0)
--- a/abc-bundlelib.patch
+++ b/abc-bundlelib.patch
@ -0,0 +1,113 @@
+--- Makefile.orig	2019-05-30 20:27:31.000000000 -0600
+++ Makefile	2019-06-04 09:40:32.212192338 -0600
+@@ -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/misc/parse \
+ 	src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
+ 	src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
+@@ -42,6 +42,7 @@ $(ARCHFLAGS_EXE) : arch_flags.c
+ 	$(CC) arch_flags.c -o $(ARCHFLAGS_EXE)
+ 
+ INCLUDES += -I$(ABCSRC)/src
+LIBS=-lbz2 -lz
+ 
+ # Use C99 stdint.h header for platform-dependent types
+ ifdef ABC_USE_STDINT_H
+--- src/base/io/ioReadAiger.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/base/io/ioReadAiger.c	2019-06-04 09:40:32.231192003 -0600
+@@ -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	2019-05-30 20:27:31.000000000 -0600
+++ src/base/io/ioReadBlifMv.c	2019-06-04 09:40:32.232191985 -0600
+@@ -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	2019-05-30 20:27:31.000000000 -0600
+++ src/base/io/ioWriteAiger.c	2019-06-04 09:40:32.233191967 -0600
+@@ -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/bsat2/MainSat.cpp.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/bsat2/MainSat.cpp	2019-06-04 09:40:32.234191950 -0600
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #include <errno.h>
+ 
+ #include <signal.h>
+-#include "misc/zlib/zlib.h"
+#include <zlib.h>
+ 
+ #include "System.h"
+ #include "ParseUtils.h"
+--- src/sat/bsat2/MainSimp.cpp.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/bsat2/MainSimp.cpp	2019-06-04 09:40:32.234191950 -0600
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #include <errno.h>
+ 
+ #include <signal.h>
+-#include "misc/zlib/zlib.h"
+#include <zlib.h>
+ 
+ #ifndef _WIN32
+ #include <sys/resource.h>
+--- src/sat/bsat2/ParseUtils.h.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/bsat2/ParseUtils.h	2019-06-04 09:40:32.235191932 -0600
+@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #include <stdlib.h>
+ #include <stdio.h>
+ 
+-#include "misc/zlib/zlib.h"
+#include <zlib.h>
+ 
+ namespace Minisat {
+ 
+--- src/sat/cnf/cnfMan.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/cnf/cnfMan.c	2019-06-04 09:40:32.235191932 -0600
+@@ -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
+ 
+--- src/sat/glucose/ParseUtils.h.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/glucose/ParseUtils.h	2019-06-04 09:40:32.236191914 -0600
+@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #include <stdio.h>
+ #include <math.h>
+ 
+-#include "misc/zlib/zlib.h"
+#include <zlib.h>
+ 
+ ABC_NAMESPACE_CXX_HEADER_START
+ 
--- a/abc-format.patch
+++ b/abc-format.patch
@ -0,0 +1,136 @@
+--- src/aig/aig/aigUtil.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/aig/aig/aigUtil.c	2019-06-04 09:42:11.236444258 -0600
+@@ -725,7 +725,7 @@ void Aig_ManPrintVerbose( Aig_Man_t * p,
+ void Aig_ManDump( Aig_Man_t * p )
+ { 
+     static int Counter = 0;
+-    char FileName[20];
+    char FileName[24];
+     // dump the logic into a file
+     sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
+     Aig_ManDumpBlif( p, FileName, NULL, NULL );
+--- src/aig/gia/giaScript.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/aig/gia/giaScript.c	2019-06-04 09:42:11.237444240 -0600
+@@ -610,10 +610,10 @@ void Gia_ManPerformFlow( int fIsMapped,
+ void Gia_ManPerformFlow2( int fIsMapped, int nAnds, int nLevels, int nLutSize, int nCutNum, int fBalance, int fMinAve, int fUseMfs, int fVerbose )
+ {
+     char Comm1[100], Comm2[100], Comm3[100], Comm4[100];
+-    sprintf( Comm1, "&synch2 -K %d -C 500; &if -m%s       -K %d -C %d; %s &save", nLutSize, fMinAve?"t":"", nLutSize, nCutNum,   fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+-    sprintf( Comm2, "&dch -C 500;          &if -m%s       -K %d -C %d; %s &save",           fMinAve?"t":"", nLutSize, nCutNum+4, fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+-    sprintf( Comm3, "&synch2 -K %d -C 500; &lf -m%s  -E 5 -K %d -C %d; %s &save", nLutSize, fMinAve?"t":"", nLutSize, nCutNum,   fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+-    sprintf( Comm4, "&dch -C 500;          &lf -m%sk -E 5 -K %d -C %d; %s &save",           fMinAve?"t":"", nLutSize, nCutNum+4, fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+    snprintf( Comm1, 100U, "&synch2 -K %d -C 500; &if -m%s       -K %d -C %d; %s &save", nLutSize, fMinAve?"t":"", nLutSize, nCutNum,   fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+    snprintf( Comm2, 100U, "&dch -C 500;          &if -m%s       -K %d -C %d; %s &save",           fMinAve?"t":"", nLutSize, nCutNum+4, fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+    snprintf( Comm3, 100U, "&synch2 -K %d -C 500; &lf -m%s  -E 5 -K %d -C %d; %s &save", nLutSize, fMinAve?"t":"", nLutSize, nCutNum,   fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+    snprintf( Comm4, 100U, "&dch -C 500;          &lf -m%sk -E 5 -K %d -C %d; %s &save",           fMinAve?"t":"", nLutSize, nCutNum+4, fUseMfs ? "&put; mfs2 -W 4 -M 500 -C 7000; &get -m;":"" );
+ 
+     // perform synthesis
+     if ( fVerbose )
+--- src/base/abci/abcMiter.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/base/abci/abcMiter.c	2019-06-04 09:42:11.238444223 -0600
+@@ -860,7 +860,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFr
+ {
+     int fVerbose = 0;
+     int NodeBef = Abc_NtkNodeNum(pNtkFrames);
+-    char Buffer[10];
+    char Buffer[12];
+     Abc_Obj_t * pNode, * pLatch;
+     int i;
+     // create the prefix to be added to the node names
+--- src/base/io/ioReadBlifMv.c.orig	2019-06-04 09:40:32.232191985 -0600
+++ src/base/io/ioReadBlifMv.c	2019-06-04 09:42:11.239444205 -0600
+@@ -1656,7 +1656,7 @@ static int Io_MvWriteValues( Abc_Obj_t *
+ ***********************************************************************/
+ static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken, Vec_Str_t * vFunc, int iLit )
+ {
+-    char Buffer[10];
+    char Buffer[12];
+     Io_MvVar_t * pVar;
+     Abc_Obj_t * pFanin, * pNet;
+     char * pCur, * pNext;
+--- src/base/ver/verCore.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/base/ver/verCore.c	2019-06-04 09:42:11.240444188 -0600
+@@ -1171,7 +1171,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan, A
+                 pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
+ 
+                 // get the fanout net
+-                sprintf( Buffer2, "%s[%d]", Buffer, Bit );
+                snprintf( Buffer2, 1000U, "%s[%d]", Buffer, Bit );
+                 pNet = Ver_ParseFindNet( pNtk, Buffer2 );
+                 if ( pNet == NULL )
+                 {
+--- src/base/wlc/wlcNdr.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/base/wlc/wlcNdr.c	2019-06-04 09:42:11.241444170 -0600
+@@ -478,7 +478,7 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData
+     pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
+     for ( i = 1; i <= NameIdMax; i++ )
+     {
+-        char pName[20]; sprintf( pName, "s%0*d", nDigits, i );
+        char pName[20]; snprintf( pName, 20U, "s%0*d", nDigits, i );
+         NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+         assert( !fFound && i == NameId );
+     }
+--- src/base/wln/wlnNdr.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/base/wln/wlnNdr.c	2019-06-04 09:42:11.242444152 -0600
+@@ -256,7 +256,7 @@ Wln_Ntk_t * Wln_NtkFromNdr( void * pData
+     pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
+     for ( i = 1; i <= NameIdMax; i++ )
+     {
+-        char pName[20]; sprintf( pName, "s%0*d", nDigits, i );
+        char pName[20]; snprintf( pName, 20U, "s%0*d", nDigits, i );
+         NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+         assert( !fFound && i == NameId );
+     }
+--- src/bdd/cas/casCore.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/bdd/cas/casCore.c	2019-06-04 09:42:11.243444135 -0600
+@@ -259,7 +259,7 @@ int Abc_CascadeExperiment( char * pFileG
+     if ( fCheck )
+     {
+         char Command[200];
+-        sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
+        snprintf( Command, 200U, "cec %s %s", FileNameIni, FileNameFin );
+         Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
+     }
+ 
+--- src/opt/dau/dauMerge.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/opt/dau/dauMerge.c	2019-06-04 09:42:11.243444135 -0600
+@@ -661,7 +661,7 @@ printf( "%s\n", pDsd1 );
+     nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
+     if ( nVarsShared == 0 )
+     {
+-        sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
+        snprintf( pRes, DAU_MAX_STR, "(%s%s)", pDsd0, pDsd1 );
+ if ( fVerbose )
+ printf( "Disjoint:\n" );
+ if ( fVerbose )
+@@ -715,7 +715,7 @@ Dau_DsdMergeStorePrintDefs( pS );
+ 
+     // create new function
+ //    assert( nVarsTotal <= 6 );
+-    sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
+    snprintf( pS->pOutput, DAU_MAX_STR, "(%s%s)", pDsd0, pDsd1 );
+     pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
+     Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput );
+ //printf( "%d ", Status );
+--- src/proof/fra/fraCore.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/proof/fra/fraCore.c	2019-06-04 09:42:11.243444135 -0600
+@@ -156,7 +156,7 @@ int Fra_FraigMiterAssertedOutput( Aig_Ma
+ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
+ { 
+     static int Counter = 0;
+-    char FileName[20];
+    char FileName[24];
+     Aig_Man_t * pTemp;
+     Aig_Obj_t * pNode;
+     int i;
+--- src/sat/bmc/bmcMaj.c.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/bmc/bmcMaj.c	2019-06-04 09:42:11.243444135 -0600
+@@ -585,7 +585,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int
+     Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars );
+     if ( fCompl )
+         Abc_TtNot( p->pTruth, p->nWords );
+-    sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
+    snprintf( FileName, 1000U, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
+     pFile = fopen( FileName, "wb" );
+     fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes );
+     fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes );
--- a/abc-header.patch
+++ b/abc-header.patch
@ -0,0 +1,10 @@
+--- src/sat/glucose/Glucose.cpp.orig	2019-05-30 20:27:31.000000000 -0600
+++ src/sat/glucose/Glucose.cpp	2019-06-04 09:41:02.469658200 -0600
+@@ -33,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #include "sat/glucose/Solver.h"
+ #include "sat/glucose/Constants.h"
+ #include "sat/glucose/System.h"
+#include "misc/util/abc_global.h"
+ 
+ ABC_NAMESPACE_IMPL_START
+ 
--- a/abc-sharedlib.patch
+++ b/abc-sharedlib.patch
@ -0,0 +1,22 @@
+--- Makefile.orig	2019-06-04 09:40:32.212192338 -0600
+++ Makefile	2019-06-04 09:40:51.291855524 -0600
+@@ -55,7 +55,7 @@ ARCHFLAGS := $(ARCHFLAGS)
+ 
+ OPTFLAGS  ?= -g -O
+ 
+-CFLAGS    += -Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare $(ARCHFLAGS)
+CFLAGS    += -Wno-unused-function $(OPTFLAGS) $(ARCHFLAGS) -Isrc
+ ifneq ($(findstring arm,$(shell uname -m)),)
+ 	CFLAGS += -DABC_MEMALIGN=4
+ endif
+@@ -221,7 +221,9 @@ lib$(PROG).a: $(LIBOBJ)
+ 
+ lib$(PROG).so: $(LIBOBJ)
+ 	@echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
+-	$(VERBOSE)$(CXX) -shared -o $@ $^ $(LIBS)
+	$(VERBOSE)$(CXX) -shared -Wl,-h,lib$(PROG).so.0 -o lib$(PROG).so.0.0.0 $^ $(LIBS)
+	$(VERBOSE)ln -s lib$(PROG).so.0.0.0 lib$(PROG).so.0
+	$(VERBOSE)ln -s lib$(PROG).so.0 $@
+ 
+ docs:
+ 	@echo "$(MSG_PREFIX)\`\` Building documentation." $(notdir $@)
--- a/abc.1
+++ b/abc.1
@ -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.
--- a/abc.spec
+++ b/abc.spec
@ -0,0 +1,207 @@
+# Upstream doesn't make releases.  We have to check the code out of git.
+%global owner    berkeley-abc
+%global gittag   35280f30504ad16f1d0ab005905883bee883747c
+%global shorttag %(cut -b -7 <<< %{gittag})
+%global gitdate  20190608
+
+# WARNING: When updating to a newer snapshot, because upstream doesn't do
+# shared library versioning, run abipkgdiff (from libabigail) against the
+# old and new binary and debuginfo packages to detect abi changes that would
+# require bumping the shared library version, e.g.,
+#   abipkgdiff --d1 abc-libs-debuginfo-<old>.rpm \
+#              --d2 abc-libs-debuginfo-<new>.rpm \
+#              --devel1 abc-devel-<old>.rpm \
+#              --devel2 abc-devel-<new>.rpm \
+#              abc-libs-<old>.rpm abc-libs-<new>.rpm
+# If the shared library version is bumped, remember to rebuild dependent
+# packages, finding them using e.g.
+#   repoquery --whatrequires abc-libs
+# This should be done for each branch in which abc-libs will be updated.
+
+Name:           abc
+Version:        1.01
+Release:        23.git%{gitdate}%{?dist}
+Summary:        Sequential logic synthesis and formal verification
+
+License:        MIT
+URL:            http://www.eecs.berkeley.edu/~alanmi/abc/abc.htm
+Source0:        https://github.com/%{owner}/%{name}/archive/%{gittag}/%{name}-%{shorttag}.tar.gz
+# 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
+# Fix a minor header issue
+Patch2:         %{name}-header.patch
+# Set an soname on the library
+Patch3:         %{name}-build.patch
+# Fix sprintf calls that can overflow their buffers
+Patch4:         %{name}-format.patch
+
+BuildRequires:  bzip2-devel
+BuildRequires:  cmake
+BuildRequires:  gcc-c++
+BuildRequires:  readline-devel
+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
+# ABC includes a bundled and modified version of CUDD 2.4.2, which is
+# incompatible with the Fedora-provided CUDD 3.0.0.
+Provides:       bundled(cudd) = 2.4.2
+
+%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.
+
+%prep
+%autosetup -p0 -n %{name}-%{gittag}
+
+# Do not use the bundled libraries
+rm -fr lib src/misc/{bzlib,zlib}
+
+# Set the version number in the man page
+sed 's/@VERSION@/%{version} (%{gitdate})/' %{SOURCE1} > %{name}.1
+touch -r %{SOURCE1} %{name}.1
+
+%build
+export CFLAGS="%{optflags} -DNDEBUG -I%{_includedir}/cudd"
+export CXXFLAGS="$CFLAGS"
+%cmake -DCMAKE_SKIP_RPATH:BOOL=YES -DCMAKE_SKIP_INSTALL_RPATH:BOOL=YES .
+%make_build ABC_MAKE_VERBOSE=1 ABC_USE_STDINT_H=1
+
+%install
+# 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
+pushd src
+mkdir -p %{buildroot}%{_includedir}/%{name}
+tar -cBf - $(find -O3 . -name \*.h) | \
+  (cd %{buildroot}%{_includedir}/%{name}; tar -xBf -)
+popd
+
+# Install the binary
+mkdir -p %{buildroot}%{_bindir}
+install -p -m 0755 %{name} %{buildroot}%{_bindir}
+
+# Install the man page
+mkdir -p %{buildroot}%{_mandir}/man1
+install -p -m 0644 %{name}.1 %{buildroot}%{_mandir}/man1
+
+%files
+%doc README.md readmeaig
+%{_bindir}/%{name}
+%{_mandir}/man1/%{name}*
+
+%files libs
+%license copyright.txt
+%{_libdir}/lib%{name}.so.*
+
+%files devel
+%{_includedir}/%{name}/
+%{_libdir}/lib%{name}.so
+
+%changelog
+* Wed Jul 24 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-23.git20190608
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Wed Jun 12 2019 Jerry James <loganjerry@gmail.com> - 1.01-22.git20190608
+- Update to latest git snapshot
+- Add -build and -format patches
+- Build with cmake
+- Enable CUDD support
+
+* Sun Feb 17 2019 Igor Gnatenko <ignatenkobrain@fedoraproject.org> - 1.01-21.git20181121
+- Rebuild for readline 8.0
+
+* Thu Jan 31 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-20.git20181121
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Mon Nov 26 2018 Jerry James <loganjerry@gmail.com> - 1.01-19.git20181121
+- Update to latest git snapshot
+
+* Thu Jul 12 2018 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-18.git20180708
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Tue Jul 10 2018 Jerry James <loganjerry@gmail.com> - 1.01-17.git20180708
+- Update to latest git snapshot
+
+* Sat Mar  3 2018 Jerry James <loganjerry@gmail.com> - 1.01-16.hg20180228
+- Update to latest mercurial snapshot
+- BR gcc-c++ instead of gcc
+
+* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-15.hg20180129
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Fri Feb  2 2018 Jerry James <loganjerry@gmail.com> - 1.01-14.hg20180129
+- Update to latest mercurial snapshot
+
+* Wed Aug 02 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-13.hg20160905
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
+
+* Wed Jul 26 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-12.hg20160905
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
+
+* Fri Feb 10 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-11.hg20160905
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Thu Jan 12 2017 Igor Gnatenko <ignatenko@redhat.com> - 1.01-10.hg20160905
+- Rebuild for readline 7.x
+
+* Sat Sep 10 2016 Eric Smith <brouhaha@fedoraproject.org> - 1.01-9.hg20160905
+- Update to latest mercurial snapshot
+
+* Fri Feb  5 2016 Jerry James <loganjerry@gmail.com> - 1.01-8.hg20160203
+- Update to latest mercurial snapshot
+- Drop the python2 subpackage; upstream moved support to a separate project
+
+* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 1.01-7.hg20150306
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Tue Jun 16 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.01-6.hg20150306
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
+
+* Sat May 02 2015 Kalev Lember <kalevlember@gmail.com> - 1.01-5.hg20150306
+- Rebuilt for GCC 5 C++11 ABI change
+
+* Sat Mar  7 2015 Jerry James <loganjerry@gmail.com> - 1.01-4.hg20150306
+- Update to latest mercurial snapshot
+
+* Thu Jan  1 2015 Jerry James <loganjerry@gmail.com> - 1.01-3.hg20150101
+- Update to latest mercurial snapshot
+- Fix installation of header files
+
+* 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
--- a/dead.package
+++ b/dead.package
@ -1 +0,0 @@
-Superseded by yosyshq-abc
--- a/1
+++ b/1
@ -0,0 +1 @@
+SHA512 (abc-35280f3.tar.gz) = d18c6509ad0efa2c98cbd3aa5d22d3b302147bad34fa438100b603febded2df7ea16040c766ebc17b6ac35b84a41bf453907560885c26d5a47a76440b097c3fa
				`@ -0,0 +1 @@`
				`SHA512 (abc-35280f3.tar.gz) = d18c6509ad0efa2c98cbd3aa5d22d3b302147bad34fa438100b603febded2df7ea16040c766ebc17b6ac35b84a41bf453907560885c26d5a47a76440b097c3fa`