26 lines
894 B
Python
26 lines
894 B
Python
from nmigen import *
|
|
from nmigen.test.utils import *
|
|
from ..core import *
|
|
from ....checks.pc_bwd_check import *
|
|
|
|
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")
|