X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;h=fc3ce637bc0ebbbab37469caa65eabbbfa0500e9;hb=2d2b85257f887ac68e01eac35619f4129a29c1b4;hp=cbbe8570cd6701ed6152b024ba8bbef6d84876f0;hpb=b798c228e694ffee8c1ba371f73cd7ed0b666588;p=soc.git

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index cbbe8570..fc3ce637 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -131,6 +131,10 @@ class CompALUMultiTestCase(FHDLTestCase):
         m.d.comb += do_alu_write.eq(alu.p.i_valid & alu.p.o_ready)
         cnt_alu_write = Signal(4)
         m.d.sync += cnt_alu_write.eq(cnt_alu_write + do_alu_write)
+        do_alu_read = Signal()
+        m.d.comb += do_alu_read.eq(alu.n.o_valid & alu.n.i_ready)
+        cnt_alu_read = Signal(4)
+        m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read)
 
         # Ask the formal engine to give an example
         m.d.comb += Cover((cnt_issue == 2)
@@ -138,7 +142,8 @@ class CompALUMultiTestCase(FHDLTestCase):
                           & (cnt_read[1] == 1)
                           & (cnt_write[0] == 1)
                           & (cnt_write[1] == 1)
-                          & (cnt_alu_write == 1))
+                          & (cnt_alu_write == 1)
+                          & (cnt_alu_read == 1))
         self.assertFormal(m, mode="cover", depth=10)