yosys/tests/sva/nested_clk_else.sv at 1b25e1cee00a3d73ab42706684860f476bbb813e - mirrors/yosys - Libre-Chip.org

mirrors/yosys

mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 01:24:10 +00:00

Jannis Harder 96f64f4788 verific: Fix conditions of SVAs with explicit clocks within procedures

For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.

2022-05-03 14:13:08 +02:00

12 lines

241 B

Systemverilog

Raw Blame History

 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