Design Rule Violations (DRVs)

Header: fiction/algorithms/verification/design_rule_violations.hpp

struct gate_level_drv_params

Parameters for design rule violation checking that specify the checks that are to be executed.

Public Members

bool unplaced_nodes = true

Check for nodes without locations.

bool placed_dead_nodes = true

Check for placed but dead nodes.

bool missing_connections = true

Check for nodes without connections.

bool crossing_gates = true

Check for wires that are crossing gates.

bool clocked_data_flow = true

Check if all node connections obey the clocking scheme data flow.

bool has_io = true

Check if the layout has I/Os.

bool empty_io = true

Check if the I/Os are assigned to empty tiles.

bool io_pins = true

Check if the I/Os are assigned to wire segments.

bool border_io = true

Check if the I/Os are located at the layout’s border.

std::ostream *out = &std::cout

Stream to write the report into.

struct gate_level_drv_stats

Public Members

nlohmann::json report = {}

Report.

std::size_t drvs = 0

Number of design rule violations.

std::size_t warnings = 0

Number of warnings.

template<typename Lyt>
void fiction::gate_level_drvs(const Lyt &lyt, const gate_level_drv_params &ps = {}, gate_level_drv_stats *pst = nullptr)

Performs design rule violation (DRV) checking on the given gate-level layout. The implementation of gate_level_layout allows for layouts with structural defects like the connection of non-adjacent tiles or connections that defy the clocking scheme. This function checks for such violations and documents them in the statistics. A brief report can be printed and more in-depth information including with error sites can be obtained from a generated json object.

Furthermore, this function does not only find and log DRVs but can also warn for instances that are not per se errors but defy best practices of layout generation, e.g., I/Os not being placed at the layout borders.

For this function to work, detail::gate_level_drvs_impl need to be declared as a friend class to the layout type that is going to be examined.

Template Parameters:

Lyt – Gate-level layout type.

Parameters:

  • lyt – The gate-level layout that is to be examined for DRVs and warnings.

  • ps – Parameters.

  • pst – Statistics.

Equivalence Checking

Header: fiction/algorithms/verification/equivalence_checking.hpp

enum class fiction::eq_type

The different equivalence types possible.

Values:

enumerator NO

Spec and Impl are logically not equivalent OR Impl has DRVs.

enumerator WEAK

Spec and Impl are logically equivalent BUT Impl has a throughput of \( \frac{1}{x} \) with \( x > 1 \).

enumerator STRONG

Spec and Impl are logically equivalent AND Impl has a throughput of \( \frac{1}{1} \).

struct equivalence_checking_stats

Public Members

eq_type eq = eq_type::NO

Stores the equivalence type.

int64_t tp_spec = 1ll

Throughput values at which weak equivalence manifests.

std::vector<bool> counter_example = {}

Stores a possible counter example.

mockturtle::stopwatch::duration runtime = {0}

Stores the runtime.

fiction::gate_level_drv_stats spec_drv_stats = {}

Stores DRVs.

template<typename Spec, typename Impl>
eq_type fiction::equivalence_checking(const Spec &spec, const Impl &impl, equivalence_checking_stats *pst = nullptr)

Performs SAT-based equivalence checking between a specification of type Spec and an implementation of type Impl. Both Spec and Impl need to be network types (that is, gate-level layouts can be utilized as well).

This implementation enables the comparison of two logic networks, a logic network and a gate-level layout or two gate-level layouts. Since gate-level layouts have a notion of timing that logic networks do not, this function does not simply prove logical equivalence but, additionally, takes timing aspects into account as well.

Thereby, three different types of equivalences arise:

  • NO equivalence: Spec and Impl are not logically equivalent or one of them is a gate-level layout that contains DRVs and, thus, cannot be checked for equivalence.

  • WEAK equivalence: Spec and Impl are logically equivalent but either one of them is a gate-level layout with TP of \( \frac{1}{x} \) with \( x > 1 \) or both of them are gate-level layouts with TP of \( \frac{1}{x} \) and \( \frac{1}{y} \), respectively, where \( x \neq y \).

  • STRONG equivalence: Spec and Impl are logically equivalent and all involved gate-level layouts have TP of \( \frac{1}{1} \).

This approach was first proposed in “Verification for Field-coupled Nanocomputing Circuits” by M. Walter, R. Wille, F. Sill Torres, D. Große, and R. Drechsler in DAC 2020.

Template Parameters:

  • Spec – Specification type.

  • Impl – Implementation type.

Parameters:

  • spec – The specification.

  • impl – The implementation.

  • pst – Statistics.

Returns:

The equivalence type of spec and impl.