Examples¶
In the following example, we show how percy can be used to synthesize an optimum full adder. While simple, the example shows some common interactions between the library’s components.
dynamic_truth_table x(3), y(3), z(3);
create_nth_var(x, 0);
create_nth_var(y, 1);
create_nth_var(z, 2);
// The sum and carry functions represent the outputs of the
// chain that we want to synthesize.
const auto sum = x ^ y ^ z;
const auto carry = ternary_majority(x, y, z);
spec[0] = sum;
spec[1] = carry;
// Call the synthesizer with the specification we've constructed.
auto result = synthesize(spec, c);
// Ensure that synthesis was successful.
assert(result == success);
// Simulate the synthesized circuit and ensure that it
// computes the correct functions.
auto sim_fs = c.simulate();
assert(sim_fs[0] == sum);
assert(sim_fs[1] == carry);
return 0;
}
In this example, we see how a synthesizer is instantiated based on a specification. The synthesizer is of the std_synthesizer type, which is the conventional synthesis engine. By default all engines use ABC’s bsat solver backend 1. Suppose that this particular combination is not suitable for our workflow. We can then easily switch to a new synthesizer and solving backend by changing one line of code:
auto synth = new_std_synth<3, Glucose::MultiSolvers*>();
In doing so we switch to a synthesis engine which synthesizes 3-input Boolean chains, with the Knuth CNF encoder, and the parallel Glucose-Syrup SAT solver backend. While we now use a completely different synthesis engine, its interface remains the same.