mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

examples: Fix use of SVA value change expressions

Browse source 
The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.
This commit is contained in:
Jannis Harder 2022-05-11 10:38:54 +02:00
parent 832888f0f0
commit fedfae0e9c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
docs/examples/multiclk/dpmem.sv
View file

@ -47,9 +47,9 @@ module top (
(* gclk *) reg gclk; (* gclk *) reg gclk;
always @(posedge gclk) begin always @(posedge gclk) begin
assume ($stable(rc) || $stable(wc));
if (!init) begin if (!init) begin
assume ($stable(rc) || $stable(wc));
if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
assert (shadow_data == rd); assert (shadow_data == rd);
end end