93 lines
3.2 KiB
ReStructuredText
93 lines
3.2 KiB
ReStructuredText
Examples
|
|
============
|
|
|
|
Synthesis of EPFL benchmarks
|
|
----------------------------------
|
|
|
|
In the following example, we show how `phyLS` can be used to synthesize a EPFL benchamrk.
|
|
|
|
.. .. 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
|