Skip to content

Incremental CNF construction in circuit_validator #361

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
Jun 12, 2020
Merged

Incremental CNF construction in circuit_validator #361

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
182a27c
patch for bsat/bookmark
lee30sonia Jun 9, 2020
918dd93
first try
lee30sonia Jun 10, 2020
da2898c
only use push/pop for ODC window and non-existing circuit
lee30sonia Jun 10, 2020
ea7ad3e
debug
lee30sonia Jun 10, 2020
ff2ebf1
debug
lee30sonia Jun 10, 2020
d7dbb17
debug
lee30sonia Jun 11, 2020
28641c9
remove add_node; rename ps.max_clauses
lee30sonia Jun 11, 2020
fe5a99b
update doc
lee30sonia Jun 11, 2020
e9d8e91
port bill changes
lee30sonia Jun 12, 2020
884f843
rename variables; use initializer_list
lee30sonia Jun 12, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 14 additions & 11 deletions docs/algorithms/circuit_validator.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,10 @@ 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.
Expand Down Expand Up @@ -34,18 +38,18 @@ The following code shows how to check functional equivalence of a root node to s
}
}

circuit_validator<aig_network>::gate::fanin fi1;
fi1.idx = 0; fi1.inv = true;
circuit_validator<aig_network>::gate::fanin fi2;
fi2.idx = 1; fi2.inv = true;
circuit_validator<aig_network>::gate g;
g.fanins = {fi1, fi2};
g.type = circuit_validator<aig_network>::gate_type::AND;
circuit_validator<aig_network>::gate::fanin gi1{0, true};
circuit_validator<aig_network>::gate::fanin gi2{1, true};
circuit_validator<aig_network>::gate g{{gi1, gi2}, circuit_validator<aig_network>::gate_type::AND};

circuit_validator<aig_network>::gate::fanin hi1{2, false};
circuit_validator<aig_network>::gate::fanin hi2{0, false};
circuit_validator<aig_network>::gate h{{hi1, hi2}, circuit_validator<aig_network>::gate_type::AND};

result = v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g}, true );
result = v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g, h}, true );
if ( result && *result )
{
std::cout << "f3 is equivalent to NOT(NOT f1 AND NOT f2)\n";
std::cout << "f3 is equivalent to NOT((NOT f1 AND NOT f2) AND f1)\n";
}

**Parameters**
Expand All @@ -70,9 +74,8 @@ The following code shows how to check functional equivalence of a root node to s
.. doxygenstruct:: mockturtle::circuit_validator::gate
:members: fanins, type
.. doxygenstruct:: mockturtle::circuit_validator::gate::fanin
:members: idx, inv
:members: index, inverted

**Updating**

.. doxygenfunction:: mockturtle::circuit_validator::add_node
.. doxygenfunction:: mockturtle::circuit_validator::update
Loading