SMT-based Exact Physical Design

Header: fiction/algorithms/physical_design/exact.hpp

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.

template<typename Lyt>
struct exact_physical_design_params

Parameters for the exact physical design algorithm.

Template Parameters:

Lyt – Gate-level layout type to create.

Public Members

std::shared_ptr<clocking_scheme<typename Lyt::tile>> scheme = std::make_shared<clocking_scheme<typename Lyt::tile>>(twoddwave_clocking<Lyt>())

Clocking scheme to be used.

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 an x-dimension 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

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

bool minimize_crossings = false

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

unsigned timeout = 4294967u

Sets a timeout in ms for the solving process. Standard is 4294967 seconds as defined by Z3.

technology_constraints technology_specifics = technology_constraints::NONE

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

surface_black_list<Lyt, port_direction> black_list = {}

Maps tiles to blacklisted gate types via their truth tables and port information.

struct exact_physical_design_stats

Statistics.

template<typename Lyt, typename Ntk>
std::optional<Lyt> fiction::exact(const Ntk &ntk, const exact_physical_design_params<Lyt> &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 is_gate_level_layout, 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.

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.