Sometimes fiction is more easily understood than true events (v0.3.2) (…

…#9)

This version adds a novel One-pass Synthesis algorithm for Physical Design that combines logic synthesis and placement & routing into a single step. Many thanks to Winston Haaswijk for the collaboration on this project!

.gitignore

@@ -8,3 +8,4 @@ build/
 *.synctex.gz
 /.vs
 *.json
+__pycache__

.travis.yml

@@ -20,7 +20,7 @@ script:
 - mkdir -p build
 - cd build
 # set compiler, python executable, and Z3 build verbosity
-- cmake -DCMAKE_CXX_COMPILER=$COMPILER -DPYTHON_EXECUTABLE=$(which $PY_CMD) -DBUILD_Z3_VERBOSE=TRUE -DENABLE_PROGRESS_BARS=OFF ..
+- cmake -DCMAKE_CXX_COMPILER=$COMPILER -DPYTHON_EXECUTABLE=$(which $PY_CMD) -DBUILD_LIBS_VERBOSE=TRUE -DENABLE_PROGRESS_BARS=OFF ..
 # build fiction
 - make -j2
 # run integration tests

CHANGELOG.md

@@ -3,6 +3,22 @@ All notable changes to this project will be documented in this file.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
+## v0.3.2 - 2021-01-06
+*Sometimes fiction is more easily understood than true events.* — Young-ha Kim
+
+### Added
+- Command `onepass` for a combined SAT-based logic synthesis and physical design using [Mugen](https://github.com/whaaswijk/mugen). Thanks to Winston Haaswijk for cooperating with me on this project!
+- SVG output for irregular (cell-based) clocked `fcn_cell_layout`s (thanks to Gregor Kuhn!)
+- `csv_writer` for conveniently formatting experiments' results
+- `tt_reader` for reading truth tables from a [file format used by Alan Mishchenko](https://people.eecs.berkeley.edu/~alanmi/temp5/)
+
+### Changed
+- `exact --asynchronous/-a` has been renamed to `exact --async/-a` and `exact --asynchronous_max/-A` has been renamed to `exact --async_max`
+- outsourced Verilog and AIGER file handling into a distinct `network_reader` class so that it can be used in custom experiments
+
+### Fixed
+- `Docker` build that broke down due to updates to `mockturtle` and `bill`
+
 ## v0.3.1 - 2020-06-04
 *There is no doubt fiction makes a better job of the truth.* — Doris Lessing
 
@@ -30,9 +46,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Moved to the latest releases of all libraries
 
 ### Fixed
+- Python detection in CMake under different versions
 - Runtime logging in `exact`
 - Performance issues in `ortho`
-- Python detection in CMake under different versions
+- SEGFAULTS caused by `ortho` on large networks when compiling with gcc
 - `ortho -b` losing bent wire connections
 - `fcn_layout::random_face`'s index to coordinate mapping again, but for real now (thanks to Till Schlechtweg!)
 - `logic_network`s are deep-copied for each physical design call now to secure them from external changes

CMakeLists.txt

@@ -1,7 +1,7 @@
 cmake_minimum_required(VERSION 3.2)
 project(fiction
         LANGUAGES CXX
-        VERSION 0.3.1)
+        VERSION 0.3.2)
 
 # C++17
 set(CMAKE_CXX_STANDARD 17)
@@ -30,6 +30,12 @@ if (NOT WIN32)
     endif ()
 endif()
 
+# Enable Mugen
+option(ENABLE_MUGEN "Enable the usage of Mugen, a Python3 library by Winston Haaswijk for FCN one-pass synthesis, and its dependencies" ON)
+if (ENABLE_MUGEN)
+    add_definitions(-DMUGEN)
+endif ()
+
 # Include header files
 include_directories(src/algo/ src/io/ src/io/cmd/ src/tech/ src/topo/ src/util/)
 
@@ -53,26 +59,27 @@ else ()
 	link_directories(${Boost_CUSTOM_LIBRARY_DIRS})
 endif ()
 
+# Add option to compile libraries with verbose output
+option(BUILD_LIBS_VERBOSE "Output status and warnings during library build" OFF)
+# Use /dev/null to silence libraries. Not elegant but efficient
+if (NOT BUILD_LIBS_VERBOSE)
+    set(LIB_OUTPUT_CHANNEL > /dev/null)
+endif ()
+
 # Custom install prefix for libraries
 set(LIB_PREFIX ${CMAKE_SOURCE_DIR}/libs)
 
 # Set up a directory for Z3 solver
-set(Z3_DIR ${CMAKE_BINARY_DIR}/z3)
+set(Z3_DIR ${PROJECT_BINARY_DIR}/z3)
 
 if (UNIX)
     # Require Python interpreter
     if (${CMAKE_VERSION} VERSION_LESS "3.12.0")
         find_package(PythonInterp)  # deprecated since CMake 3.12, but works far better
         set(Z3_PYTHON ${PYTHON_EXECUTABLE})
     else ()
-        find_package(Python COMPONENTS Interpreter)
-        set(Z3_PYTHON ${Python_EXECUTABLE})
-    endif ()
-    # Add option to compile Z3 with verbose output
-    option(BUILD_Z3_VERBOSE "Output status and warnings during Z3 build" OFF)
-    # Use /dev/null to silence Z3. Not elegant but efficient
-    if (NOT BUILD_Z3_VERBOSE)
-        set(Z3_OUTPUT_CHANNEL > /dev/null)
+        find_package(Python3 COMPONENTS Interpreter Development)
+        set(Z3_PYTHON ${Python3_EXECUTABLE})
     endif ()
 
     # Add option to build Z3 as a static library
@@ -96,9 +103,9 @@ if (UNIX)
     add_custom_command(
             OUTPUT ${Z3_LIB_DIR}/${Z3_LINK_TARGET}
             PRE_BUILD
-            COMMAND ${Z3_PYTHON} scripts/mk_make.py -s --prefix=${Z3_DIR} ${Z3_LIB_FLAG} ${Z3_OUTPUT_CHANNEL}
-            COMMAND $(MAKE) -C build ${Z3_OUTPUT_CHANNEL}
-            COMMAND $(MAKE) -C build install ${Z3_OUTPUT_CHANNEL}
+            COMMAND ${Z3_PYTHON} scripts/mk_make.py -s --prefix=${Z3_DIR} ${Z3_LIB_FLAG} ${LIB_OUTPUT_CHANNEL}
+            COMMAND $(MAKE) -C build ${LIB_OUTPUT_CHANNEL}
+            COMMAND $(MAKE) -C build install ${LIB_OUTPUT_CHANNEL}
             WORKING_DIRECTORY ${LIB_PREFIX}/z3/)
 
     # Make sure Z3's custom build commands are actually being executed
@@ -125,11 +132,28 @@ add_subdirectory(${LIB_PREFIX}/alice/)
 # Include mockturtle
 add_subdirectory(${LIB_PREFIX}/mockturtle/)
 
+# Build glucose-syrup-4.1-parallel if Mugen is enabled
+if (ENABLE_MUGEN)
+    add_custom_command(
+            OUTPUT ${PROJECT_BINARY_DIR}/glucose-syrup
+            PRE_BUILD
+            COMMAND make ${LIB_OUTPUT_CHANNEL}
+            COMMAND mv glucose-syrup ${PROJECT_BINARY_DIR}/glucose-syrup ${LIB_OUTPUT_CHANNEL}
+            COMMAND make clean ${LIB_OUTPUT_CHANNEL}
+            WORKING_DIRECTORY ${LIB_PREFIX}/mugen/glucose-syrup-4.1/parallel/)
+
+    # Make sure glucose's custom build commands are actually being executed
+    add_custom_target(glucose_syrup
+            ALL
+            DEPENDS ${PROJECT_BINARY_DIR}/glucose-syrup)
+endif ()
+
 # Build executable
 add_executable(fiction ${SOURCES})
 if (UNIX)
     add_dependencies(fiction z3)
 endif ()
 
-# Link against Boost, Z3, alice, and lorina
-target_link_libraries(fiction ${Boost_FILESYSTEM_LIBRARIES} ${Boost_SYSTEM_LIBRARIES} ${Z3_LIB_DIR}/${Z3_LINK_TARGET} alice mockturtle)
+# Link against Boost, Z3, alice, lorina, and pybind11
+target_link_libraries(fiction PRIVATE ${Boost_FILESYSTEM_LIBRARIES} ${Boost_SYSTEM_LIBRARIES}
+                                      ${Z3_LIB_DIR}/${Z3_LINK_TARGET} alice mockturtle pybind11::embed ${Python3_LIBRARIES})

Dockerfile

@@ -10,7 +10,7 @@ ARG NUMBER_OF_JOBS=1
         cmake cmake-doc extra-cmake-modules extra-cmake-modules-doc \
     #
     # Install packages needed to build fiction
-        git g++ cmake boost-dev python readline-dev
+        git g++ cmake boost-dev python3 python3-dev readline-dev zlib-dev
 
 # Clone the repository including submodules
 RUN git clone --recursive https://github.com/marcelwa/fiction.git

README.md

@@ -1,6 +1,7 @@
 # Let there be a fiction
 
 [![Build Status](https://travis-ci.com/marcelwa/fiction.svg?branch=master)](https://travis-ci.com/marcelwa/fiction)
+[![deepcode](https://www.deepcode.ai/api/gh/badge?key=eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJwbGF0Zm9ybTEiOiJnaCIsIm93bmVyMSI6Im1hcmNlbHdhIiwicmVwbzEiOiJmaWN0aW9uIiwiaW5jbHVkZUxpbnQiOmZhbHNlLCJhdXRob3JJZCI6MTU1MTUsImlhdCI6MTYxMDAxNTE1OH0.CGPNrF5TRz3lojNPfCoM_dOBS8Qxm8aZ1IzlvHfbRA0)](https://www.deepcode.ai/app/gh/marcelwa/fiction/_/dashboard?utm_content=gh%2Fmarcelwa%2Ffiction)
 
 This code base provides a framework for **fi**eld-**c**oupled **t**echnology-**i**ndependent **o**pen **n**anocomputing
 in C++17 using the [EPFL Logic Synthesis Libraries](https://github.com/lsils/lstools-showcase). *fiction* focuses on the
@@ -16,7 +17,7 @@ technologies, and cell types, these can easily be compiled down to any desired F
 
 ### Implemented physical design algorithms
 
-Thus for, *fiction* provides two types of physical design approaches.
+Thus for, *fiction* provides three physical design approaches.
 
 First, an [exact approach](https://ieeexplore.ieee.org/document/8342060)
 ([PDF](http://www.informatik.uni-bremen.de/agra/doc/konf/2018DATE_ExactMethodforDesignExplorationOfQCA.pdf)) determines
@@ -32,7 +33,15 @@ is implemented which is based on Orthogonal Graph Drawing (OGD). It has a huge r
 Although the layouts generated by this approach are not optimal in terms of area, this technique is applicable even for larger
 circuits and provides results in reasonable runtime. (See [OGD-based physical design](#ogd-based-ortho).)
 
-This is ongoing research and more algorithms are to come!
+Finally, an experimental [one-pass algorithm](http://www.informatik.uni-bremen.de/agra/doc/konf/ASP-DAC2021_One-pass_Synthesis_for_Field-coupled_Nanocomputing_Technologies.pdf)
+([PDF](http://www.informatik.uni-bremen.de/agra/doc/konf/ASP-DAC2021_One-pass_Synthesis_for_Field-coupled_Nanocomputing_Technologies.pdf))
+is provided that uses SAT solver calls to perform logic synthesis and physical design combined in a single run. This
+enables absolute minimality, but has the largest runtime overhead. Thereby, it is not suited for large-scale circuits.
+(See [SAT-based one-pass synthesis](#sat-based-one-pass-synthesis-onepass).)
+
+Furthermore, *fiction* provides [formal verification](http://www.informatik.uni-bremen.de/agra/doc/konf/2020_DAC_Verification_for_Field-coupled_Nanocomputing_Circuits.pdf)
+([PDF](http://www.informatik.uni-bremen.de/agra/doc/konf/2020_DAC_Verification_for_Field-coupled_Nanocomputing_Circuits.pdf))
+and utility functions. See the [CLI functionality](#Using-the-command-line-interface-(CLI)) for more details.
 
 ### Supported technologies
 
@@ -155,21 +164,24 @@ Learn more about [benchmarking and scripting](#benchmarking-and-scripting).
 
 ### Logic synthesis
 
-*fiction* focuses on physical design, i.e. placement, routing, and timing, of circuits and takes logic synthesis for granted. As
+*fiction* focuses on physical design, i.e., placement, routing, and timing, of circuits and takes logic synthesis for granted. As
 described [later](#preface), the tool [ABC](https://github.com/berkeley-abc/abc) for example could be used to generate synthesized
 logic networks which can be passed to *fiction* as circuit specifications.
 
-However, *fiction* makes use of the logic network library [mockturtle](https://github.com/lsils/mockturtle) by Mathias Soeken which
+However, *fiction* makes use of the logic network library [mockturtle](https://github.com/lsils/mockturtle) by Mathias Soeken, which
 comes with various logic synthesis and optimization algorithms. The reader may feel free to make use of them prior to physical
 design in order to obtain optimized layouts.
 
 The `mockturtle` library is also used to provide functionality for generating networks from truth tables as well as random networks. 
 See the section about [logic networks](#circuit-specifications-in-terms-of-logic-networks) for more information about network
 generation and manipulation.
 
+The [one-pass synthesis algorithm](#sat-based-one-pass-synthesis) can be utilized for combined logic synthesis and
+physical design from truth table or logic network specifications.
+
 ## Building process
 
-*For building within a Docker container, see section [Docker](#docker).*
+*For building within a Docker container, see the [Docker directions](#docker).*
 
 Git, g++, cmake and the Boost libraries are necessary in order to build *fiction*. Since a Python interpreter and
 GNU readline are utilized by some dependencies, it is also recommended to set them up.
@@ -196,7 +208,7 @@ Afterwards, *fiction* is ready to be built.
 Use this command to install all necessary libraries.
 
 ```sh
-sudo apt-get install git g++ cmake libboost-all-dev python libreadline-dev
+sudo apt-get install git g++ cmake libboost-all-dev graphviz python3 python3-dev libreadline-dev
 ```
 
 Note that there is no guarantee that a system does not lack some required packages which are not listed here!
@@ -216,6 +228,23 @@ One have the choice to change the `cmake` call to `cmake -DCMAKE_BUILD_TYPE=Debu
 information is preferred. The build mode can also be toggled via the `ccmake` CLI. Note that building with
 debug information will have a significant negative impact on *fiction*'s runtime!
 
+
+The [one-pass synthesis algorithm](#sat-based-one-pass-synthesis) is embedded via the Python3 script
+[Mugen](https://github.com/whaaswijk/mugen) by Winston Haaswijk using [pybind11](https://github.com/pybind/pybind11).
+It has some further Python dependencies that can be installed via `pip`:
+
+```sh
+pip3 install python-sat wrapt_timeout_decorator graphviz
+```
+
+The Python3 integration may cause issues on some systems. In case, you want to utilize Mugen, make sure to follow the
+setup thoroughly. Note that Mugen requires at least Python 3.7! Mugen can be disabled via toggling the `ENABLE_MUGEN`
+flag, e.g., calling
+
+```sh
+cmake -DENABLE_MUGEN=OFF ..
+```
+
 ### Docker
 
 [Docker](https://www.docker.com/) can be used to build an image to run *fiction* or to use it for development
@@ -497,7 +526,7 @@ The most important ones are
 - Route all I/Os to the layout's borders (`-b`)
 - Allow for de-synchronized circuits (`-d`)
 - Allow artificial clock latches (`-l`)
-- Enable parallelism (`-a ...` / `-A`)
+- Enable parallelism (`-a ...` / `--async_max`)
 
 See `exact -h` for a full list.
 
@@ -524,6 +553,20 @@ This scalable approach only works on logic networks which are AOIGs (MAJ gates d
 [2DDWave](https://ieeexplore.ieee.org/document/1717097) and the algorithm can only be slightly parameterized
 (see `ortho -h`). The recommended setting is `ortho -b`.
 
+#### SAT-based one-pass synthesis (`onepass`)
+
+The idea of the one-pass synthesis is to combine logic synthesis and physical design into a single run and, thereby,
+obtain even smaller layouts than possible with the SMT-based exact placement & routing approach. The backend of this
+algorithm was developed by Winston Haaswijk as the Python3 library [Mugen](https://github.com/whaaswijk/mugen).
+It utilizes the SAT solver [Glucose](https://www.labri.fr/perso/lsimon/glucose/) to solve instances of said combined
+physical design problem. Given a clocking scheme and a set of gate types to use, this algorithm finds the true minimum
+FCN circuit implementation of some specification under the provided parameters. For more information, see
+[the paper](http://www.informatik.uni-bremen.de/agra/doc/konf/ASP-DAC2021_One-pass_Synthesis_for_Field-coupled_Nanocomputing_Technologies.pdf)
+([PDF](http://www.informatik.uni-bremen.de/agra/doc/konf/ASP-DAC2021_One-pass_Synthesis_for_Field-coupled_Nanocomputing_Technologies.pdf))
+
+The possible parameters are similar to the ones used for `exact`. See `onepass -h` for a full list. 
+
+
 ### Design rule checking (`check`)
 
 Physical integrity of designed circuits can be verified using command `check`. It triggers a design rule checker which

libs/.dcignore

@@ -0,0 +1,2 @@
+* 
+**

libs/mugen/README.md

@@ -0,0 +1,9 @@
+[![Documentation Status](https://readthedocs.org/projects/mugen/badge/?version=latest)](http://mugen.readthedocs.io/en/latest/?badge=latest)
+
+# Mugen
+
+Mugen is a Python library for gate-level SAT-based physical synthesis
+of [Field-coupled Nanocomputing
+(FCN)](https://www.springer.com/de/book/9783662437216) devices.
+
+[Read the full documentation.](https://mugen.readthedocs.io/en/latest/?badge=latest)

libs/mugen/glucose-syrup-4.1/Changelog

@@ -0,0 +1,30 @@
+Version 4.1
+ - Adaptative (activated by default) strategies. See SAT 2016 paper.
+
+Version 4.0
+ - Add a Multithread version, called syrup (many glucose ;-)
+   See SAT14 paper: Lazy Clause Exchange Policy for parallel SAT solvers.
+
+ - Can work indepentently in sequential or with many cores
+
+Version 3.0 (2013)
+ - Add incremental features. 
+    See SAT13 paper: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
+
+ - Add certified UNSAT proof.
+
+Version 2.3 (2012)
+ - Add new restart strategy 
+    See CP12 paper: Refining Restarts Strategies For SAT and UNSAT
+
+ - Add additionnal features to speed the search
+
+Version 2.0 (2011) 
+ - Add additionnal features (freeze potential good clauses for one turn)
+
+ - Based on Minisat 2.2
+
+Version 1.0 (2009)
+ - Based on Minisat 2.0
+    First release of glucose.
+    See ijcai 2009 paper: Predicting Learnt Clauses Quality in Modern SAT Solver

libs/mugen/glucose-syrup-4.1/LICENCE

@@ -0,0 +1,47 @@
+ Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                LRI  - Univ. Paris Sud, France (2009-2013)
+                                Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it 
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, 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 and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of 
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
+
+
+--------------- Original Minisat Copyrights
+
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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.
+