mirror of
https://github.com/YosysHQ/sby.git
synced 2025-08-18 19:02:21 +00:00
tests: Add statusdb test
Ensures that `--statusreset` doesn't break the schema.
This commit is contained in:
parent
10040ce859
commit
b1d9bcbb42
3 changed files with 46 additions and 0 deletions
14
tests/statusdb/reset.sby
Normal file
14
tests/statusdb/reset.sby
Normal file
|
@ -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
|
11
tests/statusdb/reset.sh
Normal file
11
tests/statusdb/reset.sh
Normal file
|
@ -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'
|
21
tests/statusdb/reset.sv
Normal file
21
tests/statusdb/reset.sv
Normal file
|
@ -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
|
Loading…
Add table
Add a link
Reference in a new issue