From d84852e36842b1d3058b81f53aba123bcf081af8 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Mon, 7 Sep 2020 12:32:14 +0800 Subject: [PATCH] Replace unconditional pass and OOM issue with assertion failure --- README.md | 5 +- rvfi/cores/minerva/memory_bus.py | 108 ---------- rvfi/cores/minerva/verify.py | 338 ++++++++++--------------------- 3 files changed, 107 insertions(+), 344 deletions(-) delete mode 100644 rvfi/cores/minerva/memory_bus.py diff --git a/README.md b/README.md index f65c0e9..95a30e8 100644 --- a/README.md +++ b/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 -- 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 +- ~~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~~ +- 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 diff --git a/rvfi/cores/minerva/memory_bus.py b/rvfi/cores/minerva/memory_bus.py deleted file mode 100644 index e1f3e83..0000000 --- a/rvfi/cores/minerva/memory_bus.py +++ /dev/null @@ -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 diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index e9663d4..a28b53f 100644 --- a/rvfi/cores/minerva/verify.py +++ b/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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) + m.d.comb += insn_spec.reset.eq(AnySeq(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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) - m.d.comb += pc_fwd_spec.reset.eq(0) - m.d.comb += pc_fwd_spec.check.eq(1) + m.d.comb += pc_fwd_spec.reset.eq(AnySeq(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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) - m.d.comb += pc_bwd_spec.reset.eq(0) - m.d.comb += pc_bwd_spec.check.eq(1) + m.d.comb += pc_bwd_spec.reset.eq(AnySeq(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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) + + m.d.comb += reg_spec.reset.eq(AnySeq(1)) + m.d.comb += reg_spec.check.eq(AnySeq(1)) - 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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) + + m.d.comb += causal_spec.reset.eq(AnySeq(1)) + m.d.comb += causal_spec.check.eq(AnySeq(1)) - 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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) + + m.d.comb += liveness_spec.reset.eq(AnySeq(1)) + m.d.comb += liveness_spec.trig.eq(AnySeq(1)) + m.d.comb ++ liveness_spec.check.eq(AnySeq(1)) - 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 - m.submodules.ibus = ibus = MemoryBus() - m.d.comb += ibus.adr.eq(cpu.ibus.adr) - m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w) - m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r) - m.d.comb += ibus.sel.eq(cpu.ibus.sel) - m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) - m.d.comb += ibus.stb.eq(cpu.ibus.stb) - m.d.comb += cpu.ibus.ack.eq(ibus.ack) - m.d.comb += ibus.we.eq(cpu.ibus.we) - 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) + # Wire input ports to Minerva core + m.d.comb += cpu.external_interrupt.eq(AnySeq(32)) + m.d.comb += cpu.timer_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.software_interrupt.eq(AnySeq(1)) + m.d.comb += cpu.ibus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.ibus.ack.eq(AnySeq(1)) + m.d.comb += cpu.ibus.err.eq(AnySeq(1)) + m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32)) + m.d.comb += cpu.dbus.ack.eq(AnySeq(1)) + m.d.comb += cpu.dbus.err.eq(AnySeq(1)) + + m.d.comb += unique_spec.reset.eq(AnySeq(1)) + m.d.comb += unique_spec.trig.eq(AnySeq(1)) + m.d.comb += unique_spec.check.eq(AnySeq(1)) - 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 + '*')