From 1a574ce24acdf2aa80ea03f742ccd688e97cbfff Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 29 Jan 2017 17:10:17 +0100 Subject: [PATCH] Improve documentation --- docs/examples/quickstart/.gitignore | 2 + docs/examples/quickstart/demo.sby | 13 +++++ docs/examples/quickstart/demo.v | 15 ++++++ docs/examples/quickstart/memory.sby | 13 +++++ docs/examples/quickstart/memory.v | 57 ++++++++++++++++++++ docs/source/quickstart.rst | 84 ++++++++++++++++------------- 6 files changed, 148 insertions(+), 36 deletions(-) create mode 100644 docs/examples/quickstart/.gitignore create mode 100644 docs/examples/quickstart/demo.sby create mode 100644 docs/examples/quickstart/demo.v create mode 100644 docs/examples/quickstart/memory.sby create mode 100644 docs/examples/quickstart/memory.v diff --git a/docs/examples/quickstart/.gitignore b/docs/examples/quickstart/.gitignore new file mode 100644 index 0000000..5a875a0 --- /dev/null +++ b/docs/examples/quickstart/.gitignore @@ -0,0 +1,2 @@ +demo +memory diff --git a/docs/examples/quickstart/demo.sby b/docs/examples/quickstart/demo.sby new file mode 100644 index 0000000..01fb2aa --- /dev/null +++ b/docs/examples/quickstart/demo.sby @@ -0,0 +1,13 @@ +[options] +mode bmc +depth 100 + +[engines] +smtbmc + +[script] +read_verilog -formal demo.v +prep -top demo + +[files] +demo.v diff --git a/docs/examples/quickstart/demo.v b/docs/examples/quickstart/demo.v new file mode 100644 index 0000000..09044de --- /dev/null +++ b/docs/examples/quickstart/demo.v @@ -0,0 +1,15 @@ +module demo ( + input clk, + output [5:0] counter +); + reg [5:0] counter = 0; + + always @(posedge clk) begin + if (counter == 15) + counter <= 0; + else + counter <= counter + 1; + end + + assert property (counter < 32); +endmodule diff --git a/docs/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby new file mode 100644 index 0000000..4b25060 --- /dev/null +++ b/docs/examples/quickstart/memory.sby @@ -0,0 +1,13 @@ +[options] +mode bmc +depth 10 + +[engines] +smtbmc -s boolector + +[script] +read_verilog -formal memory.v +prep -top testbench + +[files] +memory.v diff --git a/docs/examples/quickstart/memory.v b/docs/examples/quickstart/memory.v new file mode 100644 index 0000000..f633e38 --- /dev/null +++ b/docs/examples/quickstart/memory.v @@ -0,0 +1,57 @@ +module testbench ( + input clk, wen, + input [15:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + memory uut ( + .clk (clk ), + .wen (wen ), + .addr (addr ), + .wdata(wdata), + .rdata(rdata) + ); + + wire [15:0] test_addr = $anyconst; + reg test_data_valid = 0; + reg [7:0] test_data; + + always @(posedge clk) begin + if (addr == test_addr) begin + if (wen) begin + test_data <= wdata; + test_data_valid <= 1; + end + if (test_data_valid) begin + assert(test_data == rdata); + end + end + end +endmodule + +module memory ( + input clk, wen, + input [15:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + reg [7:0] bank0 [0:'h3fff]; + reg [7:0] bank1 [0:'h3fff]; + reg [7:0] bank2 [0:'h3fff]; + reg [7:0] bank3 [0:'h3fff]; + + always @(posedge clk) begin + case (addr[15:14]) + 0: if (wen) bank0[addr[13:0]] <= wdata; + 1: if (wen) bank1[addr[13:0]] <= wdata; + 2: if (wen) bank1[addr[13:0]] <= wdata; // BUG: Should assign to bank2 + 3: if (wen) bank3[addr[13:0]] <= wdata; + endcase + end + + assign rdata = + addr[15:14] == 0 ? bank0[addr[13:0]] : + addr[15:14] == 1 ? bank1[addr[13:0]] : + addr[15:14] == 2 ? bank2[addr[13:0]] : + addr[15:14] == 3 ? bank3[addr[13:0]] : 'bx; +endmodule diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 6408527..5547575 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -2,12 +2,15 @@ Getting Started =============== +The example files used in this chapter can be downloaded from `here +`_. + Installing ---------- TBD -Until I find the time to write this section this links must be sufficient: +Until I find the time to write this section this links must suffice: * Yosys: http://www.clifford.at/yosys/ * SymbiYosys: https://github.com/cliffordwolf/SymbiYosys @@ -24,24 +27,8 @@ First step: A simple BMC example Here is a simple example design with a safety property (assertion). -.. code-block:: systemverilog - - module demo ( - - input clk, - output [5:0] counter - ); - reg [5:0] counter = 0; - - always @(posedge clk) begin - if (counter == 15) - counter <= 0; - else - counter <= counter + 1; - end - - assert property (counter < 32); - endmodule +.. literalinclude:: ../examples/quickstart/demo.v + :language: systemverilog The property in this example is true. We'd like to verify this using a bounded model check (BMC) that is 100 cycles deep. @@ -49,21 +36,8 @@ model check (BMC) that is 100 cycles deep. SymbiYosys is controlled by ``.sby`` files. The following file can be used to configure SymbiYosys to run a BMC for 100 cycles on the design: -.. code-block:: text - - [options] - mode bmc - depth 100 - - [engines] - smtbmc - - [script] - read_verilog -formal demo.v - prep -top demo - - [files] - demo.v +.. literalinclude:: ../examples/quickstart/demo.sby + :language: text Simply create a text file ``demo.v`` with the example design and another text file ``demo.sby`` with the SymbiYosys configuration. Then run:: @@ -98,8 +72,46 @@ Time for a simple exercise: Modify the design so that the property is false and the offending state is reachable within 100 cycles. Re-run ``sby`` with the modified design and see if the proof now fails. -Going beyond bounded model checks ---------------------------------- +Selecting the right engine +-------------------------- + +The ``.sby`` file for a project selects one or more engines. (When multiple +engines are selected, all engines are executed in parallel and the result +returned by the first engine to finish is the result returned by SymbiYosys.) + +Each engine has its strengths and weaknesses. Therefore it is important to +select the right engine for each project. The documentation for the individual +engines can provide some guidance for engine selection. (Trial and error can +also be a useful method for engine selection.) + +Let's consider the following example: + +.. literalinclude:: ../examples/quickstart/memory.v + :language: systemverilog + +This example is expected to fail verification (see the BUG comment). +The following ``.sby`` file can be used to show this: + +.. literalinclude:: ../examples/quickstart/memory.sby + :language: text + +This project uses the ``smtbmc`` engine, which uses SMT solvers to perform the +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 +permissively licensed solver Z3 instead. Z3 is the default solver when no +``-s`` option 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``? + +Beyond bounded model checks +--------------------------- TBD -- 2.30.2