documentation
panhongyang
parent
f93d0333d5
commit
7a77c8b2cf
|
|
@ -1,92 +1,56 @@
|
||||||
Examples
|
Examples
|
||||||
============
|
============
|
||||||
|
|
||||||
|
All commands
|
||||||
|
----------------------------------
|
||||||
|
|
||||||
|
Input:
|
||||||
|
.. code-block:: bash
|
||||||
|
|
||||||
|
help
|
||||||
|
|
||||||
|
Output:
|
||||||
|
::
|
||||||
|
Verification commands:
|
||||||
|
cec exprsim sat sim
|
||||||
|
|
||||||
|
Mapping commands:
|
||||||
|
lut_mapping lutmap techmap
|
||||||
|
|
||||||
|
Synthesis commands:
|
||||||
|
balance create_graph reduction refactor
|
||||||
|
resub resyn rewrite
|
||||||
|
|
||||||
|
I/O commands:
|
||||||
|
load read_aiger read_bench read_blif
|
||||||
|
read_genlib read_verilog write_aiger write_bench
|
||||||
|
write_blif write_dot write_genlib write_verilog
|
||||||
|
|
||||||
|
General commands:
|
||||||
|
alias convert current help
|
||||||
|
print ps quit set
|
||||||
|
show store
|
||||||
|
|
||||||
|
For more details, simply add '-h' after command to see all options of this command.
|
||||||
|
|
||||||
Synthesis of EPFL benchmarks
|
Synthesis of EPFL benchmarks
|
||||||
----------------------------------
|
----------------------------------
|
||||||
|
|
||||||
In the following example, we show how `phyLS` can be used to synthesize a EPFL benchamrk.
|
In the following example, we show how `phyLS` can be used to synthesize a EPFL benchamrk.
|
||||||
|
|
||||||
.. .. code-black:: c++
|
Input:
|
||||||
|
.. code-block:: bash
|
||||||
|
|
||||||
.. spec spec;
|
read_aiger ~/phyLS/benchmarks/adder.aig
|
||||||
.. spec.verbosity = 0;
|
ps -a
|
||||||
|
resub // any synthesis commands
|
||||||
|
ps -a
|
||||||
|
read_genlib ~/phyLS/src/mcnc.genlib
|
||||||
|
techmap
|
||||||
|
|
||||||
.. chain c;
|
Output:
|
||||||
|
::
|
||||||
.. dynamic_truth_table x( 3 ), y( 3 ), z( 3 );
|
$ AIG i/o = 256/129 gates = 1020 level = 255
|
||||||
|
$ ntk i/o = 256/129 gates = 893 level = 256
|
||||||
.. create_nth_var( x, 0 );
|
[CPU time] 0.09 s
|
||||||
.. create_nth_var( y, 1 );
|
$ Mapped AIG into #gates = 701 area = 1849.00 delay = 204.90
|
||||||
.. 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
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue