mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 00:55:32 +00:00
Merge pull request #3297 from jix/sva_nested_clk_else
verific: Fix conditions of SVAs with explicit clocks within procedures
This commit is contained in:
commit
5ca2ee0c31
4 changed files with 27 additions and 5 deletions
11
tests/sva/nested_clk_else.sv
Normal file
11
tests/sva/nested_clk_else.sv
Normal file
|
@ -0,0 +1,11 @@
|
|||
module top (input clk, a, b);
|
||||
always @(posedge clk) begin
|
||||
if (a);
|
||||
else assume property (@(posedge clk) b);
|
||||
end
|
||||
|
||||
`ifndef FAIL
|
||||
assume property (@(posedge clk) !a);
|
||||
`endif
|
||||
assert property (@(posedge clk) b);
|
||||
endmodule
|
Loading…
Add table
Add a link
Reference in a new issue