tests/units_formal: split up tests in hopes of making them run faster

crates/cpu/tests/units_formal.rs

@@ -20,12 +20,13 @@ use cpu::{
 use fayalite::{
     checked_vcd_output,
     firrtl::ExportOptions,
+    intern::Memoize,
     module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind, wire_with_loc},
     prelude::*,
     sim::compiler::Compiled,
     ty::StaticType,
 };
-use std::{cell::OnceCell, collections::BTreeSet, num::NonZero};
+use std::{collections::BTreeSet, num::NonZero, sync::OnceLock};
 
 #[hdl_module]
 fn formal_harness(
@@ -111,119 +112,94 @@ type CheckOutput = DecodeAndRunSingleInsnOutput<
     DecodeOneInsnMaxMOpCount<simple_power_isa::decode_one_insn>,
 >;
 
-struct CaseOutput {
+struct CaseIO {
+    input: Expr<CheckInput>,
+    suffix: Expr<UInt<32>>,
     output: Expr<CheckOutput>,
     read_output_regs: BTreeSet<u32>,
 }
 
-impl CaseOutput {
-    fn reg(&mut self, reg_num: u32) -> Expr<TraceAsString<PRegValue>> {
+impl CaseIO {
+    fn in_reg(&self, reg_num: u32) -> Expr<TraceAsString<PRegValue>> {
+        self.input.regs.regs[reg_num as usize]
+    }
+    fn out_reg(&mut self, reg_num: u32) -> Expr<TraceAsString<PRegValue>> {
         self.read_output_regs.insert(reg_num);
         self.output.regs.regs[reg_num as usize]
     }
 }
 
-type UnprefixedCheckFn = fn(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput);
+type CheckFn = fn(clk: Expr<Clock>, io: &mut CaseIO);
 
-type PrefixedCheckFn =
-    fn(clk: Expr<Clock>, input: Expr<CheckInput>, suffix: Expr<UInt<32>>, output: &mut CaseOutput);
-
-enum Case {
+enum CaseData {
     Unprefixed {
-        asm: &'static str,
         encoded: u32,
         imm_mask: u32,
-        inputs: Vec<u32>,
-        check: UnprefixedCheckFn,
-        source_location: SourceLocation,
     },
     Prefixed {
-        asm: &'static str,
         encoded: (u32, u32),
         imm_mask: (u32, u32),
-        inputs: Vec<u32>,
-        check: PrefixedCheckFn,
-        source_location: SourceLocation,
     },
 }
 
+struct Case {
+    data: CaseData,
+    asm: &'static str,
+    inputs: Vec<u32>,
+    check: CheckFn,
+    source_location: SourceLocation,
+}
+
 impl Case {
-    fn asm(&self) -> &'static str {
-        match *self {
-            Self::Unprefixed { asm, .. } | Self::Prefixed { asm, .. } => asm,
-        }
-    }
     #[track_caller]
     fn mnemonic(&self) -> &'static str {
-        self.asm()
+        self.asm
             .split_whitespace()
             .next()
             .expect("asm should have mnemonic")
     }
-    fn inputs(&self) -> &[u32] {
-        match self {
-            Self::Unprefixed { inputs, .. } | Self::Prefixed { inputs, .. } => inputs,
-        }
-    }
-    fn source_location(&self) -> SourceLocation {
-        match *self {
-            Self::Unprefixed {
-                source_location, ..
-            }
-            | Self::Prefixed {
-                source_location, ..
-            } => source_location,
-        }
-    }
     fn needed_mop_kinds(&self) -> NeededMOpKinds {
-        thread_local! {
-            static COMPILED: OnceCell<Compiled<simple_power_isa::decode_one_insn>> = const { OnceCell::new() };
-        }
-        let compiled = COMPILED.with(|compiled| {
-            *compiled.get_or_init(|| Compiled::new(simple_power_isa::decode_one_insn(())))
-        });
-        let mut sim = Simulation::from_compiled(compiled);
-        const IMM_BITS: u32 = 0xAAAA_AAAA; // something non-zero so we avoid special cases for zero immediates or similar
-        match *self {
-            Self::Unprefixed {
-                asm: _,
-                encoded,
-                imm_mask,
-                inputs: _,
-                check: _,
-                source_location: _,
-            } => {
-                sim.write(sim.io().first_input, encoded | (IMM_BITS & imm_mask));
-                sim.write(sim.io().second_input, HdlNone());
+        #[derive(Clone, Copy, PartialEq, Eq, Hash)]
+        struct MyMemoize;
+        impl Memoize for MyMemoize {
+            type Input = (u32, Option<u32>);
+            type InputOwned = (u32, Option<u32>);
+            type Output = NeededMOpKinds;
+
+            fn inner(self, input: &Self::Input) -> Self::Output {
+                let (first_input, second_input) = *input;
+                static COMPILED: OnceLock<Compiled<simple_power_isa::decode_one_insn>> =
+                    OnceLock::new();
+                let compiled =
+                    *COMPILED.get_or_init(|| Compiled::new(simple_power_isa::decode_one_insn(())));
+                let mut sim = Simulation::from_compiled(compiled);
+                sim.write(sim.io().first_input, first_input);
+                sim.write(sim.io().second_input, second_input);
                 sim.advance_time(SimDuration::from_micros(1));
-                assert!(!sim.read_bool(sim.io().second_input_used));
+                assert_eq!(
+                    sim.read_bool(sim.io().second_input_used),
+                    second_input.is_some(),
+                );
+                assert!(!sim.read_bool(sim.io().is_illegal));
+                let mut retval = NeededMOpKinds::default();
+                for mop in ArrayVec::elements_sim_ref(&sim.read(sim.io().output)) {
+                    retval = retval.or(NeededMOpKinds::new(mop.inner()));
+                }
+                retval
             }
-            Self::Prefixed {
-                asm: _,
+        }
+        const IMM_BITS: u32 = 0xAAAA_AAAA; // something non-zero so we avoid special cases for zero immediates or similar
+        let input = match self.data {
+            CaseData::Unprefixed { encoded, imm_mask } => (encoded | (IMM_BITS & imm_mask), None),
+            CaseData::Prefixed {
                 encoded: (encoded_prefix, encoded_suffix),
                 imm_mask: (imm_mask_prefix, imm_mask_suffix),
-                inputs: _,
-                check: _,
-                source_location: _,
-            } => {
-                sim.write(
-                    sim.io().first_input,
-                    encoded_prefix | (IMM_BITS & imm_mask_prefix),
-                );
-                sim.write(
-                    sim.io().second_input,
-                    HdlSome(encoded_suffix | (IMM_BITS & imm_mask_suffix)),
-                );
-                sim.advance_time(SimDuration::from_micros(1));
-                assert!(sim.read_bool(sim.io().second_input_used));
-            }
-        }
-        assert!(!sim.read_bool(sim.io().is_illegal));
-        let mut retval = NeededMOpKinds::default();
-        for mop in ArrayVec::elements_sim_ref(&sim.read(sim.io().output)) {
-            retval = retval.or(NeededMOpKinds::new(mop.inner()));
-        }
-        retval
+            } => (
+                encoded_prefix | (IMM_BITS & imm_mask_prefix),
+                Some(encoded_suffix | (IMM_BITS & imm_mask_suffix)),
+            ),
+        };
+        MyMemoize.get_owned(input)
     }
 }
 
@@ -327,17 +303,19 @@ impl NeededMOpKinds {
 
 #[derive(Default)]
 struct Cases {
-    mnemonics: BTreeSet<&'static str>,
-    need_mop_kinds: NeededMOpKinds,
     cases: Vec<Case>,
 }
 
 impl Cases {
-    #[track_caller]
-    fn add_maybe_prefixed(&mut self, case: Case) {
-        self.mnemonics.insert(case.mnemonic());
-        self.need_mop_kinds = self.need_mop_kinds.or(case.needed_mop_kinds());
-        self.cases.push(case);
+    fn mnemonics(&self) -> BTreeSet<&'static str> {
+        BTreeSet::from_iter(self.cases.iter().map(|c| c.mnemonic()))
+    }
+    fn needed_mop_kinds(&self) -> NeededMOpKinds {
+        let mut retval = NeededMOpKinds::default();
+        for case in &self.cases {
+            retval = retval.or(case.needed_mop_kinds());
+        }
+        retval
     }
     #[track_caller]
     fn add(
@@ -346,12 +324,11 @@ impl Cases {
         encoded: u32,
         imm_mask: u32,
         inputs: impl AsRef<[u32]>,
-        check: UnprefixedCheckFn,
+        check: CheckFn,
     ) {
-        self.add_maybe_prefixed(Case::Unprefixed {
+        self.cases.push(Case {
+            data: CaseData::Unprefixed { encoded, imm_mask },
             asm,
-            encoded,
-            imm_mask,
             inputs: inputs.as_ref().to_vec(),
             check,
             source_location: SourceLocation::caller(),
@@ -364,17 +341,24 @@ impl Cases {
         encoded: (u32, u32),
         imm_mask: (u32, u32),
         inputs: impl AsRef<[u32]>,
-        check: PrefixedCheckFn,
+        check: CheckFn,
     ) {
-        self.add_maybe_prefixed(Case::Prefixed {
+        self.cases.push(Case {
+            data: CaseData::Prefixed { encoded, imm_mask },
             asm,
-            encoded,
-            imm_mask,
             inputs: inputs.as_ref().to_vec(),
             check,
             source_location: SourceLocation::caller(),
         });
     }
+    fn subdivide(self, subdivision_index: usize, subdivision_count: usize) -> Self {
+        let Self { mut cases } = self;
+        let start_index = (subdivision_index * cases.len()) / subdivision_count;
+        let end_index = ((subdivision_index + 1) * cases.len()) / subdivision_count;
+        cases.truncate(end_index);
+        cases.drain(..start_index);
+        Self { cases }
+    }
 }
 
 #[hdl]
@@ -382,12 +366,12 @@ fn case_check_addi(cases: &mut Cases) {
     let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
     cases.add("addi 3, 4, imm", 0x3864_0000, 0xFFFF, [r4], check_addi);
     #[hdl]
-    fn check_addi(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
+    fn check_addi(clk: Expr<Clock>, io: &mut CaseIO) {
         #[hdl]
         let addi_imm = wire();
-        connect(addi_imm, input.decoder_input.0.cast_to_static::<SInt<16>>());
-        let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
+        connect(addi_imm, io.suffix.cast_to_static::<SInt<16>>());
+        let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
         hdl_assert(
             clk,
             (r4_in + addi_imm.cast_to_static::<UInt<64>>())
@@ -416,22 +400,17 @@ fn case_check_paddi(cases: &mut Cases) {
         check_paddi::<true>,
     );
     #[hdl]
-    fn check_paddi<const R: bool>(
-        clk: Expr<Clock>,
-        input: Expr<CheckInput>,
-        suffix: Expr<UInt<32>>,
-        output: &mut CaseOutput,
-    ) {
+    fn check_paddi<const R: bool>(clk: Expr<Clock>, io: &mut CaseIO) {
         #[hdl]
         let paddi_imm: SInt<34> = wire();
         connect(
             paddi_imm,
-            (suffix[..16] | (input.decoder_input.0[..18] << 16)).cast_to_static::<SInt<34>>(),
+            (io.suffix[..16] | (io.input.decoder_input.0[..18] << 16)).cast_to_static::<SInt<34>>(),
         );
-        let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
+        let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
         let sum = r4_in + paddi_imm.cast_to_static::<UInt<64>>();
-        let sum = if R { sum + input.pc } else { sum };
+        let sum = if R { sum + io.input.pc } else { sum };
         hdl_assert(clk, sum.cast_to_static::<UInt<64>>().cmp_eq(r3_out), "");
     }
 }
@@ -441,15 +420,12 @@ fn case_check_addis(cases: &mut Cases) {
     let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
     cases.add("addis 3, 4, imm", 0x3C64_0000, 0xFFFF, [r4], check_addis);
     #[hdl]
-    fn check_addis(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
+    fn check_addis(clk: Expr<Clock>, io: &mut CaseIO) {
         #[hdl]
         let addis_imm = wire();
-        connect(
-            addis_imm,
-            input.decoder_input.0.cast_to_static::<SInt<16>>(),
-        );
-        let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
+        connect(addis_imm, io.suffix.cast_to_static::<SInt<16>>());
+        let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
         hdl_assert(
             clk,
             (r4_in + (addis_imm << 16).cast_to_static::<UInt<64>>())
@@ -464,35 +440,26 @@ fn case_check_addis(cases: &mut Cases) {
 fn case_check_addpcis(cases: &mut Cases) {
     cases.add("addpcis 3, imm", 0x4C60_0004, 0x1F_FFC1, [], check_addpcis);
     #[hdl]
-    fn check_addpcis(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
+    fn check_addpcis(clk: Expr<Clock>, io: &mut CaseIO) {
         #[hdl]
         let addpcis_d0 = wire();
-        connect(
-            addpcis_d0,
-            input.decoder_input.0[6..].cast_to_static::<UInt<10>>(),
-        );
+        connect(addpcis_d0, io.suffix[6..].cast_to_static::<UInt<10>>());
         #[hdl]
         let addpcis_d1 = wire();
-        connect(
-            addpcis_d1,
-            input.decoder_input.0[16..].cast_to_static::<UInt<5>>(),
-        );
+        connect(addpcis_d1, io.suffix[16..].cast_to_static::<UInt<5>>());
         #[hdl]
         let addpcis_d2 = wire();
-        connect(
-            addpcis_d2,
-            input.decoder_input.0.cast_to_static::<UInt<1>>(),
-        );
+        connect(addpcis_d2, io.suffix.cast_to_static::<UInt<1>>());
         #[hdl]
         let addpcis_d = wire();
         connect(
             addpcis_d,
             (addpcis_d2 + (addpcis_d1 << 1) + (addpcis_d0 << 6)).cast_to_static::<SInt<16>>(),
         );
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
         hdl_assert(
             clk,
-            (input.pc + 4u64 + (addpcis_d << 16).cast_to_static::<UInt<64>>())
+            (io.input.pc + 4u64 + (addpcis_d << 16).cast_to_static::<UInt<64>>())
                 .cast_to_static::<UInt<64>>()
                 .cmp_eq(r3_out),
             "",
@@ -530,21 +497,21 @@ fn case_check_add_addc_adde_subf_subfc_subfe(cases: &mut Cases) {
     cases.add("subfeo  3, 3, 4", 0x7C63_2510, 0, [r3, r4, ca], check);
     cases.add("subfeo. 3, 3, 4", 0x7C63_2511, 0, [r3, r4, ca], check);
     #[hdl]
-    fn check(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
-        let has_ca_out = (input.decoder_input.0 & 0x240u32).cmp_eq(0u32);
-        let oe = (input.decoder_input.0 & 0x400u32).cmp_ne(0u32);
-        let use_ca_in = (input.decoder_input.0 & 0x100u32).cmp_ne(0u32);
-        let is_sub = (input.decoder_input.0 & 0x4u32).cmp_eq(0u32);
-        let rc = (input.decoder_input.0 & 1u32).cmp_ne(0u32);
-        let r3_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp;
-        let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
-        let ca_in = input.regs.regs[MOpRegNum::power_isa_xer_ca_ca32_reg().value];
-        let ov_in = input.regs.regs[MOpRegNum::power_isa_xer_so_ov_ov32_reg().value];
-        let cr0_in = input.regs.regs[MOpRegNum::power_isa_cr_0_reg().value];
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3));
-        let ca_out = output.reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
-        let ov_out = output.reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
-        let cr0_out = output.reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
+    fn check(clk: Expr<Clock>, io: &mut CaseIO) {
+        let has_ca_out = (io.suffix & 0x240u32).cmp_eq(0u32);
+        let oe = (io.suffix & 0x400u32).cmp_ne(0u32);
+        let use_ca_in = (io.suffix & 0x100u32).cmp_ne(0u32);
+        let is_sub = (io.suffix & 0x4u32).cmp_eq(0u32);
+        let rc = (io.suffix & 1u32).cmp_ne(0u32);
+        let r3_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
+        let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
+        let ca_in = io.in_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
+        let ov_in = io.in_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
+        let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
+        let ca_out = io.out_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
+        let ov_out = io.out_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
+        let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
         #[hdl]
         let add_sub_add_in0 = wire();
         connect(add_sub_add_in0, r3_in);
@@ -633,20 +600,17 @@ fn case_check_addic_subfic(cases: &mut Cases) {
     cases.add("addic. 3, 4, imm", 0x3464_0000, 0xFFFF, [r4], check);
     cases.add("subfic 3, 4, imm", 0x2064_0000, 0xFFFF, [r4], check);
     #[hdl]
-    fn check(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
-        let rc = (input.decoder_input.0 & 0x400_0000u32).cmp_ne(0u32);
-        let is_sub = (input.decoder_input.0 & 0x1000_0000u32).cmp_eq(0u32);
-        let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
-        let cr0_in = input.regs.regs[MOpRegNum::power_isa_cr_0_reg().value];
-        let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3));
-        let ca_out = output.reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
-        let cr0_out = output.reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
+    fn check(clk: Expr<Clock>, io: &mut CaseIO) {
+        let rc = (io.suffix & 0x400_0000u32).cmp_ne(0u32);
+        let is_sub = (io.suffix & 0x1000_0000u32).cmp_eq(0u32);
+        let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
+        let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
+        let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
+        let ca_out = io.out_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
+        let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
         #[hdl]
         let addic_subfic_imm = wire();
-        connect(
-            addic_subfic_imm,
-            input.decoder_input.0.cast_to_static::<SInt<16>>(),
-        );
+        connect(addic_subfic_imm, io.suffix.cast_to_static::<SInt<16>>());
         #[hdl]
         let addic_subfic_in = wire();
         connect(addic_subfic_in, r4_in);
@@ -785,12 +749,14 @@ fn check_power_isa_alu_formal(
             rst: formal_reset().to_reset(),
         },
     );
+    let mnemonics = cases.mnemonics();
+    let needed_mop_kinds = cases.needed_mop_kinds();
     #[hdl]
     let harness = instance(formal_harness(
         config,
-        |args: &DecodeFilterArgs<'_>| cases.mnemonics.contains(&args.mnemonic()),
+        |args: &DecodeFilterArgs<'_>| mnemonics.contains(&args.mnemonic()),
         &mut |mop: &SimValue<_>| -> bool {
-            cases.need_mop_kinds == cases.need_mop_kinds.or(NeededMOpKinds::new(mop))
+            needed_mop_kinds == needed_mop_kinds.or(NeededMOpKinds::new(mop))
         },
     ));
     connect(harness.cd, cd);
@@ -842,19 +808,12 @@ fn check_power_isa_alu_formal(
     let matched_cases = Vec::from_iter(cases.cases.iter().map(|case| {
         let matched_case = wire_with_loc(
             &format!("matched_case_{}", case.mnemonic()),
-            case.source_location(),
+            case.source_location,
             Bool,
         );
         connect(matched_case, false);
-        match *case {
-            Case::Unprefixed {
-                asm: _,
-                encoded,
-                imm_mask,
-                check: _,
-                inputs: _,
-                source_location: _,
-            } => {
+        match case.data {
+            CaseData::Unprefixed { encoded, imm_mask } => {
                 #[hdl]
                 if !decoder_has_second_word_any_const
                     & (decoder_first_word & !imm_mask).cmp_eq(encoded)
@@ -864,13 +823,9 @@ fn check_power_isa_alu_formal(
                     hdl_assume(cd.clk, predicted_next_pc.cmp_eq(pc + 0x4u8), "");
                 }
             }
-            Case::Prefixed {
-                asm: _,
+            CaseData::Prefixed {
                 encoded: (encoded_prefix, encoded_suffix),
                 imm_mask: (imm_mask_prefix, imm_mask_suffix),
-                inputs: _,
-                check: _,
-                source_location: _,
             } => {
                 #[hdl]
                 if decoder_has_second_word_any_const
@@ -946,36 +901,27 @@ fn check_power_isa_alu_formal(
         for (case, &matched_case) in cases.cases.iter().zip(&matched_cases) {
             #[hdl]
             if matched_case {
-                let mut case_output = CaseOutput {
+                let input = harness.input;
+                let suffix = match case.data {
+                    CaseData::Unprefixed { .. } => input.decoder_input.0,
+                    CaseData::Prefixed { .. } => decoder_second_word_any_const,
+                };
+                let mut case_io = CaseIO {
+                    input,
+                    suffix,
                     output,
                     read_output_regs: BTreeSet::new(),
                 };
-                match *case {
-                    Case::Unprefixed {
-                        asm: _,
-                        encoded: _,
-                        imm_mask: _,
-                        inputs: _,
-                        check,
-                        source_location: _,
-                    } => check(cd.clk, harness.input, &mut case_output),
-                    Case::Prefixed {
-                        asm: _,
-                        encoded: _,
-                        imm_mask: _,
-                        inputs: _,
-                        check,
-                        source_location: _,
-                    } => check(
-                        cd.clk,
-                        harness.input,
-                        decoder_second_word_any_const,
-                        &mut case_output,
-                    ),
-                }
+                (case.check)(cd.clk, &mut case_io);
+                let CaseIO {
+                    input: _,
+                    suffix: _,
+                    output: _,
+                    read_output_regs,
+                } = case_io;
                 for (reg_index, output_reg) in output_regs.regs.into_iter().enumerate() {
                     let reg_num = reg_index as u32;
-                    if case_output.read_output_regs.contains(&reg_num) {
+                    if read_output_regs.contains(&reg_num) {
                         continue;
                     }
                     hdl_assert(cd.clk, output_reg.cmp_eq(input_regs.regs[reg_index]), "");
@@ -985,15 +931,18 @@ fn check_power_isa_alu_formal(
     }
 }
 
-#[test]
-fn test_power_isa_add_sub_formal() {
+fn test_power_isa_add_sub_formal(subdivision_index: usize, subdivision_count: usize) {
     let config = PhantomConst::new_sized(CpuConfig::new(
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let m = check_power_isa_alu_formal(config, &cases_add_sub(), None);
+    let m = check_power_isa_alu_formal(
+        config,
+        &cases_add_sub().subdivide(subdivision_index, subdivision_count),
+        None,
+    );
     assert_formal(
-        "test_power_isa_add_sub_formal",
+        format_args!("test_power_isa_add_sub_formal_{subdivision_index}"),
         m,
         FormalMode::BMC,
         7,
@@ -1005,6 +954,36 @@ fn test_power_isa_add_sub_formal() {
     );
 }
 
+#[test]
+fn test_power_isa_add_sub_formal_0() {
+    test_power_isa_add_sub_formal(0, 6);
+}
+
+#[test]
+fn test_power_isa_add_sub_formal_1() {
+    test_power_isa_add_sub_formal(1, 6);
+}
+
+#[test]
+fn test_power_isa_add_sub_formal_2() {
+    test_power_isa_add_sub_formal(2, 6);
+}
+
+#[test]
+fn test_power_isa_add_sub_formal_3() {
+    test_power_isa_add_sub_formal(3, 6);
+}
+
+#[test]
+fn test_power_isa_add_sub_formal_4() {
+    test_power_isa_add_sub_formal(4, 6);
+}
+
+#[test]
+fn test_power_isa_add_sub_formal_5() {
+    test_power_isa_add_sub_formal(5, 6);
+}
+
 #[hdl]
 fn test_power_isa_alu_sim(
     cases: Cases,
@@ -1037,18 +1016,18 @@ fn test_power_isa_alu_sim(
     const IMM_S34_VALUES: &[i64] = &[0, 1, -1, S34_MAX, S34_MIN];
     const PC: u64 = 0x1000;
     for case in &cases.cases {
-        let r3_values = if case.inputs().contains(&MOpRegNum::power_isa_gpr_reg_num(3)) {
+        let r3_values = if case.inputs.contains(&MOpRegNum::power_isa_gpr_reg_num(3)) {
             REG_VALUES
         } else {
             &[0]
         };
-        let r4_values = if case.inputs().contains(&MOpRegNum::power_isa_gpr_reg_num(4)) {
+        let r4_values = if case.inputs.contains(&MOpRegNum::power_isa_gpr_reg_num(4)) {
             REG_VALUES
         } else {
             &[0]
         };
         let ca_values: &[bool] = if case
-            .inputs()
+            .inputs
             .contains(&MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM)
         {
             &[false, true]
@@ -1060,8 +1039,8 @@ fn test_power_isa_alu_sim(
                 for &ca in ca_values {
                     let mut imm_index = 0;
                     loop {
-                        let asm = case.asm();
-                        let source_location = case.source_location();
+                        let asm = case.asm;
+                        let source_location = case.source_location;
                         println!(
                             "\ncase: {asm}\n\
                             r3={r3:#x} r4={r4:#x} ca={ca}\n\
@@ -1072,15 +1051,8 @@ fn test_power_isa_alu_sim(
                         sim.write(ca_any_const, ca);
                         sim.write(pc_any_const, PC);
                         let imm_count;
-                        match *case {
-                            Case::Unprefixed {
-                                asm: _,
-                                encoded,
-                                imm_mask,
-                                inputs: _,
-                                check: _,
-                                source_location: _,
-                            } => {
+                        match case.data {
+                            CaseData::Unprefixed { encoded, imm_mask } => {
                                 sim.write(predicted_next_pc_any_const, PC + 4);
                                 let imm = IMM_S16_VALUES[imm_index] as i64;
                                 if imm_mask == 0 {
@@ -1100,13 +1072,9 @@ fn test_power_isa_alu_sim(
                                 sim.write(decoder_has_second_word_any_const, false);
                                 sim.write(decoder_second_word_any_const, 0u32);
                             }
-                            Case::Prefixed {
-                                asm: _,
+                            CaseData::Prefixed {
                                 encoded: (encoded_prefix, encoded_suffix),
                                 imm_mask: (imm_mask_prefix, imm_mask_suffix),
-                                inputs: _,
-                                check: _,
-                                source_location: _,
                             } => {
                                 sim.write(predicted_next_pc_any_const, PC + 8);
                                 let imm = IMM_S34_VALUES[imm_index];
@@ -1155,9 +1123,62 @@ fn test_power_isa_alu_sim(
 }
 
 #[test]
-fn test_power_isa_add_sub_sim() {
-    test_power_isa_alu_sim(cases_add_sub(), |sim| {
-        checked_vcd_output!(sim, "tests/expected/units_formal_power_isa_add_sub_sim.vcd")
+fn test_power_isa_add_sub_sim_0() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(0, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_0.vcd"
+        )
+    });
+}
+
+#[test]
+fn test_power_isa_add_sub_sim_1() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(1, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_1.vcd"
+        )
+    });
+}
+
+#[test]
+fn test_power_isa_add_sub_sim_2() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(2, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_2.vcd"
+        )
+    });
+}
+
+#[test]
+fn test_power_isa_add_sub_sim_3() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(3, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_3.vcd"
+        )
+    });
+}
+
+#[test]
+fn test_power_isa_add_sub_sim_4() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(4, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_4.vcd"
+        )
+    });
+}
+
+#[test]
+fn test_power_isa_add_sub_sim_5() {
+    test_power_isa_alu_sim(cases_add_sub().subdivide(5, 6), |sim| {
+        checked_vcd_output!(
+            sim,
+            "tests/expected/units_formal_power_isa_add_sub_sim_5.vcd"
+        )
     });
 }