more work on proof_datamerger.py

diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/proof_datamerger.py
index fb80b63274f19da97ae9c69a08d49dfc6943df3b..cfa936e1cfb0241201a3fce0b4f5d36aa57d1b5d 100644 (file)
--- 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