Test autotune

diff --git a/tests/autotune/Makefile b/tests/autotune/Makefile
new file mode 100644 (file)
index 0000000..44a02a7
--- /dev/null
+++ b/tests/autotune/Makefile
@@ -0,0 +1,2 @@
+SUBDIR=autotune
+include ../make/subdir.mk

diff --git a/tests/autotune/autotune_div.sby b/tests/autotune/autotune_div.sby
new file mode 100644 (file)
index 0000000..863e160
--- /dev/null
+++ b/tests/autotune/autotune_div.sby
@@ -0,0 +1,85 @@
+[tasks]
+bmc
+cover
+prove
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode prove
+expect pass
+
+[engines]
+smtbmc boolector
+
+[script]
+read -sv autotune_div.sv
+prep -top top
+
+[file autotune_div.sv]
+module top #(
+    parameter WIDTH = 4 // Reduce this if it takes too long on CI
+) (
+    input clk,
+    input load,
+    input [WIDTH-1:0] a,
+    input [WIDTH-1:0] b,
+    output reg [WIDTH-1:0] q,
+    output reg [WIDTH-1:0] r,
+    output reg done
+);
+
+    reg [WIDTH-1:0] a_reg = 0;
+    reg [WIDTH-1:0] b_reg = 1;
+
+    initial begin
+        q <= 0;
+        r <= 0;
+        done <= 1;
+    end
+
+    reg [WIDTH-1:0] q_step = 1;
+    reg [WIDTH-1:0] r_step = 1;
+
+    // This is not how you design a good divider circuit!
+    always @(posedge clk) begin
+        if (load) begin
+            a_reg <= a;
+            b_reg <= b;
+            q <= 0;
+            r <= a;
+            q_step <= 1;
+            r_step <= b;
+            done <= b == 0;
+        end else begin
+            if (r_step <= r) begin
+                q <= q + q_step;
+                r <= r - r_step;
+
+                if (!r_step[WIDTH-1]) begin
+                    r_step <= r_step << 1;
+                    q_step <= q_step << 1;
+                end
+            end else begin
+                if (!q_step[0]) begin
+                    r_step <= r_step >> 1;
+                    q_step <= q_step >> 1;
+                end else begin
+                    done <= 1;
+                end
+            end
+        end
+    end
+
+    always @(posedge clk) begin
+        assert (r_step == b_reg * q_step); // Helper invariant
+
+        assert (q * b_reg + r == a_reg); // Main invariant & correct output relationship
+        if (done) assert (r <= b_reg - 1); // Output range
+
+        cover (done);
+        cover (done && b_reg == 0);
+        cover (r != a_reg);
+        cover (r == a_reg);
+    end
+endmodule

diff --git a/tests/autotune/autotune_div.sh b/tests/autotune/autotune_div.sh
new file mode 100644 (file)
index 0000000..e22aa5d
--- /dev/null
+++ b/tests/autotune/autotune_div.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+set -e
+python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK

diff --git a/tests/autotune/autotune_options.sby b/tests/autotune/autotune_options.sby
new file mode 100644 (file)
index 0000000..daacb3f
--- /dev/null
+++ b/tests/autotune/autotune_options.sby
@@ -0,0 +1,50 @@
+[tasks]
+a
+b
+c
+d
+
+[options]
+mode bmc
+expect fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read -sv autotune_div.sv
+prep -top top
+
+[autotune]
+a: timeout 60
+a: wait 10%+20
+a: parallel 1
+a: presat on
+a: incr on
+a: mem on
+a: forall on
+
+b: timeout none
+b: parallel auto
+b: presat off
+b: incr off
+b: mem auto
+b: mem_threshold 20
+b: forall any
+
+c: presat any
+c: incr any
+c: mem any
+c: forall auto
+
+d: incr auto
+d: incr_threshold 10
+
+[file autotune_div.sv]
+module top (input clk);
+    reg [7:0] counter = 0;
+    always @(posedge clk) begin
+        counter <= counter + 1;
+        assert (counter != 4);
+    end
+endmodule

diff --git a/tests/autotune/autotune_options.sh b/tests/autotune/autotune_options.sh
new file mode 100644 (file)
index 0000000..e22aa5d
--- /dev/null
+++ b/tests/autotune/autotune_options.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+set -e
+python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK