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

import sys
import traceback
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 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 *

stderr = sys.stderr
sys.stderr = open('/dev/null', 'w')

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLui,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LuiTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LuiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnAuipc,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 AuipcTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(AuipcSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnJal,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 JalTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(JalSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnJalr,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 JalrTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(JalrSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBeq,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BeqTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BeqSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBne,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BneTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BneSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBlt,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BltTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BltSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBge,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BgeTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BgeSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBltu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BltuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BltuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnBgeu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 BgeuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(BgeuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLb,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LbTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LbSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLh,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LhTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LhSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLw,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LwTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LwSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLbu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LbuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LbuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnLhu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 LhuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(LhuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSb,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SbTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SbSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSh,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 ShTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(ShSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSw,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SwTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SwSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnAddi,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 AddiTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(AddiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSlti,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SltiTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SltiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSltiu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SltiuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SltiuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnXori,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 XoriTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(XoriSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnOri,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 OriTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(OriSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnAndi,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 AndiTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(AndiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSlli,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SlliTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SlliSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSrli,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SrliTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SrliSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSrai,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SraiTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SraiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnAdd,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 AddTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(AddSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSub,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SubTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SubSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSll,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SllTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SllSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSlt,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SltTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SltSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSltu,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SltuTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SltuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnXor,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 XorTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(XorSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSrl,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SrlTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SrlSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnSra,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 SraTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(SraSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnOr,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 OrTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(OrSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32,
            RISCV_FORMAL_XLEN=32,
            RISCV_FORMAL_CSR_MISA=False,
            RISCV_FORMAL_COMPRESSED=False,
            RISCV_FORMAL_ALIGNED_MEM=False,
            insn_model=InsnAnd,
            rvformal_addr_valid=lambda x:Const(1))

        m.d.comb += insn_spec.reset.eq(0)
        m.d.comb += insn_spec.check.eq(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 AndTestCase(FHDLTestCase):
    def verify(self):
        self.assertFormal(AndSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(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.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="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(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.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="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.reg_spec = reg_spec = RegCheck(RISCV_FORMAL_XLEN=32)

        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)
        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="bmc", depth=12, engine="smtbmc --nopresat")

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

        m.submodules.cpu = cpu = Minerva(with_rvfi=True)
        m.submodules.causal_spec = causal_spec = CausalCheck()

        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)
        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="bmc", depth=12, engine="smtbmc --nopresat")

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

try:
    print("Verifying RV32I instructions ...")
    LuiTestCase().verify()
    AuipcTestCase().verify()
    JalTestCase().verify()
    JalrTestCase().verify()
    BeqTestCase().verify()
    BneTestCase().verify()
    BltTestCase().verify()
    BgeTestCase().verify()
    BltuTestCase().verify()
    BgeuTestCase().verify()
    LbTestCase().verify()
    LhTestCase().verify()
    LwTestCase().verify()
    LbuTestCase().verify()
    LhuTestCase().verify()
    SbTestCase().verify()
    ShTestCase().verify()
    SwTestCase().verify()
    AddiTestCase().verify()
    SltiTestCase().verify()
    SltiuTestCase().verify()
    XoriTestCase().verify()
    OriTestCase().verify()
    AndiTestCase().verify()
    SlliTestCase().verify()
    SrliTestCase().verify()
    SraiTestCase().verify()
    AddTestCase().verify()
    SubTestCase().verify()
    SllTestCase().verify()
    SltTestCase().verify()
    SltuTestCase().verify()
    XorTestCase().verify()
    SrlTestCase().verify()
    SraTestCase().verify()
    OrTestCase().verify()
    AndTestCase().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()
except:
    sys.stderr = stderr
    traceback.print_exc()
    sys.exit(1)

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