Equivalence Checking

Header: fiction/verification/equivalence_checking.hpp

enum class fiction::verification::eq_type

Equivalence classification for logic and layout throughput.

Values:

enumerator NO

Spec and Impl differ logically, contain required topology defects, or either layout has DRVs.

enumerator WEAK

Spec and Impl are logically equivalent and have different throughput denominators.

enumerator STRONG

Spec and Impl are logically equivalent and have equal throughput denominators.

struct equivalence_checking_stats

Physical equivalence result, throughput, and diagnostics.

Public Members

eq_type eq = eq_type::NO

Stores the equivalence type.

int64_t tp_spec = 1ll

Specification throughput denominator. Defaults to 1.

int64_t tp_impl = 1ll

Implementation throughput denominator. Defaults to 1.

int64_t tp_diff = 0ll

Absolute difference between the throughput denominators. Defaults to 0.

std::vector<bool> counter_example = {}

Stores a possible counter example.

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

Stores the runtime.

fiction::verification::gate_level_drv_stats spec_drv_stats = {}

Design rule violations in the specification layout.

fiction::verification::gate_level_drv_stats impl_drv_stats = {}

Design rule violations in the implementation layout.

template<typename Spec, typename Impl>
eq_type fiction::verification::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. Each operand is a logic network or a placed gate-level layout. Layout logic is extracted before SAT checking. Interfaces match by names unique on both sides, then by remaining declared positions. Unequal interface sizes, missing required inputs, and required dependency cycles return NO.

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 and have different throughput denominators.

  • STRONG equivalence: Spec and Impl are logically equivalent and have equal throughput denominators. Logic networks have throughput denominator one.

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.

class eq_type(*values)

Equivalence classification for logic and layout throughput.

NO = 0
WEAK = 1
STRONG = 2
class equivalence_checking_stats

Physical equivalence result, throughput, and diagnostics.

property counter_example

Stores a possible counter example.

property eq

Stores the equivalence type.

property impl_drv_stats

Design rule violations in the implementation layout.

property runtime

Stores the runtime.

property spec_drv_stats

Design rule violations in the specification layout.

property tp_diff

Absolute difference between the throughput denominators. Defaults to 0.

property tp_impl

Implementation throughput denominator. Defaults to 1.

property tp_spec

Specification throughput denominator. Defaults to 1.

equivalence_checking(specification: technology_network, implementation: technology_network, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: technology_network, implementation: cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: technology_network, implementation: shifted_cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: technology_network, implementation: hexagonal_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: cartesian_gate_layout, implementation: technology_network, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: cartesian_gate_layout, implementation: cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: cartesian_gate_layout, implementation: shifted_cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: cartesian_gate_layout, implementation: hexagonal_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: shifted_cartesian_gate_layout, implementation: technology_network, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: shifted_cartesian_gate_layout, implementation: cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: shifted_cartesian_gate_layout, implementation: shifted_cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: shifted_cartesian_gate_layout, implementation: hexagonal_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: hexagonal_gate_layout, implementation: technology_network, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: hexagonal_gate_layout, implementation: cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: hexagonal_gate_layout, implementation: shifted_cartesian_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type
equivalence_checking(specification: hexagonal_gate_layout, implementation: hexagonal_gate_layout, statistics: equivalence_checking_stats | None = None) → eq_type

Performs SAT-based equivalence checking between a specification of type Spec and an implementation of type Impl. Each operand is a logic network or a placed gate-level layout. Layout logic is extracted before SAT checking. Interfaces match by names unique on both sides, then by remaining declared positions. Unequal interface sizes, missing required inputs, and required dependency cycles return NO.

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 and have different throughput denominators. - STRONG equivalence: Spec and Impl are logically equivalent and have equal throughput denominators. Logic networks have throughput denominator one.

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.

Parameters:

  • specification – The specification.

  • implementation – The implementation.

  • statistics – Statistics.

Template Args:

  • Spec – Specification type.

  • Impl – Implementation type.

Returns:

The equivalence type of specification and implementation.