From fe835e272dd3e02bef998bc695f6bc5506812978 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Thu, 27 Aug 2020 10:48:35 +0800 Subject: [PATCH] Replace RV32I with RV32M for Minerva verification tasks --- rvfi/cores/minerva/verify.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index 3472da0..e9663d4 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -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 ...")