example for autotune

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