examples: Fix use of SVA value change expressions

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.

diff --git a/docs/examples/multiclk/dpmem.sv b/docs/examples/multiclk/dpmem.sv
index 87e4f61fe48df41323e3cbdaecb249f1b94ba4fd..4a920e4e4696003cd822297d48082874e5aea34f 100644 (file)
--- a/docs/examples/multiclk/dpmem.sv
+++ b/docs/examples/multiclk/dpmem.sv
@@ -47,9 +47,9 @@ module top (
        (* gclk *) reg gclk;
 
        always @(posedge gclk) begin
-               assume ($stable(rc) || $stable(wc));
-
                if (!init) begin
+                       assume ($stable(rc) || $stable(wc));
+
                        if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
                                assert (shadow_data == rd);
                        end