riscv-formal-nmigen/rvfi/cores/minerva/verify.py

from nmigen.test.utils import *
from ...checks.insn_check import *
from ...checks.pc_fwd_check import *
from ...checks.pc_bwd_check import *
from ...checks.reg_check import *
from ...checks.causal_check import *
from ...checks.liveness_check import *
from ...checks.unique_check import *
from minerva.core import *
from ...insns.insn_lui import *
from ...insns.insn_auipc import *
from ...insns.insn_jal import *
from ...insns.insn_jalr import *
from ...insns.insn_beq import *
from ...insns.insn_bne import *
from ...insns.insn_blt import *
from ...insns.insn_bge import *
from ...insns.insn_bltu import *
from ...insns.insn_bgeu import *
from ...insns.insn_lb import *
from ...insns.insn_lh import *
from ...insns.insn_lw import *
from ...insns.insn_lbu import *
from ...insns.insn_lhu import *
from ...insns.insn_sb import *
from ...insns.insn_sh import *
from ...insns.insn_sw import *
from ...insns.insn_addi import *
from ...insns.insn_slti import *
from ...insns.insn_sltiu import *
from ...insns.insn_xori import *
from ...insns.insn_ori import *
from ...insns.insn_andi import *
from ...insns.insn_slli import *
from ...insns.insn_srli import *
from ...insns.insn_srai import *
from ...insns.insn_add import *
from ...insns.insn_sub import *
from ...insns.insn_sll import *
from ...insns.insn_slt import *
from ...insns.insn_sltu import *
from ...insns.insn_xor import *
from ...insns.insn_srl import *
from ...insns.insn_sra import *
from ...insns.insn_or import *
from ...insns.insn_and import *
from ...insns.insn_mul import *
from ...insns.insn_mulh import *
from ...insns.insn_mulhsu import *
from ...insns.insn_mulhu import *
from ...insns.insn_div import *
from ...insns.insn_divu import *
from ...insns.insn_rem import *
from ...insns.insn_remu import *
from collections import namedtuple

RISCVFormalParameters = namedtuple('RISCVFormalParameters',
    ['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem', 'altops'])

class InsnSpec(Elaboratable):
    def __init__(self, insn_model):
        self.insn_model = insn_model

    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.insn_spec = insn_spec = InsnCheck(
            params=RISCVFormalParameters(32, 32, False, False, True, True),
            insn_model=self.insn_model,
            rvformal_addr_valid=lambda x:Const(1))

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        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)
        m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn)
        m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap)
        m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt)
        m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr)
        m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode)
        m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl)
        m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
        m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
        m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
        m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
        m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
        m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)
        m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
        m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)
        m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr)
        m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask)
        m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask)
        m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata)
        m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata)

        return m

class InsnTestCase(FHDLTestCase):
    def verify(self):
        print("Verifying LUI instruction ...")
        self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=20)
        print("Verifying AUIPC instruction ...")
        self.assertFormal(InsnSpec(InsnAuipc), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=20)
        print("Verifying JAL instruction ...")
        self.assertFormal(InsnSpec(InsnJal), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=20)
        print("Verifying JALR instruction ...")
        self.assertFormal(InsnSpec(InsnJalr), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=20)
        print("Verifying BEQ instruction ...")
        self.assertFormal(InsnSpec(InsnBeq), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=20)
        print("Verifying BNE instruction ...")
        self.assertFormal(InsnSpec(InsnBne), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=20)
        print("Verifying BLT instruction ...")
        self.assertFormal(InsnSpec(InsnBlt), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=20)
        print("Verifying BGE instruction ...")
        self.assertFormal(InsnSpec(InsnBge), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=20)
        print("Verifying BLTU instruction ...")
        self.assertFormal(InsnSpec(InsnBltu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=20)
        print("Verifying BGEU instruction ...")
        self.assertFormal(InsnSpec(InsnBgeu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=20)
        print("Verifying LB instruction ...")
        self.assertFormal(InsnSpec(InsnLb), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=20)
        print("Verifying LH instruction ...")
        self.assertFormal(InsnSpec(InsnLh), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=20)
        print("Verifying LW instruction ...")
        self.assertFormal(InsnSpec(InsnLw), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=20)
        print("Verifying LBU instruction ...")
        self.assertFormal(InsnSpec(InsnLbu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=20)
        print("Verifying LHU instruction ...")
        self.assertFormal(InsnSpec(InsnLhu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=20)
        print("Verifying SB instruction ...")
        self.assertFormal(InsnSpec(InsnSb), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=20)
        print("Verifying SH instruction ...")
        self.assertFormal(InsnSpec(InsnSh), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=20)
        print("Verifying SW instruction ...")
        self.assertFormal(InsnSpec(InsnSw), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=20)
        print("Verifying ADDI instruction ...")
        self.assertFormal(InsnSpec(InsnAddi), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=20)
        print("Verifying SLTI instruction ...")
        self.assertFormal(InsnSpec(InsnSlti), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=20)
        print("Verifying SLTIU instruction ...")
        self.assertFormal(InsnSpec(InsnSltiu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=20)
        print("Verifying XORI instruction ...")
        self.assertFormal(InsnSpec(InsnXori), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=20)
        print("Verifying ORI instruction ...")
        self.assertFormal(InsnSpec(InsnOri), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=20)
        print("Verifying ANDI instruction ...")
        self.assertFormal(InsnSpec(InsnAndi), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=20)
        print("Verifying SLLI instruction ...")
        self.assertFormal(InsnSpec(InsnSlli), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=20)
        print("Verifying SRLI instruction ...")
        self.assertFormal(InsnSpec(InsnSrli), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=20)
        print("Verifying SRAI instruction ...")
        self.assertFormal(InsnSpec(InsnSrai), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=20)
        print("Verifying ADD instruction ...")
        self.assertFormal(InsnSpec(InsnAdd), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=20)
        print("Verifying SUB instruction ...")
        self.assertFormal(InsnSpec(InsnSub), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=20)
        print("Verifying SLL instruction ...")
        self.assertFormal(InsnSpec(InsnSll), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=20)
        print("Verifying SLT instruction ...")
        self.assertFormal(InsnSpec(InsnSlt), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=20)
        print("Verifying SLTU instruction ...")
        self.assertFormal(InsnSpec(InsnSltu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=20)
        print("Verifying XOR instruction ...")
        self.assertFormal(InsnSpec(InsnXor), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=20)
        print("Verifying SRL instruction ...")
        self.assertFormal(InsnSpec(InsnSrl), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=20)
        print("Verifying SRA instruction ...")
        self.assertFormal(InsnSpec(InsnSra), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=20)
        print("Verifying OR instruction ...")
        self.assertFormal(InsnSpec(InsnOr), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=20)
        print("Verifying AND instruction ...")
        self.assertFormal(InsnSpec(InsnAnd), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=20)
        print("Verifying MUL instruction ...")
        self.assertFormal(InsnSpec(InsnMul), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=20)
        print("Verifying MULH instruction ...")
        self.assertFormal(InsnSpec(InsnMulh), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=20)
        print("Verifying MULHSU instruction ...")
        self.assertFormal(InsnSpec(InsnMulhsu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=20)
        print("Verifying MULHU instruction ...")
        self.assertFormal(InsnSpec(InsnMulhu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=20)
        print("Verifying DIV instruction ...")
        self.assertFormal(InsnSpec(InsnDiv), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=20)
        print("Verifying DIVU instruction ...")
        self.assertFormal(InsnSpec(InsnDivu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=20)
        print("Verifying REM instruction ...")
        self.assertFormal(InsnSpec(InsnRem), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=20)
        print("Verifying REMU instruction ...")
        self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=20)
        self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=20)

class PcFwdSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(
            params=RISCVFormalParameters(32, 32, False, False, True, True),
            rvformal_addr_valid=lambda x:Const(1))

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        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)
        m.d.comb += pc_fwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
        m.d.comb += pc_fwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)

        return m

class PcFwdTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(PcFwdSpec(), mode="cover", depth=20)
        self.assertFormal(PcFwdSpec(), mode="bmc", depth=20)

class PcBwdSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(
            params=RISCVFormalParameters(32, 32, False, False, True, True),
            rvformal_addr_valid=lambda x:Const(1))

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        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)
        m.d.comb += pc_bwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
        m.d.comb += pc_bwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)

        return m

class PcBwdTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(PcBwdSpec(), mode="cover", depth=20)
        self.assertFormal(PcBwdSpec(), mode="bmc", depth=20)

class RegSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, True, True))

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        m.d.comb += reg_spec.reset.eq(AnySeq(1))
        m.d.comb += reg_spec.check.eq(AnySeq(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)
        m.d.comb += reg_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
        m.d.comb += reg_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
        m.d.comb += reg_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
        m.d.comb += reg_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
        m.d.comb += reg_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)

        return m

class RegTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(RegSpec(), mode="cover", depth=10)
        self.assertFormal(RegSpec(), mode="bmc", depth=10)

class CausalSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.causal_spec = causal_spec = CausalCheck()

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        m.d.comb += causal_spec.reset.eq(AnySeq(1))
        m.d.comb += causal_spec.check.eq(AnySeq(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)
        m.d.comb += causal_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
        m.d.comb += causal_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)

        return m

class CausalTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(CausalSpec(), mode="cover", depth=20)
        self.assertFormal(CausalSpec(), mode="bmc", depth=20)

class LivenessSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.liveness_spec = liveness_spec = LivenessCheck()

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)

        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.rvfi_valid.eq(cpu.rvfi.valid)
        m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
        m.d.comb += liveness_spec.rvfi_halt.eq(cpu.rvfi.halt)

        # Bounded fairness constraints
        ibus_wait = Signal(2, reset=0)
        dbus_wait = Signal(2, reset=0)
        with m.If(cpu.ibus.cyc & cpu.ibus.stb & ~(cpu.ibus.ack | cpu.ibus.err)):
            m.d.sync += ibus_wait.eq(ibus_wait + 1)
        with m.Else():
            m.d.sync += ibus_wait.eq(0)
        with m.If(cpu.dbus.cyc & cpu.dbus.stb & ~(cpu.dbus.ack | cpu.dbus.err)):
            m.d.sync += dbus_wait.eq(dbus_wait + 1)
        with m.Else():
            m.d.sync += dbus_wait.eq(0)
        m.d.comb += Assume((ibus_wait < 2) & (dbus_wait < 2))
        with m.If(liveness_spec.reset):
            m.d.sync += ibus_wait.eq(0)
            m.d.sync += dbus_wait.eq(0)

        return m

class LivenessTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LivenessSpec(), mode="cover", depth=20)
        self.assertFormal(LivenessSpec(), mode="bmc", depth=20)

class UniqueSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.cpu = cpu = Minerva(
            with_rvfi=True,
            with_muldiv=True,
            with_icache=True,
            icache_nways=2,
            icache_nlines=2,
            icache_nwords=4,
            icache_base=0x1000,
            icache_limit=0x4000,
            with_dcache=True,
            dcache_nways=2,
            dcache_nlines=2,
            dcache_nwords=4,
            dcache_base=0x1000,
            dcache_limit=0x4000)
        m.submodules.unique_spec = unique_spec = UniqueCheck()

        # Wire input ports to Minerva core
        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 += cpu.ibus.dat_r.eq(AnySeq(32))
        m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
        m.d.comb += cpu.ibus.err.eq(0)
        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(0)
        
        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.rvfi_valid.eq(cpu.rvfi.valid)
        m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)

        return m

class UniqueTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(UniqueSpec(), mode="cover", depth=20)
        self.assertFormal(UniqueSpec(), mode="bmc", depth=20)

print('*' * 80)
print('*' + ' ' * 78 + '*')
print('*                        Verifying the Minerva core ...                        *')
print('*' + ' ' * 78 + '*')
print('*' * 80)

print("Verifying RV32M instructions ...")
InsnTestCase().verify()

print("Verifying PC forward checks ...")
PcFwdTestCase().verify()

print("Verifying PC backward checks ...")
PcBwdTestCase().verify()

print("Verifying register checks ...")
RegTestCase().verify()

print("Verifying causal checks ...")
CausalTestCase().verify()

print("Verifying liveness checks ...")
LivenessTestCase().verify()

print("Verifying uniqueness checks ...")
UniqueTestCase().verify()

print('*' * 80)
print('*' + ' ' * 78 + '*')
print('*                      All verification tasks successful!                      *')
print('*' + ' ' * 78 + '*')
print('*' * 80)