From: Clifford Wolf Date: Sun, 19 Feb 2017 21:55:39 +0000 (+0100) Subject: Update documentation X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=404f8de16d94a0c8eff59696f0739c689d6bac7e;p=SymbiYosys.git Update documentation --- diff --git a/docs/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby index 055d8da..066c023 100644 --- a/docs/examples/quickstart/memory.sby +++ b/docs/examples/quickstart/memory.sby @@ -4,7 +4,7 @@ depth 10 expect fail [engines] -smtbmc -s boolector +smtbmc boolector [script] read_verilog -formal memory.v diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index cec67d7..c7c7232 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -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 ``smtbmc`` engine is a good match. -(``smtbmc -s boolector`` uses boolector as SMT solver. Note that boolector is -only free-to-use for noncommercial purposes. Use ``smtbmc -s z3`` to use the +(``smtbmc boolector`` uses boolector as SMT solver. Note that boolector is +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 -``-s`` option is used with ``smtbmc``.) +argument is used with ``smtbmc``.) Exercise: The engine ``abc bmc3`` does not provide abstract memory models. Therefore SymbiYosys has to synthesize the memories in the example to FFs 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? Beyond bounded model checks