whitespace fix for proof_datamerger.py

diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/proof_datamerger.py
index 0f6b8e5d5e028e9dac26f32d2a1a63aef7afa4e3..fb80b63274f19da97ae9c69a08d49dfc6943df3b 100644 (file)
--- a/src/soc/experiment/proof_datamerger.py
+++ b/src/soc/experiment/proof_datamerger.py
@@ -4,7 +4,7 @@
 
 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
                     signed)
-from nmigen.asserts import Assert, AnyConst,AnySeq, Assume, Cover
+from nmigen.asserts import Assert, AnyConst, AnySeq, Assume, Cover
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil
 
@@ -23,23 +23,25 @@ class Driver(Elaboratable):
     def elaborate(self, platform):
         m = Module()
         comb = m.d.comb
-        
+
         array_size = 8
         m.submodules.dut = dut = DataMerger(array_size)
-        
-        #assign anyseq to inputs
+
+        # assign anyseq to inputs
         for j in range(dut.array_size):
             comb += dut.addr_array_i[j].eq(AnySeq(dut.array_size))
             comb += dut.data_i[j].eq(AnySeq(16+128))
-        
-        allzero = 1    
+
+        allzero = 1
         for j in range(dut.array_size):
-              allzero = (dut.addr_array_i[j] == 0) & allzero
-            
-        #assert that the output is zero when the datamerger is idle
+            allzero = (dut.addr_array_i[j] == 0) & allzero
+
+        # assert that the output is zero when the datamerger is idle
         with m.If(allzero):
-            comb += Assert(dut.data_o==0)
-    
+            comb += Assert(dut.data_o == 0)
+        with m.Else():
+            TODO
+
         return m
 
 
@@ -50,6 +52,7 @@ class DataMergerTestCase(FHDLTestCase):
         self.assertFormal(module, mode="bmc", depth=2)
         # self.assertFormal(module, mode="cover", depth=2)     # case can happen
         # XXX self.assertFormal(module, mode="prove")          # uses induction
+
     def test_ilang(self):
         dut = Driver()
         vl = rtlil.convert(dut, ports=[])