diff --git a/README.md b/README.md
index 0c8a8f2..8a8ebd9 100644
--- a/README.md
+++ b/README.md
@@ -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
 
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index ac1d561..5248325 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -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):
diff --git a/shell.nix b/shell.nix
index 63daa9d..07dd003 100644
--- a/shell.nix
+++ b/shell.nix
@@ -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 {