From fedfae0e9c1b0e5fdd81b268f7b94e40f08e9349 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 11 May 2022 10:38:54 +0200 Subject: [PATCH] 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. --- docs/examples/multiclk/dpmem.sv | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.30.2