From: Tobias Platen <tplaten@posteo.de>
Date: Wed, 3 Jun 2020 13:15:02 +0000 (+0200)
Subject: more work on proof_datamerger.py
X-Git-Tag: div_pipeline~635
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a55b2fb3129627ad78a829fb1c8415f2a96057e6;p=soc.git

more work on proof_datamerger.py
---

diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/proof_datamerger.py
index fb80b632..cfa936e1 100644
--- a/src/soc/experiment/proof_datamerger.py
+++ b/src/soc/experiment/proof_datamerger.py
@@ -40,7 +40,14 @@ class Driver(Elaboratable):
         with m.If(allzero):
             comb += Assert(dut.data_o == 0)
         with m.Else():
-            TODO
+            comb += Assume(dut.data_o != 0) # at least one output bit is set
+            for j in range(dut.array_size):
+                for b in range(0,8):
+                    with m.If(dut.data_o.en[b]):
+                        comb += Assume(dut.data_i[j].en[b])
+                for b in range(0,128):
+                    with m.If(dut.data_o.data[b]):
+                        comb += Assume(dut.data_i[j].data[b])
 
         return m