From 472ccc4e4c3b7ad6cefb7a2103328b24fd1ab33a Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 1 Jun 2020 14:40:41 -0400 Subject: [PATCH] Have regfile use AnySeq instead of AnyConst --- src/soc/regfile/formal/proof_regfile.py | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py index 0dcb1964..6dc89144 100644 --- a/src/soc/regfile/formal/proof_regfile.py +++ b/src/soc/regfile/formal/proof_regfile.py @@ -2,7 +2,7 @@ from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, signed, ResetSignal) -from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial, +from nmigen.asserts import (Assert, AnySeq, Assume, Cover, Initial, Rose, Fell, Stable, Past) from nmigen.test.utils import FHDLTestCase from nmigen.cli import rtlil @@ -27,13 +27,11 @@ class Driver(Register): writethru = self.writethru _rdports = self._rdports _wrports = self._wrports - reg = self.reg - comb += _wrports[0].data_i.eq(AnyConst(8)) - comb += _wrports[0].wen.eq(AnyConst(1)) - comb += _rdports[0].ren.eq(AnyConst(1)) - sync += reg.eq(AnyConst(8)) + comb += _wrports[0].data_i.eq(AnySeq(8)) + comb += _wrports[0].wen.eq(AnySeq(1)) + comb += _rdports[0].ren.eq(AnySeq(1)) rst = ResetSignal() @@ -51,6 +49,9 @@ class Driver(Register): register_data = Signal(self.width) register_written = Signal() + # Make sure we're actually hitting a read and write + comb += Cover(_rdports[0].ren & register_written) + with m.If(init): comb += Assume(rst == 1) for port in _rdports: @@ -106,7 +107,8 @@ class TestCase(FHDLTestCase): def test_formal(self): for writethrough in [False, True]: module = Driver(writethrough) - self.assertFormal(module, mode="prove", depth=10) + self.assertFormal(module, mode="bmc", depth=10) + self.assertFormal(module, mode="cover", depth=10) def test_ilang(self): dut = Driver() -- 2.30.2