diff --git a/tests/statusdb/reset.sby b/tests/statusdb/reset.sby new file mode 100644 index 0000000..aaf03c4 --- /dev/null +++ b/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 diff --git a/tests/statusdb/reset.sh b/tests/statusdb/reset.sh new file mode 100644 index 0000000..3030056 --- /dev/null +++ b/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' diff --git a/tests/statusdb/reset.sv b/tests/statusdb/reset.sv new file mode 100644 index 0000000..4514a9d --- /dev/null +++ b/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