95 lines
3.1 KiB
ReStructuredText
95 lines
3.1 KiB
ReStructuredText
Examples
|
|
============
|
|
|
|
Synthesis of an optimum full adder
|
|
----------------------------------
|
|
|
|
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.
|
|
|
|
.. code-black:: c++
|
|
|
|
spec spec;
|
|
spec.verbosity = 0;
|
|
|
|
chain c;
|
|
|
|
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.
|
|
auto const sum = x ^ y ^ z;
|
|
auto const carry = ternary_majority( x, y, z );
|
|
spec[0] = sum;
|
|
spec[1] = carry;
|
|
|
|
// Call the synthesizer with the specification we've constructed.
|
|
auto const 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 );
|
|
|
|
In this example, we synthesize a Boolean chain for a full adder
|
|
specified by the two Boolean functions `sum` and `carry`. We see how
|
|
synthesis is invoked using the `synthesize` function that takes two
|
|
parameters. The first parameter is the specification `spec`, the
|
|
second parameter `c` references a chain. If synthesis is successful,
|
|
the `synthesize` function returns `success` and stores the synthesized
|
|
chain in `c`. Last but not least, we simulate the chain to ensure
|
|
that it's output functions are equivalent to the specified functions
|
|
of the full adder.
|
|
|
|
Percy offers several different encodings and synthesis methods, and
|
|
allows its users to select from various SAT solver backends. By
|
|
default all engines use ABC's `bsat` solver backend [1]_
|
|
(`SLV_BSAT2`), the SSV encoding (`ENC_SSV`), and the standard
|
|
synthesis method (`SYNTH_STD`). Suppose that this particular
|
|
combination is not suitable for our workflow. We can then easily
|
|
customize the synthesis process by cherry-picking a solver, encoder,
|
|
and synthesis method from the available options.
|
|
|
|
The next example demonstrates fence-based synthesis using the
|
|
corresponding encoder and synthesis method together with ABC's `bsat`
|
|
as solver backend:
|
|
|
|
.. code-black:: c++
|
|
|
|
percy::SolverType solver_type = percy::SLV_BSAT2;
|
|
percy::EncoderType encoder_type = percy::ENC_FENCE;
|
|
percy::SynthMethod synth_method = percy::SYNTH_FENCE;
|
|
|
|
auto solver = get_solver( solver_type );
|
|
auto encoder = get_encoder( *solver, encoder_type );
|
|
auto const result = synthesize( spec, c, *solver, *encoder, synth_method );
|
|
|
|
Enumerate (and count) partial DAGs
|
|
----------------------------------
|
|
|
|
In the following code snippet, we use `percy` to enumerate partial
|
|
DAGs for a given number of nodes (up to 7 nodes), count them, and
|
|
print the numbers.
|
|
|
|
.. code-black:: c++
|
|
|
|
#include <percy/partial_dag.hpp>
|
|
|
|
for ( auto i = 1u; i < 8; ++i )
|
|
{
|
|
const auto dags = percy::pd_generate( i );
|
|
std::cout << i << ' ' << dags.size() << std::endl;
|
|
}
|
|
|
|
|
|
.. [1] https://github.com/berkeley-abc/abc
|