From dad60225725b2b5513dd613afafb0f74a5bd50f0 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Fri, 21 Aug 2020 15:14:42 +0800
Subject: [PATCH] Replace individual instruction checks with ISA check
---
rvfi/checks/insn_check.py | 2 +-
rvfi/cores/minerva/verify.py | 93 ++++--------------------------------
2 files changed, 9 insertions(+), 86 deletions(-)
diff --git a/rvfi/checks/insn_check.py b/rvfi/checks/insn_check.py
index 54ad837..1e65a96 100644
--- a/rvfi/checks/insn_check.py
+++ b/rvfi/checks/insn_check.py
@@ -10,7 +10,7 @@ class InsnCheck(Elaboratable):
# Core-specific parameters
self.params = params
- # Instruction under test
+ # ISA under test
self.insn_model = insn_model
# Address validity and equality
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index e9f0b95..2b1b8dc 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -7,43 +7,7 @@ from ...checks.causal_check import *
from ...checks.liveness_check import *
from ...checks.unique_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 *
+from ...insns.isa_rv32i import *
from ...riscv_formal_parameters import *
class InsnSpec(Elaboratable):
@@ -88,48 +52,7 @@ class InsnSpec(Elaboratable):
class InsnTestCase(FHDLTestCase):
def verify(self):
- insns = [
- ('LUI', InsnLui),
- ('AUIPC', InsnAuipc),
- ('JAL', InsnJal),
- ('JALR', InsnJalr),
- ('BEQ', InsnBeq),
- ('BNE', InsnBne),
- ('BLT', InsnBlt),
- ('BGE', InsnBge),
- ('BLTU', InsnBltu),
- ('BGEU', InsnBgeu),
- ('LB', InsnLb),
- ('LH', InsnLh),
- ('LW', InsnLw),
- ('LBU', InsnLbu),
- ('LHU', InsnLhu),
- ('SB', InsnSb),
- ('SH', InsnSh),
- ('SW', InsnSw),
- ('ADDI', InsnAddi),
- ('SLTI', InsnSlti),
- ('SLTIU', InsnSltiu),
- ('XORI', InsnXori),
- ('ORI', InsnOri),
- ('ANDI', InsnAndi),
- ('SLLI', InsnSlli),
- ('SRLI', InsnSrli),
- ('SRAI', InsnSrai),
- ('ADD', InsnAdd),
- ('SUB', InsnSub),
- ('SLL', InsnSll),
- ('SLT', InsnSlt),
- ('SLTU', InsnSltu),
- ('XOR', InsnXor),
- ('SRL', InsnSrl),
- ('SRA', InsnSra),
- ('OR', InsnOr),
- ('AND', InsnAnd)
- ]
- for insn_name, insn_model in insns:
- print("- Verifying instruction %s ..." % insn_name)
- self.assertFormal(InsnSpec(insn_model), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(InsnSpec(IsaRV32I), mode="bmc", depth=40, engine="smtbmc --nopresat")
class PcFwdSpec(Elaboratable):
def elaborate(self, platform):
@@ -152,7 +75,7 @@ class PcFwdSpec(Elaboratable):
class PcFwdTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(PcFwdSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(PcFwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class PcBwdSpec(Elaboratable):
def elaborate(self, platform):
@@ -175,7 +98,7 @@ class PcBwdSpec(Elaboratable):
class PcBwdTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(PcBwdSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(PcBwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class RegSpec(Elaboratable):
def elaborate(self, platform):
@@ -199,7 +122,7 @@ class RegSpec(Elaboratable):
class RegTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(RegSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(RegSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class CausalSpec(Elaboratable):
def elaborate(self, platform):
@@ -220,7 +143,7 @@ class CausalSpec(Elaboratable):
class CausalTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(CausalSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(CausalSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class LivenessSpec(Elaboratable):
def elaborate(self, platform):
@@ -240,7 +163,7 @@ class LivenessSpec(Elaboratable):
class LivenessTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(LivenessSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(LivenessSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class UniqueSpec(Elaboratable):
def elaborate(self, platform):
@@ -259,7 +182,7 @@ class UniqueSpec(Elaboratable):
class UniqueTestCase(FHDLTestCase):
def verify(self):
- self.assertFormal(UniqueSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
+ self.assertFormal(UniqueSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
print('*' * 80)
print('*' + ' ' * 78 + '*')