From 0d9b75ad1ae14b0f645e5a1bde343c1db85274a7 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Wed, 12 Oct 2022 09:41:42 -0300 Subject: [PATCH] If the ALU is idle, do not assert valid --- src/soc/experiment/formal/proof_compalu_multi.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index 8f75b7b0..6edb8043 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -35,7 +35,7 @@ https://bugs.libre-soc.org/show_bug.cgi?id=197 import unittest from nmigen import Signal, Module -from nmigen.hdl.ast import Cover, Const +from nmigen.hdl.ast import Cover, Const, Assume from nmutil.formaltest import FHDLTestCase from nmutil.singlepipe import ControlBase @@ -149,6 +149,9 @@ class CompALUMultiTestCase(FHDLTestCase): extra = Const(0, 1) m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra))) cnt_masked_read.append(cnt) + # If the ALU is idle, do not assert valid + with m.If(cnt_alu_read == cnt_alu_write): + m.d.comb += Assume(~alu.n.o_valid) # Ask the formal engine to give an example m.d.comb += Cover((cnt_issue == 2) -- 2.30.2