mirror of https://github.com/YosysHQ/yosys.git
32 lines
976 B
Plaintext
32 lines
976 B
Plaintext
verific -sv <<EOF
|
|
module top(input clk, input a, input b);
|
|
|
|
prop_supported1: assert property (@(posedge clk) a ##1 b |=> b);
|
|
|
|
prop_exploding: assert property (@(posedge clk)
|
|
((a [*7] ##1 b) [*11]) and
|
|
((a [*11] ##1 b) [*7]) and
|
|
((a [*13] ##1 b) [*5]) and
|
|
((a [*5] ##1 b) [*13])
|
|
);
|
|
|
|
prop_supported2: assert property (@(posedge clk) a [*5] ##1 b |=> b);
|
|
|
|
endmodule
|
|
EOF
|
|
|
|
logger -expect warning "Stopping to prevent exponential design size explosion." 1
|
|
verific -import -sva-continue-on-err top
|
|
logger -check-expected
|
|
|
|
select -assert-count 3 top/t:$assert
|
|
select -assert-count 1 top/a:unsupported_sva top/prop_exploding %% top/t:$assert %i
|
|
|
|
select -assert-count 0 top/a:unsupported_sva top/prop_supported1 %i
|
|
select -assert-count 0 top/a:unsupported_sva top/prop_supported2 %i
|
|
select -assert-count 2 top/prop_supported*
|
|
|
|
logger -expect error "uses unsupported SVA constructs." 1
|
|
hierarchy -smtcheck -top top
|
|
logger -check-expected
|