mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 08:28:16 +00:00
Code Activity

Update documentation

Browse source
This commit is contained in:
Clifford Wolf 2017-02-19 22:55:39 +01:00
parent afeab48894
commit 404f8de16d
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
docs/examples/quickstart/memory.sby
View file

@ -4,7 +4,7 @@ depth 10
expect fail expect fail
[engines] [engines]
smtbmc -s boolector smtbmc boolector
[script] [script]
read_verilog -formal memory.v read_verilog -formal memory.v

8
docs/source/quickstart.rst
View file

@ -102,15 +102,15 @@ proof. This engine uses the array-theories provided by those solvers to
efficiently model memories. Since this example uses large memories, the efficiently model memories. Since this example uses large memories, the
``smtbmc`` engine is a good match. ``smtbmc`` engine is a good match.
(``smtbmc -s boolector`` uses boolector as SMT solver. Note that boolector is (``smtbmc boolector`` uses boolector as SMT solver. Note that boolector is
only free-to-use for noncommercial purposes. Use ``smtbmc -s z3`` to use the only free-to-use for noncommercial purposes. Use ``smtbmc z3`` to use the
permissively licensed solver Z3 instead. Z3 is the default solver when no permissively licensed solver Z3 instead. Z3 is the default solver when no
``-s`` option is used with ``smtbmc``.) argument is used with ``smtbmc``.)
Exercise: The engine ``abc bmc3`` does not provide abstract memory models. Exercise: The engine ``abc bmc3`` does not provide abstract memory models.
Therefore SymbiYosys has to synthesize the memories in the example to FFs Therefore SymbiYosys has to synthesize the memories in the example to FFs
and address logic. How does the performance of this project change if and address logic. How does the performance of this project change if
``abc bmc3`` is used as engine instead of ``smtbmc -s boolector``? How fast ``abc bmc3`` is used as engine instead of ``smtbmc boolector``? How fast
can either engine verify the design when the bug has been fixed? can either engine verify the design when the bug has been fixed?
Beyond bounded model checks Beyond bounded model checks