mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-23 05:15:30 +00:00
parent
17c3961a2b
commit
a0e3dd3d9a
6 changed files with 55 additions and 61 deletions
33
tests/regression/option_skip.sby
Normal file
33
tests/regression/option_skip.sby
Normal file
|
@ -0,0 +1,33 @@
|
|||
[tasks]
|
||||
smtbmc_pass: smtbmc pass
|
||||
smtbmc_fail: smtbmc fail
|
||||
btormc_pass: btormc pass
|
||||
btormc_fail: btormc fail
|
||||
|
||||
[options]
|
||||
mode bmc
|
||||
pass: expect pass
|
||||
fail: expect fail
|
||||
pass: depth 5
|
||||
fail: depth 6
|
||||
|
||||
skip 2
|
||||
|
||||
[engines]
|
||||
smtbmc: smtbmc boolector
|
||||
[engines bmc]
|
||||
btormc: btor btormc
|
||||
|
||||
[script]
|
||||
read -formal top.sv
|
||||
prep -top top
|
||||
|
||||
[file top.sv]
|
||||
module top(input clk);
|
||||
reg [7:0] counter = 0;
|
||||
|
||||
always @(posedge clk) begin
|
||||
counter <= counter + 1;
|
||||
assert (counter < 4);
|
||||
end
|
||||
endmodule
|
Loading…
Add table
Add a link
Reference in a new issue