mirror of
https://github.com/YosysHQ/sby.git
synced 2025-12-08 06:13:24 +00:00
Intertask cancellation via database
Task checking via database rated limited to once every 10s. Rename killer.sby to cancelledby.sby and add Makefile for testing.
This commit is contained in:
parent
e7c756a43f
commit
5fc8df43f8
4 changed files with 49 additions and 6 deletions
45
tests/intertask/cancelledby.sby
Normal file
45
tests/intertask/cancelledby.sby
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
[tasks]
|
||||
c
|
||||
b
|
||||
a
|
||||
|
||||
[cancelledby]
|
||||
a: b
|
||||
b: c
|
||||
c: a
|
||||
|
||||
[options]
|
||||
mode bmc
|
||||
depth 10000
|
||||
expect fail,cancelled
|
||||
|
||||
[engines]
|
||||
btor btormc
|
||||
|
||||
[script]
|
||||
a: read -define MAX=9600
|
||||
b: read -define MAX=1267
|
||||
c: read -define MAX=7200
|
||||
read -formal demo.sv
|
||||
prep -top demo
|
||||
|
||||
[file demo.sv]
|
||||
module demo (
|
||||
input clk,
|
||||
output reg [31:0] counter
|
||||
);
|
||||
initial counter = 0;
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (counter[31] == 1'b1)
|
||||
counter <= 0;
|
||||
else
|
||||
counter <= counter + 1;
|
||||
end
|
||||
|
||||
`ifdef FORMAL
|
||||
always @(posedge clk) begin
|
||||
assert (counter < `MAX);
|
||||
end
|
||||
`endif
|
||||
endmodule
|
||||
Loading…
Add table
Add a link
Reference in a new issue