From 769a8d5444f46cd093ff03645658198eaa8bd76d Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Tue, 14 Jul 2020 12:17:45 -0700 Subject: [PATCH] SPR: FV that should fail currently passes WIP. Cannot figure out why this is not failing. Code review requested. --- src/soc/fu/spr/formal/proof_main_stage.py | 54 +++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 src/soc/fu/spr/formal/proof_main_stage.py diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py new file mode 100644 index 00000000..0c7d5231 --- /dev/null +++ b/src/soc/fu/spr/formal/proof_main_stage.py @@ -0,0 +1,54 @@ +# Proof of correctness for SPR pipeline, main stage + + +""" +Links: +* https://bugs.libre-soc.org/show_bug.cgi?id=418 +""" + +from os import getenv + +from unittest import skipUnless + +from nmigen import (Elaboratable, Module) +from nmigen.asserts import Assert +from nmigen.cli import rtlil + +from nmutil.formaltest import FHDLTestCase + +from soc.fu.spr.main_stage import SPRMainStage +from soc.fu.spr.pipe_data import SPRPipeSpec + + +class Driver(Elaboratable): + """ + Defines a module to drive the device under test and assert properties + about its outputs. + """ + + def elaborate(self, platform): + m = Module() + comb = m.d.comb + + dut = SPRMainStage(SPRPipeSpec(id_wid=2)) + + # Output context is the same as the input context. + comb += Assert(dut.o.ctx != dut.i.ctx) + + return m + + +class SPRMainStageTestCase(FHDLTestCase): + @skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]") + def test_formal(self): + self.assertFormal(Driver(), mode="bmc", depth=100) + self.assertFormal(Driver(), mode="cover", depth=100) + + def test_ilang(self): + vl = rtlil.convert(Driver(), ports=[]) + with open("spr_main_stage.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() -- 2.30.2