Commit c3498e2c authored by Théotime BOLLENGIER's avatar Théotime BOLLENGIER
Browse files

add code

parent 7734c9cc

Too many changes to show.

To preserve performance only 86 of 86+ files are displayed.
*.o
*.swp
*.log
*.d
ext/Makefile
ext/ruby_abc.so
ext/abc/arch_flags
ext/abc/libabc.so
lib/ruby_abc/ruby_abc.so
doc
ruby_abc-*.gem
MIT License
Copyright (c) 2017 Théotime Bollengier <theotime.bollengier@gmail.com>
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
Directory ext/abc is cloned from https://bitbucket.org/alanmi/abc on 2017-11-22 (hg clone https://bitbucket.org/alanmi/abc)
ABC: System for Sequential Synthesis and Verification
http://www.eecs.berkeley.edu/~alanmi/abc/
Copyright (c) The Regents of the University of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
--------------------------------------------------------------------------------
ruby_abc: A ruby C extension to use ABC from ruby
https://gitlab.ensta-bretagne.fr/argen/ruby_abc
Copyright (c) 2017 Théotime Bollengier. All rights reserved.
Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE AUTHOR BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHOR
HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE AUTHOR SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE AUTHOR HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
# ruby_abc
A ruby C extension wrapping the Berkeley synthesis and verification program ABC.
\ No newline at end of file
ruby\_abc ruby C extension
==========================
**ruby\_abc** is a ruby C extension wrapping the Berkeley logic synthesis system *abc*.
*abc* is a system for sequential synthesis and verification,
developped at the University of California, Berkeley.
*abc* documentation can be found on its website:
[http://people.eecs.berkeley.edu/~alanmi/abc/](https://people.eecs.berkeley.edu/~alanmi/abc/)
The source code of *abc* is included in this gem,
it was cloned on 2017/11/22 from :
[https://bitbucket.org/alanmi/abc](https://bitbucket.org/alanmi/abc)
Goal
----
The *abc* program is a command line interface: the user issues commands and adjust them according to the results he gets back.
For example, the user can iterrate through minimization commands, and stops when the number of nodes of the logic network stops decreasing.
To automate this process, it is possible to give *abc* a predefined sequence of commands.
In this case, however, the number of minimization command can be too short, and the resulting network will be bigger than it could be.
The number of minimization command can also be too big, and the process will take more time than needed to execute.
In order to solve this process, *ruby_abc* allows to retreive some information on the current logic network in ruby,
such as the number of nodes or its logic level, to allow automation.
In the example of the minimization of a logic network, minimization commands are sent to *abc* in a ruby loop which breaks
when the number of nodes stops decreasing.
Example
-------
```ruby
require 'ruby_abc'
## Load a netlist ##
ABC.read 'test/generic_netlist.blif'
## Print informations on the logic network ##
ABC.print_stats
puts ABC.nb_nodes
## Minimize the network ##
ABC.optimize # itera through minimization commands and stops when the number of nodes reach a plateau
## Retime the network ##
ABC.retime
## Map the network to 4-intpu LUTs (break the network in logic functions not exceeding 4 inputs) ##
n_nodes = ABC.nb_nodes
loop do
ABC.run_command 'choice; if -K 4; ps'
break if ABC.nb_nodes == n_nodes
n_nodes = ABC.nb_nodes
end
# is equivalent to:
ABC.map 4
## Write the network to an output file ##
ABC.write 'mapped_netlist.blif'
```
Installation
------------
To install *ruby_abc* from the git repository:
```bash
git clone https://gitlab.ensta-bretagne.fr/argen/ruby_abc.git
$ cd ruby_abc
$ gem build ruby_abc.gemspec
$ gem install ruby_abc.<version>.gem
```
Alternatively, *ruby_abc* gem is also hosted on RubyGems ([https://rubygems.org/gems/ruby_abc](https://rubygems.org/gems/ruby_abc)).
So you can simply type:
```bash
gem install ruby_abc
```
This will build *abc* and the *ruby_abc* extension, and install it.
Building *abc* may take quite some time.
To speed up the build, you may `export MAKEFLAGS=' -j8 '` before installing the gem.
As this gem includes a C extension, building it requires the ruby developpement headers.
On Debian, you can get them with:
```bash
sudo apt-get install ruby-dev
```
Executable
----------
To use *ruby_abc* directly from a terminal or a Makefile,
this gem also include the `ruby_abc` executable script, which uses command line arguments.
```lang-none
$ ruby_abc --help
Usage: rubyabc_synthesis [options] -i <input_file> -o <output_file>
-i, --input FILE Input BLIF file
-o, --output FILE Output netlist to FILE
-r, --retime Retime netlist
-z, --zero Set latches initial value to zero
-l, --lcorr Computes latch correspondence using 1-step induction
-a, --area Optimize for area instead of performance (minimize the number of nodes instead of the logic level)
-w, --sweep Sweep logic network to remove dangling nodes
-k, --lut_inputs K Map to K-input LUTs.
-h, --help Display this help
```
The *abc* executable is also included so that it can be used natively without ruby.
Documentation
-------------
Html documentation for *ruby_abc* can be generated with `rake doc`.
This documentation covers only the API of *ruby_abc*, not *abc* itself.
*abc* documentation can be found on [http://people.eecs.berkeley.edu/~alanmi/abc/](https://people.eecs.berkeley.edu/~alanmi/abc/).
Also, available *abc* commands can be retreived with `ABC.help` (in ruby),
and specific command documentation can be seen with `ABC.run_command('<command_name> -h')` (in ruby).
Test
----
`$ rake test` will execute `test/test_ruby_abc.rb`.
This will read a BLIF netlist, optimize it and check the result against a golden model.
require 'rake'
require 'mkmf'
require 'fileutils'
root_path = File.dirname(File.expand_path(__FILE__))
ext_path = File.join(root_path, 'ext')
test_path = File.join(root_path, 'test')
lib_path = File.join(root_path, 'lib')
ilib_path = File.join(lib_path, 'ruby_abc')
abc_path = File.join(ext_path, 'abc')
rubyabcext = File.join(ilib_path, 'ruby_abc.so')
rubyabcsrc = Rake::FileList["#{ext_path}/*.c", "#{ext_path}/*.h"]
abcsrc = Rake::FileList["#{abc_path}/**/*.c", "#{abc_path}/**/*.h"]
libabc = File.join(abc_path, 'libabc.so')
docsrcfiles = Rake::FileList["#{ext_path}/*.c", "#{ext_path}/*.h", "lib/ruby_abc.rb", "README.md"]
desc 'build the gem'
task :default => :compile
desc 'build extension'
task :compile => rubyabcext
desc 'compile extension'
task rubyabcext => ([libabc] + rubyabcsrc) do
wd = Dir.getwd
Dir.chdir ext_path
sh "ruby extconf.rb"
sh "make"
Dir.chdir wd
sh "mkdir -p '#{ilib_path}'"
sh "cp '#{File.join(ext_path, 'ruby_abc.so')}' '#{rubyabcext}'"
end
desc 'compile libabc.so and abc'
task libabc => abcsrc do
abort "Library libpthread was not found" if !have_library('pthread')
abort "Library libdl was not found" if !have_library('dl')
#abort "Library librt was not found" if !have_library('rt') ## librt.a is not on Mac OS
wd = Dir.getwd
Dir.chdir(abc_path)
sh "make ABC_USE_PIC=true OPTFLAGS='-O2' ABC_USE_NO_READLINE=true libabc.so"
sh "make ABC_USE_PIC=true OPTFLAGS='-O2' ABC_USE_NO_READLINE=true abc"
Dir.chdir(wd)
FileUtils.move(File.join(abc_path, 'abc'), File.join(root_path, 'bin', 'abc'), force: true)
end
desc 'Test ruby_abc'
task :test => rubyabcext do
sh "ruby '#{File.join(test_path, 'test_ruby_abc.rb')}'"
end
desc 'Generate html documentation'
task :doc do
sh "rdoc --main=README.md --title='ruby_abc ruby extension' --output='#{File.join(root_path, 'doc')}' #{docsrcfiles}"
end
desc 'Cleanup build files'
task :clean do
extmakefile = File.join(ext_path, 'Makefile')
if File.exist? extmakefile
wd = Dir.getwd
Dir.chdir ext_path
sh "make -f '#{extmakefile}' clean"
Dir.chdir wd
end
abcmakefile = File.join(abc_path, 'Makefile')
if File.exist? abcmakefile
wd = Dir.getwd
Dir.chdir abc_path
sh "make -f '#{abcmakefile}' clean"
Dir.chdir wd
end
sh "rm -rvf '#{File.join(root_path, 'doc')}'"
end
desc 'Cleanup everyting'
task :mrproper => :clean do
sh "rm -vf '#{File.join(ext_path, 'Makefile')}'"
sh "rm -rvf '#{ilib_path}'"
sh "rm -vf '#{File.join(root_path, 'bin', 'abc')}'"
end
#! /usr/bin/env ruby
require 'optparse'
require_relative '../lib/ruby_abc.rb'
STDOUT.sync = true
options = {}
optparse = OptionParser.new do |opts|
opts.banner = "Usage: #{File.basename($0)} [options] -i <input_file> -o <output_file>"
options[:inputFileName] = nil
opts.on('-i', '--input FILE', 'Input file') do |file|
options[:inputFileName] = file
end
options[:outputFileName] = nil
opts.on('-o', '--output FILE', 'Write processed netlist to FILE') do |file|
options[:outputFileName] = file
end
options[:sweep] = false
opts.on('-s', '--sweep', 'Sweep logic network to remove dangling nodes') do
options[:sweep] = true
end
options[:k] = nil
opts.on('-k', '--lut_inputs K', "Map to K-input LUTs.") do |k|
options[:k] = k.to_i
end
options[:area] = false
opts.on('-a', '--area', 'Optimize in area') do
options[:area] = true
end
options[:retime] = false
opts.on('-r', '--retime', 'Retime netlist') do
options[:retime] = true
end
options[:lcorr] = false
opts.on('-l', '--lcorr', 'Computes latch correspondence using 1-step induction') do
options[:lcorr] = true
end
options[:zero] = false
opts.on('-z', '--zero', 'Set latches initial value to zero') do
options[:zero] = true
end
options[:echo] = false
opts.on('-e', '--echo', 'Echo commands sent to ABC') do
options[:echo] = true
end
options[:quiet] = false
opts.on('-q', '--quiet', 'Do not print netlist statistics during synthesis') do
options[:quiet] = true
end
opts.on( '-h', '--help', 'Display this help' ) do
puts opts
exit
end
end
optparse.parse!
abort "Missing input file name.\n#{optparse}" if options[:inputFileName].nil?
ABC::echo_commands = not(not(options[:echo]))
ABC::synthesis(
input: options[:inputFileName],
output: options[:outputFileName],
zero: options[:zero],
sweep: options[:sweep],
retime: options[:retime],
lcorr: options[:lcorr],
area: options[:area],
lut_map: options[:k],
verbose: not(options[:quiet])
)
cmake_minimum_required(VERSION 3.3.0)
include(CMakeParseArguments)
include(CheckCCompilerFlag)
include(CheckCXXCompilerFlag)
function(addprefix var prefix)
foreach( s ${ARGN} )
list(APPEND tmp "-I${s}")
endforeach()
set(${var} ${tmp} PARENT_SCOPE)
endfunction()
# filter out flags that are not appropriate for the compiler being used
function(target_compile_options_filtered target visibility)
foreach( flag ${ARGN} )
if( flag MATCHES "^-D.*" )
target_compile_options( ${target} ${visibility} ${flag} )
else()
check_c_compiler_flag( ${flag} C_COMPILER_SUPPORTS__${flag} )
if( C_COMPILER_SUPPORTS__${flag} )
target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:C>:${flag}> )
endif()
check_cxx_compiler_flag( ${flag} CXX_COMPILER_SUPPORTS__${flag} )
if( CXX_COMPILER_SUPPORTS__${flag} )
target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:CXX>:${flag}> )
endif()
endif()
endforeach()
endfunction()
project(abc)
if(READLINE_FOUND MATCHES TRUE)
addprefix(ABC_READLINE_INCLUDES_FLAGS "-I" ${READLINE_INCLUDE})
string(REPLACE ";" " " ABC_READLINE_INCLUDES_FLAGS "${ABC_READLINE_INCLUDES_FLAGS}")
list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_INCLUDES=${ABC_READLINE_INCLUDES_FLAGS}")
string(REPLACE ";" " " ABC_READLINE_LIBRARIES_FLAGS "${READLINE_LIBRARIES}")
list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_LIBRARIES=${ABC_READLINE_LIBRARIES_FLAGS}")
elseif(READLINE_FOUND MATCHES FALSE)
list(APPEND ABC_READLINE_FLAGS "ABC_USE_NO_READLINE=1")
endif()
if(ABC_USE_NAMESPACE)
set(ABC_USE_NAMESPACE_FLAGS "ABC_USE_NAMESPACE=${ABC_USE_NAMESPACE}")
endif()
# run make to extract compiler options, linker options and list of source files
execute_process(
COMMAND
make
${ABC_READLINE_FLAGS}
${ABC_USE_NAMESPACE_FLAGS}
ARCHFLAGS_EXE=${CMAKE_CURRENT_BINARY_DIR}/abc_arch_flags_program.exe
ABC_MAKE_NO_DEPS=1
CC=${CMAKE_C_COMPILER}
CXX=${CMAKE_CXX_COMPILER}
LD=${CMAKE_CXX_COMPILER}
cmake_info
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
OUTPUT_VARIABLE MAKE_OUTPUT
)
# extract options from make output
function(extract_var SEPARATOR DEST_VARIABLE MAKE_OUTPUT)
string(REGEX MATCH "${SEPARATOR} .* ${SEPARATOR}" TMP "${MAKE_OUTPUT}")
string(REGEX REPLACE "${SEPARATOR} (.*) ${SEPARATOR}" "\\1" TMP "${TMP}")
separate_arguments(TMP)
set(${DEST_VARIABLE} ${TMP} PARENT_SCOPE)
endfunction()
extract_var(SEPARATOR_SRC ABC_SRC ${MAKE_OUTPUT})
extract_var(SEPARATOR_LIBS ABC_LIBS ${MAKE_OUTPUT})
extract_var(SEPARATOR_CFLAGS ABC_CFLAGS ${MAKE_OUTPUT})
extract_var(SEPARATOR_CXXFLAGS ABC_CXXFLAGS ${MAKE_OUTPUT})
if(ABC_USE_NAMESPACE)
set_source_files_properties(${ABC_SRC} PROPERTIES LANGUAGE CXX)
endif()
function(abc_properties target visibility)
target_include_directories(${target} ${visibility} ${CMAKE_CURRENT_SOURCE_DIR}/src )
target_compile_options_filtered(${target} ${visibility} ${ABC_CFLAGS} ${ABC_CXXFLAGS} -Wno-unused-but-set-variable )
target_link_libraries(${target} ${visibility} ${ABC_LIBS})
endfunction()
add_executable(abc ${ABC_SRC})
abc_properties(abc PRIVATE)
list(REMOVE_ITEM ABC_SRC src/base/main/main.c)
add_library(libabc EXCLUDE_FROM_ALL ${ABC_SRC})
abc_properties(libabc PUBLIC)
set_property(TARGET libabc PROPERTY OUTPUT_NAME abc)
add_library(libabc-pic EXCLUDE_FROM_ALL ${ABC_SRC})
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)
CC := gcc
CXX := g++
LD := $(CXX)
MSG_PREFIX ?=
ABCSRC = .
$(info $(MSG_PREFIX)Using CC=$(CC))
$(info $(MSG_PREFIX)Using CXX=$(CXX))
$(info $(MSG_PREFIX)Using LD=$(LD))
PROG := abc
MODULES := \
$(wildcard src/ext*) \
src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/exor \
src/base/ver src/base/wlc src/base/acb src/base/bac src/base/cba src/base/pla src/base/test \
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/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 \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/bool/rsb src/bool/rpo \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/aig/miniaig
all: $(PROG)
default: $(PROG)
ARCHFLAGS_EXE ?= ./arch_flags
$(ARCHFLAGS_EXE) : arch_flags.c
$(CC) arch_flags.c -o $(ARCHFLAGS_EXE)
INCLUDES += -I$(ABCSRC)/src
ARCHFLAGS ?= $(shell $(CC) $(ABCSRC)/arch_flags.c -o $(ARCHFLAGS_EXE) && $(ARCHFLAGS_EXE))
ARCHFLAGS := $(ARCHFLAGS)
OPTFLAGS ?= -g -O
CFLAGS += -Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare $(ARCHFLAGS)
ifneq ($(findstring arm,$(shell uname -m)),)
CFLAGS += -DABC_MEMALIGN=4
endif
# compile ABC using the C++ comipler and put everything in the namespace $(ABC_NAMESPACE)
ifdef ABC_USE_NAMESPACE
CFLAGS += -DABC_NAMESPACE=$(ABC_USE_NAMESPACE) -fpermissive
CC := $(CXX)
$(info $(MSG_PREFIX)Compiling in namespace $(ABC_NAMESPACE))
endif
# compile CUDD with ABC
ifndef ABC_USE_NO_CUDD
CFLAGS += -DABC_USE_CUDD=1
MODULES += src/bdd/cudd src/bdd/extrab src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/reo src/bdd/cas src/bdd/bbr src/bdd/llb
$(info $(MSG_PREFIX)Compiling with CUDD)
endif
ABC_READLINE_INCLUDES ?=
ABC_READLINE_LIBRARIES ?= -lreadline
# whether to use libreadline
ifndef ABC_USE_NO_READLINE
CFLAGS += -DABC_USE_READLINE $(ABC_READLINE_INCLUDES)
LIBS += $(ABC_READLINE_LIBRARIES)
$(info $(MSG_PREFIX)Using libreadline)
endif
# whether to compile with thread support
ifndef ABC_USE_NO_PTHREADS
CFLAGS += -DABC_USE_PTHREADS
LIBS += -lpthread
$(info $(MSG_PREFIX)Using pthreads)
endif
# whether to compile into position independent code
ifdef ABC_USE_PIC
CFLAGS += -fPIC
LIBS += -fPIC
$(info $(MSG_PREFIX)Compiling position independent code)
endif
# whether to echo commands while building
ifdef ABC_MAKE_VERBOSE
VERBOSE=
else
VERBOSE=@
endif
# Set -Wno-unused-bug-set-variable for GCC 4.6.0 and greater only
ifneq ($(or $(findstring gcc,$(CC)),$(findstring g++,$(CC))),)
empty:=
space:=$(empty) $(empty)
GCC_VERSION=$(shell $(CC) -dumpversion)
GCC_MAJOR=$(word 1,$(subst .,$(space),$(GCC_VERSION)))