From 7a77c8b2cf52c7f6ecabfeedb704fc34057e24a5 Mon Sep 17 00:00:00 2001 From: panhongyang Date: Sun, 5 Feb 2023 18:43:14 +0800 Subject: [PATCH] documentation --- docs/examples.rst | 128 +++++++++++++++++----------------------------- 1 file changed, 46 insertions(+), 82 deletions(-) diff --git a/docs/examples.rst b/docs/examples.rst index 00f1153..8dd689c 100644 --- a/docs/examples.rst +++ b/docs/examples.rst @@ -1,92 +1,56 @@ 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 ---------------------------------- 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; -.. spec.verbosity = 0; + read_aiger ~/phyLS/benchmarks/adder.aig + ps -a + resub // any synthesis commands + ps -a + read_genlib ~/phyLS/src/mcnc.genlib + techmap -.. 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 - -.. 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 +Output: +:: + $ AIG i/o = 256/129 gates = 1020 level = 255 + $ ntk i/o = 256/129 gates = 893 level = 256 + [CPU time] 0.09 s + $ Mapped AIG into #gates = 701 area = 1849.00 delay = 204.90