Circuit Equivalent to another Circuit
Given Circuit A and Circuit B; can we show that A == B, where for all inputs given to A, the output of A matches the output of B given the same circuit.
For equality we require:
- The number of inputs of A match the number of inputs of B
- The number of outputs of A match the number of outputs of B
- The names of the wires do not matter, just the order of them
SAT Version
The SAT version compares the original circuit to the locked circuit with a key, in file ckt.cpp
-
ckt_t::ckt_t(const ckt_t& c1, const ckt_t& c2)
-
c1
the original circuit -
c2
the locked circuit - Creates the comparison SAT to see if they are equivalent
-
-
int ckt_t::count_differing_inputs(const char* keys, int MAX_CNT)
- Embeds the key into the circuit and confirms if they are equivalent by returning 0, otherwise it returns the number of inputs it was able to find that differed (up to
MAX_CNT
)
- Embeds the key into the circuit and confirms if they are equivalent by returning 0, otherwise it returns the number of inputs it was able to find that differed (up to