SAT-based One-pass Synthesis

Header: fiction/algorithms/physical_design/one_pass_synthesis.hpp

Utilizes the SAT solver Glucose to generate minimal FCN gate-level layouts from truth table specifications under constraints. To this end, it combines synthesis, placement, and routing into a single step. Since this algorithm is not restricted to any logic network structure up front, it has the opportunity to generate even smaller layouts than exact. Consequently, this algorithm does also not scale.

struct one_pass_synthesis_params

Parameters for the one-pass synthesis algorithm.

Public Members

std::string scheme = "2DDWave"

Clocking scheme to be used.

uint16_t upper_bound_x = std::numeric_limits<uint16_t>::max()

Number of tiles to use as an upper bound in x direction.

uint16_t upper_bound_y = std::numeric_limits<uint16_t>::max()

Number of tiles to use as an upper bound in y direction.

bool fixed_size = false

Investigate only aspect ratios with the number of tiles given as upper bound.

bool enable_wires = false

Enable the use of wire elements.

bool enable_not = false

Enable the use of NOT gates.

bool enable_and = false

Enable the use of AND gates.

bool enable_or = false

Enable the use of OR gates.

bool enable_maj = false

Enable the use of MAJ gates.

bool crossings = false

Flag to indicate that crossings should be used.

bool io_pins = true

Flag to indicate that I/Os should be realized by designated wire segments (preferred).

std::size_t num_threads = 1ul

Number of threads to use for exploring the possible aspect ratios.

Note

This is an unstable beta feature.

uint32_t timeout = 0u

Sets a timeout in seconds for the solving process, where 0 allows for unlimited time.

std::string name = {}

Name of the resulting network.

struct one_pass_synthesis_stats
template<typename Lyt, typename TT>
std::optional<Lyt> fiction::one_pass_synthesis(const std::vector<TT> &tts, one_pass_synthesis_params ps = {}, one_pass_synthesis_stats *pst = nullptr)

A physical design approach combining logic synthesis and physical design into a single run instead of considering them independently. To this end, SAT solving is utilized, which makes this approach an exact one but one that is independent of prior logic network synthesis. Nevertheless, it does only find solutions for small specifications because it does not scale.

The algorithm was originally proposed in “One-pass Synthesis for Field-coupled Nanocomputing Technologies” by M. Walter, W. Haaswijk, R. Wille, F. Sill Torres, and Rolf Drechsler in ASP-DAC 2021.

Using iterative SAT calls, an optimal synthesis & placement & routing for a given specification will be found. Starting with \(n\), each possible layout aspect ratio in \(n\) tiles will be examined by factorization and tested for realizability using the SAT solver glucose. When no upper bound is given, this approach will run until it finds a solution to the synthesis & placement & routing problem instance under all given constraints. Note that there are combinations of constraints for which no valid solution under the given parameters might exist. It is, thus, prudent to always provide a timeout limit.

This implementation relies on Mugen, a framework for one-pass synthesis of FCN circuit layouts developed by Winston Haaswijk. It can be found on GitHub: https://github.com/whaaswijk/mugen

Since Mugen is written in Python3, fiction uses pybind11 for interoperability. This can lead to performance and integration issues. Mugen requires the following Python3 packages to be installed:

  • graphviz

  • python-sat

  • wrapt_timeout_decorator

Due to the integration hassle, possible performance issues, and its experimental status this approach is excluded from (CLI) compilation by default. To enable it, pass -DFICTION_ENABLE_MUGEN=ON to the cmake call.

Template Parameters:

  • Lyt – Gate-level layout type to generate.

  • TT – Truth table type used as specification.

Parameters:

  • tts – A vector of truth tables where table at index i specifies the Boolean function for output i.

  • ps – Parameters.

  • pst – Statistics.

Returns:

A gate-level layout of type TT implementing tts as an FCN circuit if one is found under the given parameters; std::nullopt, otherwise.

template<typename Lyt, typename Ntk>
std::optional<Lyt> fiction::one_pass_synthesis(const Ntk &ntk, const one_pass_synthesis_params &ps = {}, one_pass_synthesis_stats *pst = nullptr)

An overload of one_pass_synthesis above that utilizes a logic network as specification instead of a vector of truth tables. It first generates truth tables from the given network and then calls the function above.

This function might throw an std::bad_alloc exception if the provided logic network has too many inputs.

Template Parameters:

  • Lyt – Gate-level layout type to generate.

  • Ntk – Logic network type used as specification.

Parameters:

  • ntk – The network whose function is to be realized as an FCN circuit.

  • ps – Parameters.

  • pst – Statistics.

Returns:

A gate-level layout of type TT implementing tts as an FCN circuit if one is found under the given parameters; std::nullopt, otherwise.