M-Labs/riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Replace RV32I with RV32M for Minerva verification tasks

Browse Source
This commit is contained in:
Donald Sebastian Leung 2020-08-27 10:48:35 +08:00
parent 1ea25a4886
commit fe835e272d
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
rvfi/cores/minerva/verify.py
View File

@ -7,12 +7,12 @@ from ...checks.causal_check import *
from ...checks.liveness_check import *
from ...checks.unique_check import *
from minerva.core import *
from ...insns.isa_rv32i import *
from ...insns.isa_rv32m import *
from .memory_bus import *
from collections import namedtuple
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem'])
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem', 'altops'])
class InsnSpec(Elaboratable):
def __init__(self, insn_model):
@ -23,7 +23,7 @@ class InsnSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.insn_spec = insn_spec = InsnCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
params=RISCVFormalParameters(32, 32, False, False, False, True),
insn_model=self.insn_model,
rvformal_addr_valid=lambda x:Const(1))
@ -87,7 +87,7 @@ class InsnSpec(Elaboratable):
class InsnTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(InsnSpec(IsaRV32I), mode="bmc", depth=40, engine="smtbmc --nopresat")
self.assertFormal(InsnSpec(IsaRV32M), mode="bmc", depth=40, engine="smtbmc --nopresat")
class PcFwdSpec(Elaboratable):
def elaborate(self, platform):
@ -95,7 +95,7 @@ class PcFwdSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
params=RISCVFormalParameters(32, 32, False, False, False, True),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
@ -149,7 +149,7 @@ class PcBwdSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
params=RISCVFormalParameters(32, 32, False, False, False, True),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
@ -202,7 +202,7 @@ class RegSpec(Elaboratable):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False))
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False, True))
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
@ -411,7 +411,7 @@ print('* Verifying the Minerva core ...
print('*' + ' ' * 78 + '*')
print('*' * 80)
print("Verifying RV32I instructions ...")
print("Verifying RV32M instructions ...")
InsnTestCase().verify()
print("Verifying PC forward checks ...")