SMT-based Exact Physical Design

Utilizes the SMT solver Z3 to generate minimal FCN gate-level layouts from logic network specifications under constraints. This approach finds exact results but has a large runtime overhead.

Header: fiction/physical_design/exact.hpp

struct exact_physical_design_params

Parameters for the exact physical design algorithm.

Public Members

std::string scheme = "2DDWave"

Clocking scheme to be used.

std::optional<layouts::arrangement> layout_arrangement = std::nullopt

Arrangement of the shifted rows or columns of the created layout. Shifted Cartesian and hexagonal layouts require it, Cartesian layouts ignore it.

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

Number of total tiles to use as an upper bound.

Note

If upper_bound_area and (either) upper_bound_x or upper_bound_y are set, the imposed search space restrictions are cumulative. E.g., if upper_bound_area == 20 and upper_bound_x == 4, all aspect ratios with a width of more than 4 and a total area of more than 20 will be skipped.

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

Exclusively investigate aspect ratios that conform with the restrictions imposed by the upper bound options. E.g., if fixed_size == true and upper_bound_area == 20, only aspect ratios with exactly 20 tiles will be examined. Restricted imposed by the upper_bound_x and upper_bound_y flags additionally apply.

std::size_t num_threads = 1ul

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

Note

This is an unstable beta feature.

bool crossings = false

Flag to indicate that crossings may be used.

bool io_pins = true

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

bool border_io = false

Flag to indicate that I/Os should be placed at the layout’s border.

bool synchronization_elements = false

Flag to indicate that artificial clock latch delays should be used to balance paths (runtime expensive!).

bool straight_inverters = false

Flag to indicate that straight inverters should be used over bend ones.

bool desynchronize = false

Flag to indicate that a discrepancy in fan-in path lengths is allowed (reduces runtime!).

bool minimize_wires = false

Minimize the number of wire tiles.

bool minimize_crossings = false

Flag to indicate that the number of used crossing tiles should be minimized.

unsigned timeout = 4294967u

Timeout budget for the solving process, in milliseconds.

technology_constraints technology_specifics = technology_constraints::NONE

Technology-specific constraints that are only to be added for a certain target technology.

utils::progress_callback on_progress = {}

Callback that receives the number of examined aspect ratios.

utils::worker_progress_callback on_worker_progress = {}

Reports logical worker activity with a fixed worker count for each invocation.

struct exact_physical_design_stats

Statistics.

Public Members

uint64_t num_gates = {0ull}

Number of logic gates, excluding primary inputs and outputs.

uint64_t num_wires = {0ull}

Number of physical wires, excluding primary inputs and outputs.

uint64_t num_crossings = {0ull}

Number of crossing-layer wires above occupied ground-layer tiles.

template<typename Lyt, typename Ntk>
std::optional<Lyt> fiction::physical_design::exact(const Ntk &ntk, const exact_physical_design_params &ps = {}, exact_physical_design_stats *pst = nullptr)

An exact placement & routing approach using SMT solving as originally proposed in “An Exact Method for Design Exploration of Quantum-dot Cellular Automata” by M. Walter, R. Wille, D. Große, F. Sill Torres, and R. Drechsler in DATE 2018. A more extensive description can be found in “Design Automation for Field-coupled Nanotechnologies” by M. Walter, R. Wille, F. Sill Torres, and R. Drechsler published by Springer Nature in 2022.

Via incremental SMT calls, an optimal gate-level layout for a given logic network will be found under constraints. Starting with \(n\) tiles, where \(n\) is the number of logic network nodes, each possible layout aspect ratio will be examined by factorization and tested for routability with the SMT solver Z3. When no upper bound is given, this approach will run until it finds a solution to the placement & routing problem instance.

Note that there a combinations of constraints for which no valid solution under the given parameters exist for the given logic network. Such combinations cannot be detected automatically. It is, thus, recommended to always set a timeout. Recommended settings include the use of I/O pins located at the layout borders for better integration. Most networks are not realizable without crossings enabled. Specifying a regular clocking scheme SIGNIFICANTLY speeds up the process. 2DDWave allows for the strictest constraints and, thereby, finds a solution the quickest. However, for high input degree networks, no valid solution exists when border I/Os are to be used unless global synchronization is disabled. Generally, solutions are found the fastest with the following settings: Crossings enabled, de-synchronization enabled, and 2DDWave clocking given. Multi-threading can sometimes speed up the process, especially for large networks. Note that the more threads are being used, the less information can be shared across the individual solver runs which destroys the benefits of incremental solving and thereby, comparatively, slows down each run.

The SMT instance works with a single layer of variables even though it is possible to allow crossings in the solution. The reduced number of variables saves a considerable amount of runtime. That’s why layout.foreach_ground_tile() is used even though the model will be mapped to a 3-dimensional layout afterwards. Generally, the algorithm incorporates quite a few encoding optimizations to be as performant as possible on various layout topologies and clocking schemes.

The approach applies to any data structures that implement the necessary functions to comply with is_network_type and concrete gate-level layouts, respectively. It is, thereby, mostly technology-independent but can make certain assumptions if needed, for instance for ToPoliNano-compliant circuits.

This approach requires the Z3 SMT solver to be installed on the system. Due to this circumstance, it is excluded from (CLI) compilation by default. To enable it, pass -DFICTION_Z3=ON to the cmake call.

May throw a high_degree_fanin_exception if ntk contains any node with a fan-in too large to be handled by the specified clocking scheme.

Template Parameters:

  • Lyt – Desired gate-level layout type.

  • Ntk – Network type that acts as specification.

Parameters:

  • ntk – The network that is to place and route.

  • ps – Parameters.

  • pst – Statistics.

Throws:

std::invalid_argument – If Lyt is a shifted Cartesian or hexagonal layout and ps.layout_arrangement is empty.

Returns:

A gate-level layout of type Lyt that implements ntk as an FCN circuit if one is found under the given parameters; std::nullopt, otherwise.

template<typename Lyt, typename Ntk>
std::optional<Lyt> fiction::physical_design::exact_with_blacklist(const Ntk &ntk, const surface_black_list<fcn::port_direction> &black_list, exact_physical_design_params ps = {}, exact_physical_design_stats *pst = nullptr)

The same as exact but with a black list of tiles that are not allowed to be used to a specified set of Boolean functions and their orientations. For example, a black list could be used to exclude the use of a tile only for an AND gate of a certain rotation, but not for other gates. This is useful if a tile is known to be faulty or if it is known to be used for a different purpose.

Template Parameters:

  • Lyt – Desired gate-level layout type.

  • Ntk – Network type that acts as specification.

Parameters:

  • ntk – The network that is to place and route.

  • black_list – The black list of tiles and their gate orientations.

  • ps – Parameters.

  • pst – Statistics.

Throws:

std::invalid_argument – If Lyt is a shifted Cartesian or hexagonal layout and ps.layout_arrangement is empty.

Returns:

A gate-level layout of type Lyt that implements ntk as an FCN circuit if one is found under the given parameters; std::nullopt, otherwise.

class exact_params

Parameters for the exact physical design algorithm.

property border_io

Flag to indicate that I/Os should be placed at the layout’s border.

property crossings

Flag to indicate that crossings may be used.

property desynchronize

Flag to indicate that a discrepancy in fan-in path lengths is allowed (reduces runtime!).

property fixed_size

Exclusively investigate aspect ratios that conform with the restrictions imposed by the upper bound options. E.g., if fixed_size == true and upper_bound_area == 20, only aspect ratios with exactly 20 tiles will be examined. Restricted imposed by the upper_bound_x and upper_bound_y flags additionally apply.

property layout_arrangement

Arrangement of the shifted rows or columns of the created layout. Shifted Cartesian and hexagonal layouts require it, Cartesian layouts ignore it.

property minimize_crossings

Flag to indicate that the number of used crossing tiles should be minimized.

property minimize_wires

Minimize the number of wire tiles.

property num_threads

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

Note

This is an unstable beta feature.

property on_progress

Callback that receives the number of examined aspect ratios.

property on_worker_progress

Reports logical worker activity with a fixed worker count for each invocation.

property scheme

Clocking scheme to be used.

property straight_inverters

Flag to indicate that straight inverters should be used over bend ones.

property synchronization_elements

(self) -> bool

property technology_specifics

Technology-specific constraints that are only to be added for a certain target technology.

property timeout

Timeout budget for the solving process, in milliseconds.

property upper_bound_area

Number of total tiles to use as an upper bound.

Note

If upper_bound_area and (either) upper_bound_x or upper_bound_y are set, the imposed search space restrictions are cumulative. E.g., if upper_bound_area == 20 and upper_bound_x == 4, all aspect ratios with a width of more than 4 and a total area of more than 20 will be skipped.

property upper_bound_x

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

property upper_bound_y

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

exact(network: technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[cartesian_gate_layout] = mnt.pyfiction.layouts.cartesian_gate_layout) → cartesian_gate_layout | None
exact(network: technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[mnt.pyfiction.layouts.shifted_cartesian_gate_layout]) → mnt.pyfiction.layouts.shifted_cartesian_gate_layout | None
exact(network: technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[hexagonal_gate_layout]) → hexagonal_gate_layout | None
exact(network: technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[cartesian_gate_layout | mnt.pyfiction.layouts.shifted_cartesian_gate_layout | hexagonal_gate_layout]) → cartesian_gate_layout | mnt.pyfiction.layouts.shifted_cartesian_gate_layout | hexagonal_gate_layout | None

Overloaded function.

  1. exact(network: mnt.pyfiction.networks.technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[mnt.pyfiction.layouts.cartesian_gate_layout] = mnt.pyfiction.layouts.cartesian_gate_layout) -> mnt.pyfiction.layouts.cartesian_gate_layout | None

An exact placement & routing approach using SMT solving as originally proposed in "An Exact Method for Design Exploration of Quantum-dot Cellular Automata" by M. Walter, R. Wille, D. Große, F. Sill Torres, and R. Drechsler in DATE 2018. A more extensive description can be found in "Design Automation for Field-coupled Nanotechnologies" by M. Walter, R. Wille, F. Sill Torres, and R. Drechsler published by Springer Nature in 2022.

Via incremental SMT calls, an optimal gate-level layout for a given logic network will be found under constraints. Starting with \(n\) tiles, where \(n\) is the number of logic network nodes, each possible layout aspect ratio will be examined by factorization and tested for routability with the SMT solver Z3. When no upper bound is given, this approach will run until it finds a solution to the placement & routing problem instance.

Note that there a combinations of constraints for which no valid solution under the given parameters exist for the given logic network. Such combinations cannot be detected automatically. It is, thus, recommended to always set a timeout. Recommended settings include the use of I/O pins located at the layout borders for better integration. Most networks are not realizable without crossings enabled. Specifying a regular clocking scheme SIGNIFICANTLY speeds up the process. 2DDWave allows for the strictest constraints and, thereby, finds a solution the quickest. However, for high input degree networks, no valid solution exists when border I/Os are to be used unless global synchronization is disabled. Generally, solutions are found the fastest with the following settings: Crossings enabled, de- synchronization enabled, and 2DDWave clocking given. Multi-threading can sometimes speed up the process, especially for large networks. Note that the more threads are being used, the less information can be shared across the individual solver runs which destroys the benefits of incremental solving and thereby, comparatively, slows down each run.

The SMT instance works with a single layer of variables even though it is possible to allow crossings in the solution. The reduced number of variables saves a considerable amount of runtime. That’s why layout.foreach_ground_tile() is used even though the model will be mapped to a 3-dimensional layout afterwards. Generally, the algorithm incorporates quite a few encoding optimizations to be as performant as possible on various layout topologies and clocking schemes.

The approach applies to any data structures that implement the necessary functions to comply with is_network_type and concrete gate-level layouts, respectively. It is, thereby, mostly technology- independent but can make certain assumptions if needed, for instance for ToPoliNano-compliant circuits.

This approach requires the Z3 SMT solver to be installed on the system. Due to this circumstance, it is excluded from (CLI) compilation by default. To enable it, pass -DFICTION_Z3=ON to the cmake call.

May throw a high_degree_fanin_exception if ntk contains any node with a fan-in too large to be handled by the specified clocking scheme.

Parameters:

  • ntk – The network that is to place and route.

  • ps – Parameters.

  • pst – Statistics.

Template Args:

  • Lyt – Desired gate-level layout type.

  • Ntk – Network type that acts as specification.

Returns:

A gate-level layout of type Lyt that implements ntk as an FCN circuit if one is found under the given parameters; std::nullopt, otherwise.

Raises:

std::invalid_argument – If Lyt is a shifted Cartesian or hexagonal layout and ps.layout_arrangement is empty.

  1. exact(network: mnt.pyfiction.networks.technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[mnt.pyfiction.layouts.shifted_cartesian_gate_layout]) -> mnt.pyfiction.layouts.shifted_cartesian_gate_layout | None

  2. exact(network: mnt.pyfiction.networks.technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[mnt.pyfiction.layouts.hexagonal_gate_layout]) -> mnt.pyfiction.layouts.hexagonal_gate_layout | None

  3. exact(network: mnt.pyfiction.networks.technology_network, parameters: exact_params = ..., statistics: exact_stats | None = None, *, layout_type: type[mnt.pyfiction.layouts.cartesian_gate_layout | mnt.pyfiction.layouts.shifted_cartesian_gate_layout | mnt.pyfiction.layouts.hexagonal_gate_layout]) -> mnt.pyfiction.layouts.cartesian_gate_layout | mnt.pyfiction.layouts.shifted_cartesian_gate_layout | mnt.pyfiction.layouts.hexagonal_gate_layout | None

Python exact and orthogonal select their output with the keyword-only layout_type class, which defaults to cartesian_gate_layout. exact also supports shifted Cartesian and hexagonal layouts; orthogonal also supports hexagonal layouts. Non-Cartesian layouts require an explicit parameters.layout_arrangement. Pass the exact registered class; subclasses are not supported.

from mnt.pyfiction.layouts import arrangement, hexagonal_gate_layout
from mnt.pyfiction.networks.io import read_network
from mnt.pyfiction.physical_design import exact, exact_params

network = read_network("network.v")
params = exact_params()
params.layout_arrangement = arrangement.EVEN_ROW
layout = exact(network, params, layout_type=hexagonal_gate_layout)