X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;h=2bab836ab8f2eda3778383ed0811303972250e3e;hb=099825f7d53fb64adb30e363fd359eda3d1f14cd;hp=6edb8043b564323d339ae82d638df2cb2bd66fd1;hpb=0d9b75ad1ae14b0f645e5a1bde343c1db85274a7;p=soc.git

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 6edb8043..2bab836a 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, Assume
+from nmigen.hdl.ast import Cover, Const, Assume, Assert
 from nmutil.formaltest import FHDLTestCase
 from nmutil.singlepipe import ControlBase
 
@@ -153,6 +153,18 @@ class CompALUMultiTestCase(FHDLTestCase):
         with m.If(cnt_alu_read == cnt_alu_write):
             m.d.comb += Assume(~alu.n.o_valid)
 
+        # Invariant check
+        # For every instruction issued, at any point in time,
+        # each operand was either:
+        # 1) Already read
+        # 2) Not read yet, but the read is pending (rel_o high)
+        # 3) Masked
+        for i in range(dut.n_src):
+            sum_read = Signal(4)
+            m.d.comb += sum_read.eq(
+                cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i])
+            m.d.comb += Assert(sum_read == cnt_issue)
+
         # Ask the formal engine to give an example
         m.d.comb += Cover((cnt_issue == 2)
                           & (cnt_read[0] == 1)
@@ -164,6 +176,8 @@ class CompALUMultiTestCase(FHDLTestCase):
                           & (cnt_masked_read[0] == 1)
                           & (cnt_masked_read[1] == 1))
         self.assertFormal(m, mode="cover", depth=10)
+        # Check assertions
+        self.assertFormal(m, mode="bmc", depth=10)
 
 
 if __name__ == "__main__":