Replace unconditional pass and OOM issue with assertion failure

README.md

@@ -35,8 +35,9 @@ The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but yet to be f
 
 ## Known Issues
 
-- 21/08/2020: Verification passes unconditionally, even in the presence of obvious bugs. This is due to the `rvfi.valid` signal from the CPU being held at constant 0. Suitable instruction and data buses as well as interrupt signals have not been wired to Minerva which is likely preventing the core and verification from functioning properly
+- ~~21/08/2020: Verification passes unconditionally, even in the presence of obvious bugs. This is due to the `rvfi.valid` signal from the CPU being held at constant 0. Suitable instruction and data buses as well as interrupt signals have not been wired to Minerva which is likely preventing the core and verification from functioning properly~~
-- 25/08/2020: Interrupts have been hardwired to zero and instruction/data buses attached to the Minerva core; however, running the verification quickly exhausts available memory on a machine with 32G RAM. Possible culprit: huge number of `Assume` statements on memory values
+- ~~25/08/2020: Interrupts have been hardwired to zero and instruction/data buses attached to the Minerva core; however, running the verification quickly exhausts available memory on a machine with 32G RAM. Possible culprit: huge number of `Assume` statements on memory values~~
+- 07/09/2020: Instruction checks fail at line 201 asserting the value of `rd_wdata`. At least we now have a proper failure instead of an unconditional pass or an out of memory issue. Whether the translated specs themselves are in error is under investigation.
 
 ## License
 

rvfi/cores/minerva/memory_bus.py

@@ -1,108 +0,0 @@
-from nmigen import *
-from nmigen.asserts import *
-
-"""
-Memory Bus (Wishbone Slave)
-"""
-
-class MemoryBus(Elaboratable):
-    def __init__(self):
-        # Input/output ports
-        self.adr = Signal(30)
-        self.dat_w = Signal(32)
-        self.dat_r = Signal(32)
-        self.sel = Signal(4) # ignored during reads, just return the whole word
-        self.cyc = Signal(1)
-        self.stb = Signal(1)
-        self.ack = Signal(1, reset=0)
-        self.we = Signal(1)
-        self.cti = Signal(3) # ignored (signal for performance purposes only?)
-        self.bte = Signal(2) # ignored (signal for performance purposes only?)
-        self.err = Const(0) # unsupported
-
-        # Memory store
-        self.memory = Array(AnySeq(32) for _ in range(1 << 30))
-    def ports(self):
-        input_ports = [
-            self.adr,
-            self.dat_w,
-            self.sel,
-            self.cyc,
-            self.stb,
-            self.we,
-            self.cti,
-            self.bte
-        ]
-        output_ports = [
-            self.dat_r,
-            self.ack,
-            self.err
-        ]
-        return input_ports + output_ports
-    def elaborate(self, platform):
-        m = Module()
-
-        # Indicator of when Past() is valid
-        f_past_valid = Signal(1, reset=0)
-        m.d.sync += f_past_valid.eq(1)
-
-        # Memory store in the past clock cycle
-        f_past_memory = Array(Signal(32) for _ in range(1 << 30))
-        for i in range(1 << 30):
-            m.d.sync += f_past_memory[i].eq(self.memory[i])
-
-        # Unless both cyc and stb are asserted:
-        # - ack should be de-asserted on the next clock edge
-        # - memory contents should remain constant
-        with m.If(~self.cyc | ~self.stb):
-            m.d.sync += ack.eq(0)
-        with m.If(f_past_valid & ((~Past(self.cyc)) | ~Past(self.stb))):
-            for i in range(1 << 30):
-                m.d.comb += Assume(self.memory[i] == f_past_memory[i])
-
-        # If cyc, stb are asserted and ack de-asserted:
-        # - For a read (i.e. WE is de-asserted):
-        #   - dat_r should contain the word under the given address at the
-        #     next clock cycle
-        #   - ack should be asserted in the next clock cycle
-        #   - memory contents should remain constant
-        with m.If(self.cyc & self.stb & ~self.ack):
-            with m.If(~self.we):
-                m.d.sync += self.dat_r.eq(self.memory[self.adr])
-                m.d.sync += self.ack.eq(1)
-        with m.If(f_past_valid & Past(self.cyc) & Past(self.stb) & ~Past(self.ack)):
-            with m.If(~Past(self.we)):
-                for i in range(1 << 30):
-                    m.d.comb += Assume(self.memory[i] == f_past_memory[i])
-        # - For a write (i.e. WE is asserted)
-        #   - ack should be asserted in the next clock cycle
-        #   - For the word of data under adr:
-        #     - If the select bit is asserted, the corresponding byte is
-        #       written to memory
-        #     - Otherwise, the corresponding byte remains constant
-        #   - All other memory content should remain constant
-        with m.If(self.cyc & self.stb & ~self.ack):
-            with m.If(self.we):
-                m.d.sync += self.ack.eq(1)
-        with m.If(f_past_valid & Past(self.cyc) & Past(self.stb) & ~Past(self.ack)):
-            with m.If(Past(self.we)):
-                for i in range(1 << 30):
-                    with m.If(i == Past(self.adr)):
-                        for j in range(4):
-                            with m.If(Past(self.sel)[j]):
-                                m.d.comb += Assume(self.memory[i][j*8:j*8+8] == Past(self.dat_w)[j*8:j*8+8])
-                            with m.Else():
-                                m.d.comb += Assume(self.memory[i][j*8:j*8+8] == f_past_memory[i][j*8:j*8+8])
-                    with m.Else():
-                        m.d.comb += Assume(self.memory[i] == f_past_memory[i])
-
-        # If ack is asserted:
-        # - ack should be de-asserted in the next clock cycle
-        # - memory contents should remain constant
-        with m.If(self.ack):
-            m.d.sync += self.ack.eq(0)
-        with m.If(f_past_valid & Past(self.ack)):
-            for i in range(1 << 30):
-                m.d.comb += Assume(self.memory[i] == f_past_memory[i])
-
-        return m

rvfi/cores/minerva/verify.py

@@ -8,7 +8,6 @@ from ...checks.liveness_check import *
 from ...checks.unique_check import *
 from minerva.core import *
 from ...insns.isa_rv32m import *
-from .memory_bus import *
 from collections import namedtuple
 
 RISCVFormalParameters = namedtuple('RISCVFormalParameters',
@@ -27,39 +26,19 @@ class InsnSpec(Elaboratable):
             insn_model=self.insn_model,
             rvformal_addr_valid=lambda x:Const(1))
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
-        # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += insn_spec.reset.eq(0)
+        m.d.comb += insn_spec.reset.eq(AnySeq(1))
-        m.d.comb += insn_spec.check.eq(1)
+        m.d.comb += insn_spec.check.eq(AnySeq(1))
 
         m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order)
@@ -87,7 +66,8 @@ class InsnSpec(Elaboratable):
 
 class InsnTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(InsnSpec(IsaRV32M), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(InsnSpec(IsaRV32M), mode="cover", depth=40)
+        self.assertFormal(InsnSpec(IsaRV32M), mode="bmc", depth=40)
 
 class PcFwdSpec(Elaboratable):
     def elaborate(self, platform):
@@ -98,39 +78,19 @@ class PcFwdSpec(Elaboratable):
             params=RISCVFormalParameters(32, 32, False, False, False, True),
             rvformal_addr_valid=lambda x:Const(1))
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
-        # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += pc_fwd_spec.reset.eq(0)
+        m.d.comb += pc_fwd_spec.reset.eq(AnySeq(1))
-        m.d.comb += pc_fwd_spec.check.eq(1)
+        m.d.comb += pc_fwd_spec.check.eq(AnySeq(1))
 
         m.d.comb += pc_fwd_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += pc_fwd_spec.rvfi_order.eq(cpu.rvfi.order)
@@ -141,7 +101,8 @@ class PcFwdSpec(Elaboratable):
 
 class PcFwdTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(PcFwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(PcFwdSpec(), mode="cover", depth=40)
+        self.assertFormal(PcFwdSpec(), mode="bmc", depth=40)
 
 class PcBwdSpec(Elaboratable):
     def elaborate(self, platform):
@@ -152,39 +113,19 @@ class PcBwdSpec(Elaboratable):
             params=RISCVFormalParameters(32, 32, False, False, False, True),
             rvformal_addr_valid=lambda x:Const(1))
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
-        # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += pc_bwd_spec.reset.eq(0)
+        m.d.comb += pc_bwd_spec.reset.eq(AnySeq(1))
-        m.d.comb += pc_bwd_spec.check.eq(1)
+        m.d.comb += pc_bwd_spec.check.eq(AnySeq(1))
 
         m.d.comb += pc_bwd_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += pc_bwd_spec.rvfi_order.eq(cpu.rvfi.order)
@@ -195,7 +136,8 @@ class PcBwdSpec(Elaboratable):
 
 class PcBwdTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(PcBwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(PcBwdSpec(), mode="cover", depth=40)
+        self.assertFormal(PcBwdSpec(), mode="bmc", depth=40)
 
 class RegSpec(Elaboratable):
     def elaborate(self, platform):
@@ -204,39 +146,20 @@ class RegSpec(Elaboratable):
         m.submodules.cpu = cpu = Minerva(with_rvfi=True)
         m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False, True))
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
+
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
+        m.d.comb += reg_spec.reset.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
+        m.d.comb += reg_spec.check.eq(AnySeq(1))
-        # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += reg_spec.reset.eq(0)
-        m.d.comb += reg_spec.check.eq(1)
         m.d.comb += reg_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += reg_spec.rvfi_order.eq(cpu.rvfi.order)
         m.d.comb += reg_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
@@ -250,7 +173,8 @@ class RegSpec(Elaboratable):
 
 class RegTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(RegSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(RegSpec(), mode="cover", depth=40)
+        self.assertFormal(RegSpec(), mode="bmc", depth=40)
 
 class CausalSpec(Elaboratable):
     def elaborate(self, platform):
@@ -259,39 +183,20 @@ class CausalSpec(Elaboratable):
         m.submodules.cpu = cpu = Minerva(with_rvfi=True)
         m.submodules.causal_spec = causal_spec = CausalCheck()
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
+
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
+        m.d.comb += causal_spec.reset.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
+        m.d.comb += causal_spec.check.eq(AnySeq(1))
-        # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += causal_spec.reset.eq(0)
-        m.d.comb += causal_spec.check.eq(1)
         m.d.comb += causal_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += causal_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
         m.d.comb += causal_spec.rvfi_order.eq(cpu.rvfi.order)
@@ -302,7 +207,8 @@ class CausalSpec(Elaboratable):
 
 class CausalTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(CausalSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(CausalSpec(), mode="cover", depth=40)
+        self.assertFormal(CausalSpec(), mode="bmc", depth=40)
 
 class LivenessSpec(Elaboratable):
     def elaborate(self, platform):
@@ -311,49 +217,31 @@ class LivenessSpec(Elaboratable):
         m.submodules.cpu = cpu = Minerva(with_rvfi=True)
         m.submodules.liveness_spec = liveness_spec = LivenessCheck()
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
+
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
+        m.d.comb += liveness_spec.reset.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
+        m.d.comb += liveness_spec.trig.eq(AnySeq(1))
-        # Connect Wishbone data bus to Minerva CPU
+        m.d.comb ++ liveness_spec.check.eq(AnySeq(1))
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += liveness_spec.reset.eq(0)
         m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
-        m.d.comb += liveness_spec.trig.eq(1)
         m.d.comb += liveness_spec.rvfi_halt.eq(cpu.rvfi.halt)
-        m.d.comb += liveness_spec.check.eq(1)
 
         return m
 
 class LivenessTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(LivenessSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(LivenessSpec(), mode="cover", depth=40)
+        self.assertFormal(LivenessSpec(), mode="bmc", depth=40)
 
 class UniqueSpec(Elaboratable):
     def elaborate(self, platform):
@@ -362,48 +250,30 @@ class UniqueSpec(Elaboratable):
         m.submodules.cpu = cpu = Minerva(with_rvfi=True)
         m.submodules.unique_spec = unique_spec = UniqueCheck()
 
-        # Connect Wishbone instruction bus to Minerva CPU
+        # Wire input ports to Minerva core
-        m.submodules.ibus = ibus = MemoryBus()
+        m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
-        m.d.comb += ibus.adr.eq(cpu.ibus.adr)
+        m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
-        m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
+        m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
+        m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32))
-        m.d.comb += ibus.sel.eq(cpu.ibus.sel)
+        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
+        m.d.comb += cpu.ibus.err.eq(AnySeq(1))
-        m.d.comb += ibus.stb.eq(cpu.ibus.stb)
+        m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
-        m.d.comb += cpu.ibus.ack.eq(ibus.ack)
+        m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
-        m.d.comb += ibus.we.eq(cpu.ibus.we)
+        m.d.comb += cpu.dbus.err.eq(AnySeq(1))
-        m.d.comb += ibus.cti.eq(cpu.ibus.cti)
+        
-        m.d.comb += ibus.bte.eq(cpu.ibus.bte)
+        m.d.comb += unique_spec.reset.eq(AnySeq(1))
-        m.d.comb += cpu.ibus.err.eq(ibus.err)
+        m.d.comb += unique_spec.trig.eq(AnySeq(1))
-        # Connect Wishbone data bus to Minerva CPU
+        m.d.comb += unique_spec.check.eq(AnySeq(1))
-        m.submodules.dbus = dbus = MemoryBus()
-        m.d.comb += dbus.adr.eq(cpu.dbus.adr)
-        m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
-        m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
-        m.d.comb += dbus.sel.eq(cpu.dbus.sel)
-        m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
-        m.d.comb += dbus.stb.eq(cpu.dbus.stb)
-        m.d.comb += cpu.dbus.ack.eq(dbus.ack)
-        m.d.comb += dbus.we.eq(cpu.dbus.we)
-        m.d.comb += dbus.cti.eq(cpu.dbus.cti)
-        m.d.comb += dbus.bte.eq(cpu.dbus.bte)
-        m.d.comb += cpu.dbus.err.eq(dbus.err)
-        # Disable all interrupts
-        m.d.comb += cpu.external_interrupt.eq(0)
-        m.d.comb += cpu.timer_interrupt.eq(0)
-        m.d.comb += cpu.software_interrupt.eq(0)
 
-        m.d.comb += unique_spec.reset.eq(0)
         m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid)
         m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)
-        m.d.comb += unique_spec.trig.eq(1)
-        m.d.comb += unique_spec.check.eq(1)
 
         return m
 
 class UniqueTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(UniqueSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
+        self.assertFormal(UniqueSpec(), mode="cover", depth=40)
+        self.assertFormal(UniqueSpec(), mode="bmc", depth=40)
 
 print('*' * 80)
 print('*' + ' ' * 78 + '*')