Merge branch 'main' into krys/symlink

tests/junit/junit_cover.sby

@@ -7,6 +7,7 @@ preunsat
 [options]
 mode cover
 depth 1
+cover_assert on
 
 pass: expect pass
 fail: expect fail

tests/statusdb/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=statusdb
+include ../make/subdir.mk

tests/statusdb/mixed.py

@@ -0,0 +1,65 @@
+import json
+import sqlite3
+import sys
+
+def get_prop_type(prop: str):
+    prop = json.loads(prop or "[]")
+    name_parts = prop[-1].split("_")
+    if name_parts[0] == "\\check":
+        # read_verilog style
+        # \check_cover_mixed_v...
+        return name_parts[1]
+    else:
+        # verific style
+        # \assert_auto_verificsva_cc...
+        return name_parts[0][1:]
+
+def main():
+    workdir = sys.argv[1]
+    with open(f"{workdir}/status.path", "r") as status_path_file:
+        status_path = f"{workdir}/{status_path_file.read().rstrip()}"
+    # read only database
+    con = sqlite3.connect(f"file:{status_path}?mode=ro", uri=True)
+    db = con.cursor()
+    # custom sql to get all task property statuses for the current workdir
+    rows = db.execute(
+        """
+            SELECT task.id, task_property.id, task_property.name, task_property.src, task_property_status.status
+            FROM task
+            LEFT JOIN task_property ON task_property.task=task.id
+            LEFT JOIN task_property_status ON task_property_status.task_property=task_property.id
+            WHERE task.workdir=:workdir
+            ORDER BY task_property_status.id DESC;
+        """,
+        {"workdir": workdir}
+    ).fetchall()
+    # only check the most recent iteration of the test
+    last_id = 0
+    for row_id, _, _, _, _ in rows:
+        if row_id > last_id:
+            last_id = row_id
+    # only check the last status of a property
+    checked_props = set()
+    for row_id, prop_id, prop, src, status in rows:
+        if row_id != last_id:
+            continue
+        if prop_id in checked_props:
+            continue
+        checked_props.add(prop_id)
+        prop_type = get_prop_type(prop)
+        valid_status: list[None|str] = []
+        if workdir in ["mixed_bmc", "mixed_assert"] and prop_type == "assert":
+            valid_status = ["FAIL"]
+        elif workdir == "mixed_bmc" and prop_type == "cover":
+            valid_status = [None, "UNKNOWN"]
+        elif workdir == "mixed_assert" and prop_type == "cover":
+            valid_status = ["PASS", None, "UNKNOWN"]
+        elif workdir == "mixed_no_assert" and prop_type == "assert":
+            valid_status = [None, "UNKNOWN"]
+        elif workdir == "mixed_no_assert" and prop_type == "cover":
+            valid_status = ["PASS"]
+        assert status in valid_status, f"Unexpected {prop_type} status {status} for {prop} ({src})"
+        
+
+if __name__ == "__main__":
+    main()

tests/statusdb/mixed.sby

@@ -0,0 +1,24 @@
+[tasks]
+no_assert cover
+assert cover
+bmc
+
+[options]
+cover: mode cover
+bmc: mode bmc
+bmc: depth 1
+
+assert: cover_assert on
+no_assert: expect pass
+~no_assert: expect fail
+
+[engines]
+cover: smtbmc boolector
+bmc: smtbmc boolector
+
+[script]
+read -formal mixed.v
+prep -top test
+
+[files]
+mixed.v

tests/statusdb/mixed.sh

@@ -0,0 +1,4 @@
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 ${SBY_FILE%.sby}.py $WORKDIR

tests/statusdb/mixed.v

@@ -0,0 +1,16 @@
+module test (input CP, CN, input A, B, output reg XP, XN);
+	reg [7:0] counter = 0;
+	always @* begin
+		assume (A || B);
+		assume (!A || !B);
+		assert (A == B);
+		cover (counter == 3 && A);
+		cover (counter == 3 && B);
+	end
+	always @(posedge CP)
+		counter <= counter + 1;
+	always @(posedge CP)
+		XP <= A;
+	always @(negedge CN)
+		XN <= B;
+endmodule

tests/statusdb/reset.sby

@@ -0,0 +1,14 @@
+[options]
+mode bmc
+depth 100
+expect fail
+
+[engines]
+smtbmc --keep-going boolector
+
+[script]
+read -formal reset.sv
+prep -top demo
+
+[files]
+reset.sv

tests/statusdb/reset.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+set -e
+
+# run task
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+# task has 3 properties
+python3 $SBY_MAIN -f $SBY_FILE --status | wc -l | grep -q '3'
+# resetting task should work
+python3 $SBY_MAIN -f $SBY_FILE --statusreset
+# clean database should have no properties
+python3 $SBY_MAIN -f $SBY_FILE --status | wc -l | grep -q '0'

tests/statusdb/reset.sv

@@ -0,0 +1,21 @@
+module demo (
+  input clk,
+  output reg [5:0] counter
+);
+  initial counter = 0;
+
+  always @(posedge clk) begin
+    if (counter == 15)
+      counter <= 0;
+    else
+      counter <= counter + 1;
+  end
+
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (1);
+    assert (counter < 7);
+    assert (0);
+  end
+`endif
+endmodule

tests/statusdb/timeout.sby

@@ -0,0 +1,130 @@
+[tasks]
+btor_bmc: btor bmc
+btor_fin_bmc: btor bmc fin
+pono_bmc: pono bmc
+pono_fin_bmc: pono bmc fin
+btor_cover: btor cover
+btor_fin_cover: btor cover fin
+smt_bmc: smt bmc
+smt_fin_bmc: smt bmc fin
+smt_cover: smt cover
+smt_fin_cover: smt cover fin
+smt_prove: smt prove
+smt_fin_prove: smt prove fin
+smt_fail: smtfail bmc fail
+smt_fin_fail: smtfail bmc fail fin
+aig_bmc: aigbmc bmc
+aig_fin_bmc: aigbmc bmc fin
+aig_prove: aiger prove
+aig_fin_prove: aiger prove fin
+abc_bmc: abcbmc bmc
+abc_fin_bmc: abcbmc bmc fin
+abc_prove: abc prove
+abc_fin_prove: abc prove fin
+abc_fail: abcfail prove fail
+abc_fin_fail: abcfail prove fail fin
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode prove
+fin:
+expect PASS,FAIL,UNKNOWN
+depth 10
+--
+~fin:
+expect TIMEOUT
+depth 40000
+timeout 1
+--
+
+[engines]
+btor: btor btormc
+pono: btor pono
+smt: smtbmc bitwuzla
+smtfail: smtbmc --keep-going bitwuzla
+aigbmc: aiger aigbmc
+aiger: aiger suprove
+abcbmc: abc bmc3
+abc: abc pdr
+abcfail: abc --keep-going pdr
+
+[script]
+fin: read -define WIDTH=4
+~fin: read -define WIDTH=8
+fail: read -define FAIL=1
+read -sv timeout.sv
+prep -top top
+
+[file timeout.sv]
+module top #(
+    parameter WIDTH = `WIDTH
+) (
+    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 (1); // trivial
+    `ifdef FAIL
+        assert (0);
+    `endif
+        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);
+        cover (0); // unreachable
+    end
+endmodule

tests/statusdb/timeout.sh

@@ -0,0 +1,22 @@
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+
+STATUS_CSV=${WORKDIR}/status.csv
+python3 $SBY_MAIN -f $SBY_FILE $TASK --statuscsv --latest | tee $STATUS_CSV
+
+if [[ $TASK =~ "_cover" ]]; then
+    wc -l $STATUS_CSV | grep -q '6'
+    grep "COVER" $STATUS_CSV | wc -l | grep -q '5'
+elif [[ $TASK =~ "_fail" ]]; then
+    wc -l $STATUS_CSV | grep -q '6'
+    grep "ASSERT" $STATUS_CSV | wc -l | grep -q '5'
+    grep "FAIL" $STATUS_CSV | wc -l | grep -q '1'
+else
+    wc -l $STATUS_CSV | grep -q '5'
+    grep "ASSERT" $STATUS_CSV | wc -l | grep -q '4'
+fi
+
+if [[ $TASK == "smt_cover" ]]; then
+    grep "PASS" $STATUS_CSV | wc -l | grep -q '4'
+fi

tests/unsorted/mixed.sby

@@ -8,6 +8,9 @@ cover: mode cover
 bmc: mode bmc
 bmc: depth 1
 
+cover: expect pass
+~cover: expect fail
+
 [engines]
 cover: btor btormc
 btormc: btor btormc

tests/unsorted/mixed.v

@@ -3,7 +3,7 @@ module test (input CP, CN, input A, B, output reg XP, XN);
 	always @* begin
 		assume (A || B);
 		assume (!A || !B);
-		assert (A != B);
+		assert (A == B);
 		cover (counter == 3 && A);
 		cover (counter == 3 && B);
 	end