From ba9f154a900f6cdba21644797111772f615b06ba Mon Sep 17 00:00:00 2001 From: Tobias Platen Date: Wed, 3 Jun 2020 14:19:40 +0200 Subject: [PATCH] whitespace fix for proof_datamerger.py --- src/soc/experiment/proof_datamerger.py | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/proof_datamerger.py index 0f6b8e5d..fb80b632 100644 --- 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=[]) -- 2.30.2