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.

        // Create the truth table specification object. It has three inputs and two outputs.
        synth_spec<static_truth_table<3>> spec(3, 2);
        spec.verbosity = 1;

        // Instantiate a new standard synthesizer.
        auto synth = new_std_synth();
        chain<2> c;

        // Create the functions to synthesize.
        // We use three static truth tables to 
        // represent the three inputs to the full adder.
        static_truth_table<3> x, y, z;

        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.functions[0] = &sum;
        spec.functions[1] = &carry;

        // Call the synthesizer with the specification we've constructed.
        auto result = synth->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(spec);
        assert(sim_fs[0] == sum);
        assert(sim_fs[1] == carry);

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.

[1]	https://github.com/berkeley-abc/abc