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.

C++Python

Header: fiction/algorithms/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.

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.

struct exact_physical_design_stats

Statistics.

Warning

doxygenfunction: Unable to resolve function “fiction::exact” with arguments (const Ntk&, const exact_physical_design_params<Lyt>&, exact_physical_design_stats*) in doxygen xml output for project “fiction” from directory: doxyxml/xml. Potential matches:

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

Warning

doxygenfunction: Unable to resolve function “exact_with_blacklist” with arguments “(const Ntk& ntk, const surface_black_list<Lyt, port_direction>& black_list,”. Could not parse arguments. Parsing eror is Invalid C++ declaration: Expected identifier in nested name. [error at 75] (const Ntk& ntk, const surface_black_list<Lyt, port_direction>& black_list, —————————————————————————^