From f8ee8bd094bd9629cc43bba397e3a56e2ffefd81 Mon Sep 17 00:00:00 2001 From: Tobias Platen Date: Mon, 1 Jun 2020 17:56:21 +0200 Subject: [PATCH] proof_datamerger wip --- src/soc/experiment/proof_datamerger.py | 52 ++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 src/soc/experiment/proof_datamerger.py diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/proof_datamerger.py new file mode 100644 index 00000000..2e4112f2 --- /dev/null +++ b/src/soc/experiment/proof_datamerger.py @@ -0,0 +1,52 @@ +# Proof of correctness for partitioned equal signal combiner +# Copyright (C) 2020 Michael Nolan +# Copyright (C) 2020 Tobias Platen + +from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, + signed) +from nmigen.asserts import Assert, AnyConst, Assume, Cover +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil + +from soc.experiment.l0_cache import DataMerger + +import unittest + + +# This defines a module to drive the device under test and assert +# properties about its outputs +class Driver(Elaboratable): + def __init__(self): + # inputs and outputs + pass + + def elaborate(self, platform): + m = Module() + comb = m.d.comb + + array_size = 8 + m.submodules.dut = dut = DataMerger(array_size) + + # convenience variables + # Assert that op gets copied from the input to output + + # TODO: investigate error + "Object (rec data en) cannot be used as a key in value collections" + return m + + +class DataMergerTestCase(FHDLTestCase): + def test_formal(self): + module = Driver() + # self.assertFormal(module, mode="bmc", depth=2) + # self.assertFormal(module, mode="cover", depth=2) + self.assertFormal(module, mode="prove") + def test_ilang(self): + dut = Driver() + vl = rtlil.convert(dut, ports=[]) + with open("main_stage.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() -- 2.30.2