Record failing instructions in individual instruction checks
parent
d84852e368
commit
a9f1431959
|
|
@ -0,0 +1,47 @@
|
|||
Failing instructions:
|
||||
|
||||
- LUI (L200, 201, 202)
|
||||
- AUIPC (L202)
|
||||
- JAL (L202)
|
||||
- JALR (L202)
|
||||
- BEQ (L202)
|
||||
- BNE (L202)
|
||||
- BLT (L202)
|
||||
- BGE (L202)
|
||||
- BLTU (L202)
|
||||
- BGEU (L202)
|
||||
- LB (L202)
|
||||
- LH (L202, 205, 215, 217)
|
||||
- LW (L202, 205, 217)
|
||||
- LBU (L202)
|
||||
- LHU (L202, 205, 215, 217)
|
||||
- SB (L202)
|
||||
- SH (L202, 205, 209, 212, 217)
|
||||
- SW (L202, 205, 217)
|
||||
- ADDI (L202)
|
||||
- SLTI (L202)
|
||||
- SLTIU (L202)
|
||||
- XORI (L200, 202)
|
||||
- ORI (L202)
|
||||
- ANDI (L202)
|
||||
- SLLI (L200, 202)
|
||||
- SRLI (L202)
|
||||
- SRAI (L200, 202)
|
||||
- ADD (L202)
|
||||
- SUB (L202)
|
||||
- SLL (L202)
|
||||
- SLT (L200, 202)
|
||||
- SLTU (L200, 202)
|
||||
- XOR (L200, 202)
|
||||
- SRL (L201)
|
||||
- SRA (L202)
|
||||
- OR (L202)
|
||||
- AND (L202)
|
||||
- MUL (L202, 217)
|
||||
- MULH (L202, 217)
|
||||
- MULHSU (L202, 217)
|
||||
- MULHU (L202, 217)
|
||||
- DIV (L202, 217)
|
||||
- DIVU (L202, 217)
|
||||
- REM (L202, 217)
|
||||
- REMU (L202, 217)
|
||||
|
|
@ -7,7 +7,51 @@ from ...checks.causal_check import *
|
|||
from ...checks.liveness_check import *
|
||||
from ...checks.unique_check import *
|
||||
from minerva.core import *
|
||||
from ...insns.isa_rv32m 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.insn_mul import *
|
||||
from ...insns.insn_mulh import *
|
||||
from ...insns.insn_mulhsu import *
|
||||
from ...insns.insn_mulhu import *
|
||||
from ...insns.insn_div import *
|
||||
from ...insns.insn_divu import *
|
||||
from ...insns.insn_rem import *
|
||||
from ...insns.insn_remu import *
|
||||
from collections import namedtuple
|
||||
|
||||
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
|
||||
|
|
@ -66,8 +110,141 @@ class InsnSpec(Elaboratable):
|
|||
|
||||
class InsnTestCase(FHDLTestCase):
|
||||
def verify(self):
|
||||
self.assertFormal(InsnSpec(IsaRV32M), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(IsaRV32M), mode="bmc", depth=40)
|
||||
print("Verifying LUI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=40)
|
||||
print("Verifying AUIPC instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnAuipc), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=40)
|
||||
print("Verifying JAL instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnJal), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=40)
|
||||
print("Verifying JALR instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnJalr), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=40)
|
||||
print("Verifying BEQ instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBeq), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=40)
|
||||
print("Verifying BNE instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBne), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=40)
|
||||
print("Verifying BLT instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBlt), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=40)
|
||||
print("Verifying BGE instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBge), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=40)
|
||||
print("Verifying BLTU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBltu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=40)
|
||||
print("Verifying BGEU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnBgeu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=40)
|
||||
print("Verifying LB instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLb), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=40)
|
||||
print("Verifying LH instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLh), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=40)
|
||||
print("Verifying LW instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLw), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=40)
|
||||
print("Verifying LBU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLbu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=40)
|
||||
print("Verifying LHU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnLhu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=40)
|
||||
print("Verifying SB instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSb), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=40)
|
||||
print("Verifying SH instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSh), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=40)
|
||||
print("Verifying SW instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSw), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=40)
|
||||
print("Verifying ADDI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnAddi), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=40)
|
||||
print("Verifying SLTI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSlti), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=40)
|
||||
print("Verifying SLTIU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSltiu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=40)
|
||||
print("Verifying XORI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnXori), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=40)
|
||||
print("Verifying ORI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnOri), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=40)
|
||||
print("Verifying ANDI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnAndi), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=40)
|
||||
print("Verifying SLLI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSlli), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=40)
|
||||
print("Verifying SRLI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSrli), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=40)
|
||||
print("Verifying SRAI instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSrai), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=40)
|
||||
print("Verifying ADD instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnAdd), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=40)
|
||||
print("Verifying SUB instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSub), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=40)
|
||||
print("Verifying SLL instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSll), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=40)
|
||||
print("Verifying SLT instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSlt), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=40)
|
||||
print("Verifying SLTU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSltu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=40)
|
||||
print("Verifying XOR instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnXor), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=40)
|
||||
print("Verifying SRL instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSrl), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=40)
|
||||
print("Verifying SRA instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnSra), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=40)
|
||||
print("Verifying OR instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnOr), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=40)
|
||||
print("Verifying AND instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnAnd), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=40)
|
||||
print("Verifying MUL instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnMul), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=40)
|
||||
print("Verifying MULH instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnMulh), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=40)
|
||||
print("Verifying MULHSU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnMulhsu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=40)
|
||||
print("Verifying MULHU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnMulhu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=40)
|
||||
print("Verifying DIV instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnDiv), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=40)
|
||||
print("Verifying DIVU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnDivu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=40)
|
||||
print("Verifying REM instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnRem), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=40)
|
||||
print("Verifying REMU instruction ...")
|
||||
self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=40)
|
||||
self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=40)
|
||||
|
||||
class PcFwdSpec(Elaboratable):
|
||||
def elaborate(self, platform):
|
||||
|
|
|
|||
Loading…
Reference in New Issue