Functional equivalence of circuit nodes
Header: mockturtle/algorithms/circuit_validator.hpp
This class can be used to validate potential circuit optimization choices. It checks the functional equivalence of a circuit node with an existing or non-existing signal with SAT, with optional consideration of observability don’t-care (ODC).
If more advanced SAT validation is needed, one could consider using cnf_view
instead, which also constructs the CNF clauses of circuit nodes.
Example
The following code shows how to check functional equivalence of a root node to signals existing in the network, or created with nodes within the network. If not, get the counter example.
/* derive some AIG (can be AIG, XAG, MIG, or XMG) */
aig_network aig;
auto const a = aig.create_pi();
auto const b = aig.create_pi();
auto const f1 = aig.create_and( !a, b );
auto const f2 = aig.create_and( a, !b );
auto const f3 = aig.create_or( f1, f2 );
circuit_validator v( aig );
auto result = v.validate( f1, f2 );
/* result is an optional, which is nullopt if SAT conflict limit was exceeded */
if ( result )
{
if ( *result )
{
std::cout << "f1 and f2 are functionally equivalent\n";
}
else
{
std::cout << "f1 and f2 have different values under PI assignment: ";
std::cout << v.cex[0] << v.cex[1] << "\n";
}
}
std::vector<aig_network::node> divs;
divs.emplace_back( aig.get_node( f1 ) );
divs.emplace_back( aig.get_node( f2 ) );
xag_index_list id_list;
id_list.add_inputs( 2 );
id_list.add_and( 3, 5 ); // f3 = NOT f1 AND NOT f2
id_list.add_and( 2, 6 ); // f4 = f1 AND f3
id_list.add_output( 9 ); // NOT f4
result = v.validate( f3, divs, id_list );
if ( result && *result )
{
std::cout << "f3 is equivalent to NOT(f1 AND (NOT f1 AND NOT f2))\n";
}
Parameters
-
struct validator_params
Public Members
-
uint32_t max_clauses = {1000}
Maximum number of clauses of the SAT solver. (incremental CNF construction)
-
int32_t odc_levels = {0}
Whether to consider ODC, and how many levels. 0 = No consideration. -1 = Consider TFO until PO.
-
uint32_t conflict_limit = {1000}
Conflict limit of the SAT solver.
-
uint32_t random_seed = {0}
Seed for randomized solving.
-
uint32_t max_clauses = {1000}
Validate with existing signals
-
inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, signal const &d)
Validate functional equivalence of signals
f
andd
.
-
inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, signal const &d)
Validate functional equivalence of node
root
and signald
.
-
inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, bool value)
Validate whether signal
f
is a constant ofvalue
.
-
inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, bool value)
Validate whether node
root
is a constant ofvalue
.
Validate with non-existing circuit
A not-yet-created circuit built on existing nodes in the network can be represented by an index list and a list of support nodes. The index list must be one of the classes implemented in Index list.
-
template<class index_list_type>
inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, std::vector<node> const &divs, index_list_type const &id_list, bool inverted = false) Validate functional equivalence of signal
f
with a circuit represented by an index_list.- Parameters:
id_list – The index_list representing a circuit.
divs – Existing nodes in the network, serving as PIs of
id_list
.inverted – Whether to validate equivalence or inverse equivalence.
-
template<class index_list_type>
inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, std::vector<node> const &divs, index_list_type const &id_list, bool inverted = false) Validate functional equivalence of node
root
with an index_list.
-
template<class iterator_type, class index_list_type>
inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, iterator_type divs_begin, iterator_type divs_end, index_list_type const &id_list, bool inverted = false) Validate functional equivalence of signal
f
with an index_list.
-
template<class iterator_type, class index_list_type>
inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, iterator_type divs_begin, iterator_type divs_end, index_list_type const &id_list, bool inverted = false) Validate functional equivalence of node
root
with an index_list.
Utilizing don’t-cares
-
inline void mockturtle::circuit_validator::set_odc_levels(uint32_t odc_levels)
Set ODC levels.
-
inline void mockturtle::circuit_validator::update()
Update CNF clauses.
This function should be called when the function of one or more nodes has been modified (typically when utilizing ODCs).
Generate multiple patterns
A simulation pattern is a collection of value assignments to every primary inputs.
A counter-example of a failing validation is a simulation pattern under which the nodes being validated have different simulation values.
It can be directly read from the public data member circuit_validator::cex
(which is a std::vector<bool>
of size Ntk::num_pis()
) after a call to (any type of) circuit_validator::validate
which returns false
.
If multiple different patterns are desired, one can call circuit_validator::generate_pattern
. However, this is currently only supported for constant validation.
-
template<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>>
inline std::vector<std::vector<bool>> mockturtle::circuit_validator::generate_pattern(signal const &f, bool value, std::vector<std::vector<bool>> const &block_patterns = {}, uint32_t num_patterns = 1u) Generate pattern(s) for signal
f
to bevalue
, optionally blocking several known patterns.Requires
use_pushpop = true
, which is only supported forbsat2
andz3
. Ifbsat2
is used, and if the network has more than 2048 PIs, theBUFFER_SIZE
inlib/bill/sat/interface/abc_bsat2.hpp
has to be increased to at leastntk.num_pis()
.If
block_patterns
and the returned vector are both empty,f
is validated to be a constant of!value
.- Parameters:
block_patterns – Patterns to be blocked in the solver. (Will not generate any of them.)
num_patterns – Number of patterns to be generated, if possible. (The size of the result may be smaller than this number, but never larger.)
-
template<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>>
inline std::vector<std::vector<bool>> mockturtle::circuit_validator::generate_pattern(node const &root, bool value, std::vector<std::vector<bool>> const &block_patterns = {}, uint32_t num_patterns = 1u) Generate pattern(s) for node
root
to bevalue
, optionally blocking several known patterns.