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

Parallelize instruction verification tasks

master
Donald Sebastian Leung 2020-09-18 13:23:17 +08:00
parent 283d8531e0
commit b0a914b48e
3 changed files with 63 additions and 140 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
README.md
View File

@ -27,7 +27,7 @@ This should run the tests (cache, multiplier, divider) provided by Minerva itsel
$ python -m rvfi.cores.minerva.verify
```
This should run in the order of a few hours.
This should complete within 2 hours.
## Scope
@ -38,7 +38,6 @@ The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but only RV32IM
In no particular order:
- Combine individual instruction checks into single ISA check (currently, doing so takes forever even when depth is set to only `20`)
- Parallelize execution of verification tasks to reduce the total time required to run all verification tasks on a multi-core system
## License

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

@ -53,6 +53,7 @@ from ...insns.insn_divu import *
from ...insns.insn_rem import *
from ...insns.insn_remu import *
from collections import namedtuple
from multiprocessing import Process
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem', 'altops'])
@ -124,141 +125,64 @@ class InsnSpec(Elaboratable):
class InsnTestCase(FHDLTestCase):
def verify(self):
print("- Verifying LUI instruction ...")
self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=20)
print("- Verifying AUIPC instruction ...")
self.assertFormal(InsnSpec(InsnAuipc), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=20)
print("- Verifying JAL instruction ...")
self.assertFormal(InsnSpec(InsnJal), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=20)
print("- Verifying JALR instruction ...")
self.assertFormal(InsnSpec(InsnJalr), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=20)
print("- Verifying BEQ instruction ...")
self.assertFormal(InsnSpec(InsnBeq), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=20)
print("- Verifying BNE instruction ...")
self.assertFormal(InsnSpec(InsnBne), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=20)
print("- Verifying BLT instruction ...")
self.assertFormal(InsnSpec(InsnBlt), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=20)
print("- Verifying BGE instruction ...")
self.assertFormal(InsnSpec(InsnBge), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=20)
print("- Verifying BLTU instruction ...")
self.assertFormal(InsnSpec(InsnBltu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=20)
print("- Verifying BGEU instruction ...")
self.assertFormal(InsnSpec(InsnBgeu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=20)
print("- Verifying LB instruction ...")
self.assertFormal(InsnSpec(InsnLb), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=20)
print("- Verifying LH instruction ...")
self.assertFormal(InsnSpec(InsnLh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=20)
print("- Verifying LW instruction ...")
self.assertFormal(InsnSpec(InsnLw), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=20)
print("- Verifying LBU instruction ...")
self.assertFormal(InsnSpec(InsnLbu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=20)
print("- Verifying LHU instruction ...")
self.assertFormal(InsnSpec(InsnLhu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=20)
print("- Verifying SB instruction ...")
self.assertFormal(InsnSpec(InsnSb), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=20)
print("- Verifying SH instruction ...")
self.assertFormal(InsnSpec(InsnSh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=20)
print("- Verifying SW instruction ...")
self.assertFormal(InsnSpec(InsnSw), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=20)
print("- Verifying ADDI instruction ...")
self.assertFormal(InsnSpec(InsnAddi), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=20)
print("- Verifying SLTI instruction ...")
self.assertFormal(InsnSpec(InsnSlti), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=20)
print("- Verifying SLTIU instruction ...")
self.assertFormal(InsnSpec(InsnSltiu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=20)
print("- Verifying XORI instruction ...")
self.assertFormal(InsnSpec(InsnXori), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=20)
print("- Verifying ORI instruction ...")
self.assertFormal(InsnSpec(InsnOri), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=20)
print("- Verifying ANDI instruction ...")
self.assertFormal(InsnSpec(InsnAndi), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=20)
print("- Verifying SLLI instruction ...")
self.assertFormal(InsnSpec(InsnSlli), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=20)
print("- Verifying SRLI instruction ...")
self.assertFormal(InsnSpec(InsnSrli), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=20)
print("- Verifying SRAI instruction ...")
self.assertFormal(InsnSpec(InsnSrai), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=20)
print("- Verifying ADD instruction ...")
self.assertFormal(InsnSpec(InsnAdd), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=20)
print("- Verifying SUB instruction ...")
self.assertFormal(InsnSpec(InsnSub), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=20)
print("- Verifying SLL instruction ...")
self.assertFormal(InsnSpec(InsnSll), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=20)
print("- Verifying SLT instruction ...")
self.assertFormal(InsnSpec(InsnSlt), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=20)
print("- Verifying SLTU instruction ...")
self.assertFormal(InsnSpec(InsnSltu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=20)
print("- Verifying XOR instruction ...")
self.assertFormal(InsnSpec(InsnXor), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=20)
print("- Verifying SRL instruction ...")
self.assertFormal(InsnSpec(InsnSrl), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=20)
print("- Verifying SRA instruction ...")
self.assertFormal(InsnSpec(InsnSra), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=20)
print("- Verifying OR instruction ...")
self.assertFormal(InsnSpec(InsnOr), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=20)
print("- Verifying AND instruction ...")
self.assertFormal(InsnSpec(InsnAnd), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=20)
print("- Verifying MUL instruction ...")
self.assertFormal(InsnSpec(InsnMul), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=20)
print("- Verifying MULH instruction ...")
self.assertFormal(InsnSpec(InsnMulh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=20)
print("- Verifying MULHSU instruction ...")
self.assertFormal(InsnSpec(InsnMulhsu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=20)
print("- Verifying MULHU instruction ...")
self.assertFormal(InsnSpec(InsnMulhu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=20)
print("- Verifying DIV instruction ...")
self.assertFormal(InsnSpec(InsnDiv), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=20)
print("- Verifying DIVU instruction ...")
self.assertFormal(InsnSpec(InsnDivu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=20)
print("- Verifying REM instruction ...")
self.assertFormal(InsnSpec(InsnRem), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=20)
print("- Verifying REMU instruction ...")
self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=20)
def verify_insn(insn_spec, spec_name):
self.assertFormal(InsnSpec(insn_spec), mode="cover", depth=20, spec_name=spec_name)
self.assertFormal(InsnSpec(insn_spec), mode="bmc", depth=20, spec_name=spec_name)
print("%s PASS" % spec_name)
insns = [
(InsnLui, "verify_lui"),
(InsnAuipc, "verify_auipc"),
(InsnJal, "verify_jal"),
(InsnJalr, "verify_jalr"),
(InsnBeq, "verify_beq"),
(InsnBne, "verify_bne"),
(InsnBlt, "verify_blt"),
(InsnBge, "verify_bge"),
(InsnBltu, "verify_bltu"),
(InsnBgeu, "verify_bgeu"),
(InsnLb, "verify_lb"),
(InsnLh, "verify_lh"),
(InsnLw, "verify_lw"),
(InsnLbu, "verify_lbu"),
(InsnLhu, "verify_lhu"),
(InsnSb, "verify_sb"),
(InsnSh, "verify_sh"),
(InsnSw, "verify_sw"),
(InsnAddi, "verify_addi"),
(InsnSlti, "verify_slti"),
(InsnSltiu, "verify_sltiu"),
(InsnXori, "verify_xori"),
(InsnOri, "verify_ori"),
(InsnAndi, "verify_andi"),
(InsnSlli, "verify_slli"),
(InsnSrli, "verify_srli"),
(InsnSrai, "verify_srai"),
(InsnAdd, "verify_add"),
(InsnSub, "verify_sub"),
(InsnSll, "verify_sll"),
(InsnSlt, "verify_slt"),
(InsnSltu, "verify_sltu"),
(InsnXor, "verify_xor"),
(InsnSrl, "verify_srl"),
(InsnSra, "verify_sra"),
(InsnOr, "verify_or"),
(InsnAnd, "verify_and"),
(InsnMul, "verify_mul"),
(InsnMulh, "verify_mulh"),
(InsnMulhsu, "verify_mulhsu"),
(InsnMulhu, "verify_mulhu"),
(InsnDiv, "verify_div"),
(InsnDivu, "verify_divu"),
(InsnRem, "verify_rem"),
(InsnRemu, "verify_remu")
]
ps = []
for insn_spec, spec_name in insns:
p = Process(target=verify_insn, args=(insn_spec,spec_name))
ps.append(p)
p.start()
for p in ps:
p.join()
class PcFwdSpec(Elaboratable):
def elaborate(self, platform):

6
shell.nix
View File

@ -2,10 +2,10 @@ let
pkgs = import <nixpkgs> { };
nmigen-latest = pkgs.python3Packages.nmigen.overrideAttrs(oa: {
src = pkgs.fetchFromGitHub {
owner = "m-labs";
owner = "DonaldKellett";
repo = "nmigen";
rev = "1ad6e3207f02e913407867dddddb8f50fad0ced4";
sha256 = "14vvw1lcfmcf3374wpn3sslgvgcfg18rkbs8x45vycqag6a5zy0b";
rev = "03726c7e3f307f27626bcc7dffe75abe17b2a390";
sha256 = "1b0rjbb6is6nzbcnxrwh5iv4k9xcac0ijq5kp47wdg9rhbnaa5w0";
};
});
minerva-latest = pkgs.python3Packages.buildPythonPackage {