diff --git a/docs/examples.rst b/docs/examples.rst index f71505c..00f1153 100644 --- a/docs/examples.rst +++ b/docs/examples.rst @@ -1,94 +1,92 @@ Examples ============ -Synthesis of an optimum full adder +Synthesis of EPFL benchmarks ---------------------------------- -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. +In the following example, we show how `phyLS` can be used to synthesize a EPFL benchamrk. -.. code-black:: c++ +.. .. code-black:: c++ - spec spec; - spec.verbosity = 0; +.. spec spec; +.. spec.verbosity = 0; - chain c; +.. chain c; - dynamic_truth_table x( 3 ), y( 3 ), z( 3 ); +.. dynamic_truth_table x( 3 ), y( 3 ), z( 3 ); - create_nth_var( x, 0 ); - create_nth_var( y, 1 ); - create_nth_var( z, 2 ); +.. 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; +.. // 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 ); +.. // Call the synthesizer with the specification we've constructed. +.. auto const result = synthesize( spec, c ); - // Ensure that synthesis was successful. - assert( result == success ); +.. // 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 ); +.. // 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. +.. 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. +.. 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: +.. 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++ +.. .. code-black:: c++ - percy::SolverType solver_type = percy::SLV_BSAT2; - percy::EncoderType encoder_type = percy::ENC_FENCE; - percy::SynthMethod synth_method = percy::SYNTH_FENCE; +.. 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 ); +.. 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 ----------------------------------- +.. 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. +.. 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++ +.. .. code-black:: c++ - #include +.. #include - for ( auto i = 1u; i < 8; ++i ) - { - const auto dags = percy::pd_generate( i ); - std::cout << i << ' ' << dags.size() << std::endl; - } +.. 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 +.. .. [1] https://github.com/berkeley-abc/abc