mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-23 05:15:30 +00:00
handle unreached cover properties
This commit is contained in:
parent
5abaccab69
commit
53eb25fcae
4 changed files with 41 additions and 2 deletions
31
tests/cover_fail.sby
Normal file
31
tests/cover_fail.sby
Normal file
|
@ -0,0 +1,31 @@
|
|||
[options]
|
||||
mode cover
|
||||
depth 5
|
||||
expect fail
|
||||
|
||||
[engines]
|
||||
smtbmc boolector
|
||||
|
||||
[script]
|
||||
read_verilog -sv test.v
|
||||
prep -top test
|
||||
|
||||
[file test.v]
|
||||
module test(
|
||||
input clk,
|
||||
input rst,
|
||||
output reg [3:0] count
|
||||
);
|
||||
|
||||
initial assume (rst == 1'b1);
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (rst)
|
||||
count <= 4'b0;
|
||||
else
|
||||
count <= count + 1'b1;
|
||||
|
||||
cover (count == 0);
|
||||
cover (count == 4'd11);
|
||||
end
|
||||
endmodule
|
Loading…
Add table
Add a link
Reference in a new issue