From: Cesar Strauss <cestrauss@gmail.com>
Date: Wed, 12 Oct 2022 12:41:42 +0000 (-0300)
Subject: If the ALU is idle, do not assert valid
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d9b75ad1ae14b0f645e5a1bde343c1db85274a7;p=soc.git

If the ALU is idle, do not assert valid
---

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)