1833 lines
80 KiB
Python
1833 lines
80 KiB
Python
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)
|