From: Jannis Harder <me@jix.one>
Date: Wed, 11 May 2022 08:38:54 +0000 (+0200)
Subject: examples: Fix use of SVA value change expressions
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fedfae0e9c1b0e5fdd81b268f7b94e40f08e9349;p=SymbiYosys.git

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 87e4f61..4a920e4 100644
--- 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