Merge branch 'YosysHQ:master' into fifo_example

docs/examples/autotune/README.md

@@ -0,0 +1,30 @@
+# Autotune demo
+
+This directory contains a simple sequential integer divider circuit. The
+verilog implementation in [divider.sv](divider.sv) comes with assertions that
+this circuit will always produce the correct result and will always finish
+within a fixed number of cycles. The circuit has the divider bit-width as
+parameter.
+
+Increasing the WIDTH parameter quickly turns proving those assertions into a
+very difficult proof for fully autmated solvers. This makes it a good example
+for the `--autotune` option which tries different backend engines to find the
+best performing engine configuration for a given verification task.
+
+The [divider.sby](divider.sby) file defines 3 tasks named `small`, `medium` and
+`large` which configure the divider with different bit-widths. To verify the
+`small` divider using the default engine run:
+
+    sby -f divider.sby small
+
+To automatically try different backend engines using autotune, run
+
+    sby --autotune -f divider.sby small
+
+The `small` task should finish quickly using both the default engine and using
+autotune. The `medium` and `large` tasks take significantly longer and show
+greater differences between engine configurations. Note that the `large` tasks
+can take many minutes to hours, depending on the machine you are using.
+
+You can learn more about Sby's autotune feature from [Sby's
+documentation](https://symbiyosys.readthedocs.io/en/latest/autotune.html).

docs/examples/autotune/divider.sby

@@ -0,0 +1,24 @@
+[tasks]
+small default
+medium
+large
+
+[options]
+mode prove
+small: depth 11
+medium: depth 15
+large: depth 19
+
+[engines]
+smtbmc
+
+[script]
+small: read -define WIDTH=8
+medium: read -define WIDTH=12
+large: read -define WIDTH=16
+
+read -formal divider.sv
+prep -top divider
+
+[files]
+divider.sv

docs/examples/autotune/divider.sv

@@ -0,0 +1,85 @@
+`ifndef WIDTH
+`define WIDTH 4
+`endif
+
+module divider #(
+    parameter WIDTH=`WIDTH
+) (
+    input wire clk,
+    input wire start,
+    input wire [WIDTH-1:0] dividend,
+    input wire [WIDTH-1:0] divisor,
+
+    output reg done,
+    output reg [WIDTH-1:0] quotient,
+    output wire [WIDTH-1:0] remainder
+);
+
+    reg [WIDTH-1:0] acc;
+
+    reg [WIDTH*2-1:0] sub;
+    reg [WIDTH-1:0] pos;
+
+    assign remainder = acc;
+
+    always @(posedge clk) begin
+        if (start) begin
+            acc <= dividend;
+            quotient <= 0;
+            sub <= divisor << (WIDTH - 1);
+            pos <= 1 << (WIDTH - 1);
+            done <= 0;
+        end else if (!done) begin
+            if (acc >= sub) begin
+                acc <= acc - sub[WIDTH-1:0];
+                quotient <= quotient + pos;
+            end
+
+            sub <= sub >> 1;
+            {pos, done} <= pos;
+        end
+    end
+
+
+`ifdef FORMAL
+    reg [WIDTH-1:0] start_dividend = 0;
+    reg [WIDTH-1:0] start_divisor = 0;
+
+    reg started = 0;
+    reg finished = 0;
+    reg [$clog2(WIDTH + 1):0] counter = 0;
+
+    always @(posedge clk) begin
+        // Bound the number of cycles until the result is ready
+        assert (counter <= WIDTH);
+
+        if (started) begin
+            if (finished || done) begin
+                finished <= 1;
+                // Make sure result stays until we start a new division
+                assert (done);
+
+                // Check the result
+                if (start_divisor == 0) begin
+                    assert (&quotient);
+                    assert (remainder == start_dividend);
+                end else begin
+                    assert (quotient == start_dividend / start_divisor);
+                    assert (remainder == start_dividend % start_divisor);
+                end
+            end else begin
+                counter <= counter + 1'b1;
+            end
+        end
+
+        // Track the requested inputs
+        if (start) begin
+            start_divisor <= divisor;
+            start_dividend <= dividend;
+            started <= 1;
+            counter <= 0;
+            finished <= 0;
+        end
+    end
+`endif
+endmodule

docs/source/autotune.rst

@@ -3,7 +3,7 @@ Autotune: Automatic Engine Selection
 
 Selecting the best performing engine for a given verification task often
 requires some amount of trial and error. To reduce the manual work required for
-this, sby offers the ``--autotune`` option which takes an ``.sby`` file and
+this, sby offers the ``--autotune`` option. This takes an ``.sby`` file and
 runs it using engines and engine configurations. At the end it produces a
 report listing the fastest engines among these candidates.
 
@@ -11,15 +11,15 @@ Using Autotune
 --------------
 
 To run autotune, you can add the ``--autotune`` option to your usual sby
-invokation. For example if you usually run ``sby demo.sby`` you would run ``sby
---autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks,
-autotune is run for each task independently. As without ``--autotune``, it is
-possible to specify which tasks to run on the command line.
+invocation. For example, if you usually run ``sby demo.sby`` you would run
+``sby --autotune demo.sby`` instead. When the ``.sby`` file contains multiple
+tasks, autotune is run for each task independently. As without ``--autotune``,
+it is possible to specify which tasks to run on the command line.
 
-Autotune runs without requiring further interaction and will eventually print a
+Autotune runs without requiring further interaction, and will eventually print a
 list of engine configurations and their respective solving times. To
-permanently use an engine configuration you can copy if from the ``sby
---autotune`` output into the ``[engines]`` section of your ``.sby`` file.
+permanently use an engine configuration you can copy it from the
+``sby --autotune`` output into the ``[engines]`` section of your ``.sby`` file.
 
 Autotune Log Output
 -------------------
@@ -37,9 +37,9 @@ once and will be reused to run every candidate engine.
    SBY [demo] base: finished (returncode=0)
    SBY [demo] prepared model 'base'
 
-This is followed by selecting the engine candidates to run. For this the design
+This is followed by selecting the engine candidates to run. The design
 and sby configuration are analyzed to skip engines that are not compatible or
-unlikely to work well. When engines is skipped due to a recommendation, a
+unlikely to work well. When an engine is skipped due to a recommendation, a
 corresponding log message is displayed as well as the total number of
 candidates to try:
 
@@ -49,7 +49,7 @@ candidates to try:
    SBY [demo] testing 16 engine configurations...
 
 After this, the candidate engine configurations are started. Depending on the
-configuration engines can run in parallel. The engine output itself is not
+configuration, engines can run in parallel. The engine output itself is not
 logged to stdout when running autotune, so you will only see messages about
 starting an engine:
 
@@ -77,7 +77,7 @@ be interspersed with other log output.
    SBY [demo] smt2: finished (returncode=0)
    SBY [demo] prepared model 'smt2'
 
-Whenever an engine finishes a log message is printed:
+Whenever an engine finishes, a log message is printed:
 
 .. code-block:: text
 
@@ -91,7 +91,7 @@ When an engine takes longer than the current hard timeout, it is stopped:
    SBY [demo] engine_2 (smtbmc bitwuzla): timeout (150 seconds)
 
 Depending on the configuration, autotune will also stop an engine earlier when
-reaching a soft timeout. In that case, when no other engine finishes in less
+reaching a soft timeout. If no other engine finishes in less
 time, the engine will be retried later with a longer soft timeout:
 
 .. code-block:: text
@@ -99,7 +99,7 @@ time, the engine will be retried later with a longer soft timeout:
    SBY [demo] engine_0 (smtbmc boolector): timeout (60 seconds, will be retried if necessary)
 
 
-Finally at the end a summary of all finished engines is printed, sorted by
+Finally, a summary of all finished engines is printed, sorted by
 their solving time:
 
 .. code-block:: text
@@ -112,8 +112,8 @@ their solving time:
 
 If any tried engine encounters an error or produces an unexpected result,
 autotune will also output a list of failed engines. Note that when the sby file
-does not contain the ``expect`` option, autotune defaults to ``expect
-pass,fail`` to simplify running autotune on a verification task with a
+does not contain the ``expect`` option, autotune defaults to
+``expect pass,fail`` to simplify running autotune on a verification task with a
 currently unknown outcome.
 
 Configuring Autotune
@@ -121,7 +121,7 @@ Configuring Autotune
 
 Autotune can be configured by adding an ``[autotune]`` section to the ``.sby``
 file. Each line in that section has the form ``option_name value``, the
-possible options and their supported values are described below. In addition
+possible options and their supported values are described below. In addition,
 the ``--autotune-config`` command line option can be used to specify a file
 containing further autotune options, using the same syntax. When both are used,
 the command line option takes precedence. This makes it easy to run autotune