tests/units_formal: prove more addition instructions -- [p]addi and add[c][o][.]

crates/cpu/tests/units_formal.rs

@@ -19,11 +19,12 @@ use cpu::{
 };
 use fayalite::{
     firrtl::ExportOptions,
-    module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind},
+    module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind, wire_with_loc},
     prelude::*,
+    sim::compiler::Compiled,
     ty::StaticType,
 };
-use std::num::NonZero;
+use std::{cell::OnceCell, collections::BTreeSet, num::NonZero};
 
 #[hdl_module]
 fn formal_harness(
@@ -99,27 +100,483 @@ fn formal_harness(
     hdl_assert(cd.clk, !decode_and_run.error, "");
 }
 
-#[derive(Copy, Clone)]
-struct R3R4AnyConst {
-    r3_any_const: Expr<UInt<64>>,
-    r4_any_const: Expr<UInt<64>>,
+#[hdl(no_runtime_generics)]
+type CheckInput =
+    DecodeAndRunSingleInsnInput<PhantomConst<CpuConfig>, (UInt<32>, HdlOption<UInt<32>>)>;
+
+#[hdl(no_runtime_generics)]
+type CheckOutput = DecodeAndRunSingleInsnOutput<
+    PhantomConst<CpuConfig>,
+    DecodeOneInsnMaxMOpCount<simple_power_isa::decode_one_insn>,
+>;
+
+struct CaseOutput {
+    output: Expr<CheckOutput>,
+    read_output_regs: BTreeSet<u32>,
 }
 
-impl R3R4AnyConst {
+impl CaseOutput {
+    fn 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 PrefixedCheckFn =
+    fn(clk: Expr<Clock>, input: Expr<CheckInput>, suffix: Expr<UInt<32>>, output: &mut CaseOutput);
+
+enum Case {
+    Unprefixed {
+        asm: &'static str,
+        encoded: u32,
+        imm_mask: u32,
+        check: UnprefixedCheckFn,
+        source_location: SourceLocation,
+    },
+    Prefixed {
+        asm: &'static str,
+        encoded: (u32, u32),
+        imm_mask: (u32, u32),
+        check: PrefixedCheckFn,
+        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()
+            .split_whitespace()
+            .next()
+            .expect("asm should have mnemonic")
+    }
+    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,
+                check: _,
+                source_location: _,
+            } => {
+                sim.write(sim.io().first_input, encoded | (IMM_BITS & imm_mask));
+                sim.write(sim.io().second_input, HdlNone());
+                sim.advance_time(SimDuration::from_micros(1));
+                assert!(!sim.read_bool(sim.io().second_input_used));
+            }
+            Self::Prefixed {
+                asm: _,
+                encoded: (encoded_prefix, encoded_suffix),
+                imm_mask: (imm_mask_prefix, imm_mask_suffix),
+                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
+    }
+}
+
+#[derive(Copy, Clone, PartialEq, Eq, Debug, Default)]
+struct NeededMOpKinds {
+    need_add_sub: bool,
+    need_add_sub_i: bool,
+    need_logical_flags: bool,
+    need_logical: bool,
+    need_logical_i: bool,
+    need_shift_rotate: bool,
+    need_compare: bool,
+    need_compare_i: bool,
+    need_branch: bool,
+    need_branch_i: bool,
+    need_read_special: bool,
+}
+
+impl NeededMOpKinds {
+    fn or(self, other: Self) -> Self {
+        Self {
+            need_add_sub: self.need_add_sub | other.need_add_sub,
+            need_add_sub_i: self.need_add_sub_i | other.need_add_sub_i,
+            need_logical_flags: self.need_logical_flags | other.need_logical_flags,
+            need_logical: self.need_logical | other.need_logical,
+            need_logical_i: self.need_logical_i | other.need_logical_i,
+            need_shift_rotate: self.need_shift_rotate | other.need_shift_rotate,
+            need_compare: self.need_compare | other.need_compare,
+            need_compare_i: self.need_compare_i | other.need_compare_i,
+            need_branch: self.need_branch | other.need_branch,
+            need_branch_i: self.need_branch_i | other.need_branch_i,
+            need_read_special: self.need_read_special | other.need_read_special,
+        }
+    }
+    #[hdl]
+    fn new(mop: &SimValue<UnitMOp<impl Type, impl Type, impl Type>>) -> Self {
+        #[hdl(sim)]
+        match mop {
+            UnitMOp::<_, _, _>::AluBranch(mop) =>
+            {
+                #[hdl(sim)]
+                match mop {
+                    AluBranchMOp::<_, _>::AddSub(_) => Self {
+                        need_add_sub: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::AddSubI(_) => Self {
+                        need_add_sub_i: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::LogicalFlags(_) => Self {
+                        need_logical_flags: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::Logical(_) => Self {
+                        need_logical: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::LogicalI(_) => Self {
+                        need_logical_i: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::ShiftRotate(_) => Self {
+                        need_shift_rotate: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::Compare(_) => Self {
+                        need_compare: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::CompareI(_) => Self {
+                        need_compare_i: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::Branch(_) => Self {
+                        need_branch: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::BranchI(_) => Self {
+                        need_branch_i: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::ReadSpecial(_) => Self {
+                        need_read_special: true,
+                        ..Self::default()
+                    },
+                    AluBranchMOp::<_, _>::Unknown => unreachable!(),
+                }
+            }
+            UnitMOp::<_, _, _>::TransformedMove(_) => {
+                // removed by rename stage
+                Self::default()
+            }
+            UnitMOp::<_, _, _>::LoadStore(mop) => {
+                todo!("{mop:?}")
+            }
+            UnitMOp::<_, _, _>::Unknown => unreachable!(),
+        }
+    }
+}
+
+#[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);
+    }
+    #[track_caller]
+    fn add(&mut self, asm: &'static str, encoded: u32, imm_mask: u32, check: UnprefixedCheckFn) {
+        self.add_maybe_prefixed(Case::Unprefixed {
+            asm,
+            encoded,
+            imm_mask,
+            check,
+            source_location: SourceLocation::caller(),
+        });
+    }
+    #[track_caller]
+    fn add_prefixed(
+        &mut self,
+        asm: &'static str,
+        encoded: (u32, u32),
+        imm_mask: (u32, u32),
+        check: PrefixedCheckFn,
+    ) {
+        self.add_maybe_prefixed(Case::Prefixed {
+            asm,
+            encoded,
+            imm_mask,
+            check,
+            source_location: SourceLocation::caller(),
+        });
+    }
+}
+
+#[hdl]
+fn case_check_addi(cases: &mut Cases) {
+    cases.add("addi 3, 4, imm", 0x3864_0000, 0xFFFF, check_addi);
+    #[hdl]
+    fn check_addi(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
+        #[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;
+        hdl_assert(
+            clk,
+            (r4_in + addi_imm.cast_to_static::<UInt<64>>())
+                .cast_to_static::<UInt<64>>()
+                .cmp_eq(r3_out),
+            "",
+        );
+    }
+}
+
+#[hdl]
+fn case_check_paddi(cases: &mut Cases) {
+    cases.add_prefixed(
+        "paddi 3, 4, imm, 0",
+        (0x0600_0000, 0x3864_0000),
+        (0x0003_FFFF, 0x0000_FFFF),
+        check_paddi::<false>,
+    );
+    cases.add_prefixed(
+        "paddi 3, 4, imm, 1",
+        (0x0610_0000, 0x3864_0000),
+        (0x0003_FFFF, 0x0000_FFFF),
+        check_paddi::<true>,
+    );
+    #[hdl]
+    fn check_paddi<const R: bool>(
+        clk: Expr<Clock>,
+        input: Expr<CheckInput>,
+        suffix: Expr<UInt<32>>,
+        output: &mut CaseOutput,
+    ) {
+        #[hdl]
+        let paddi_imm: SInt<34> = wire();
+        connect(
+            paddi_imm,
+            (suffix[..16] | (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 sum = r4_in + paddi_imm.cast_to_static::<UInt<64>>();
+        let sum = if R { sum + input.pc } else { sum };
+        hdl_assert(clk, sum.cast_to_static::<UInt<64>>().cmp_eq(r3_out), "");
+    }
+}
+
+#[hdl]
+fn case_check_add_addc(cases: &mut Cases) {
+    cases.add("add    3, 3, 4", 0x7C63_2214, 0, check_add);
+    cases.add("add.   3, 3, 4", 0x7C63_2215, 0, check_add);
+    cases.add("addo   3, 3, 4", 0x7C63_2614, 0, check_add);
+    cases.add("addo.  3, 3, 4", 0x7C63_2615, 0, check_add);
+    cases.add("addc   3, 3, 4", 0x7C63_2014, 0, check_add);
+    cases.add("addc.  3, 3, 4", 0x7C63_2015, 0, check_add);
+    cases.add("addco  3, 3, 4", 0x7C63_2414, 0, check_add);
+    cases.add("addco. 3, 3, 4", 0x7C63_2415, 0, check_add);
+    #[hdl]
+    fn check_add(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
+        let is_addc = (input.decoder_input.0 & 0x200u32).cmp_eq(0u32);
+        let oe = (input.decoder_input.0 & 0x400u32).cmp_ne(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);
+        #[hdl]
+        let add_expected_out = wire(r3_out.ty());
+        connect_any(add_expected_out.int_fp, r3_in + r4_in);
+        let PRegFlagsPowerISAView {
+            unused: _,
+            xer_ca,
+            xer_ca32,
+            xer_ov,
+            xer_ov32,
+            cr_lt,
+            cr_gt,
+            cr_eq,
+            so,
+            ..
+        } = PRegFlags::view::<PRegFlagsPowerISA>(add_expected_out.flags);
+        let r3_s = r3_in.cast_to_static::<SInt<64>>();
+        let r4_s = r4_in.cast_to_static::<SInt<64>>();
+        let u64_sum = r3_in + r4_in;
+        let s64_sum = r3_s + r4_s;
+        let u32_sum = r3_in.cast_to(UInt[32]) + r4_in.cast_to(UInt[32]);
+        let s32_sum = r3_in.cast_to(SInt[32]) + r4_in.cast_to(SInt[32]);
+        let sum_as_s64 = u64_sum.cast_to(SInt[64]);
+        connect(xer_ca, u64_sum[64]);
+        connect(xer_ca32, u32_sum[32]);
+        connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
+        connect(
+            xer_ov32,
+            s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
+        );
+        connect(cr_gt, sum_as_s64.cmp_gt(0i64));
+        connect(cr_lt, sum_as_s64.cmp_lt(0i64));
+        connect(cr_eq, sum_as_s64.cmp_eq(0i64));
+        connect(so, xer_ov); // TODO: also propagate from input SO
+
+        #[hdl]
+        if is_addc {
+            hdl_assert(clk, add_expected_out.cmp_eq(ca_out), "");
+        } else {
+            hdl_assert(clk, ca_in.cmp_eq(ca_out), "");
+        }
+
+        #[hdl]
+        if oe {
+            hdl_assert(clk, add_expected_out.cmp_eq(ov_out), "");
+        } else {
+            hdl_assert(clk, ov_in.cmp_eq(ov_out), "");
+        }
+
+        #[hdl]
+        if rc {
+            hdl_assert(clk, add_expected_out.cmp_eq(cr0_out), "");
+        } else {
+            hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
+        }
+    }
+}
+
+fn cases_add_sub() -> Cases {
+    let mut cases = Cases::default();
+    case_check_addi(&mut cases);
+    case_check_paddi(&mut cases);
+    // TODO: "addis"
+    // TODO: "addpcis"
+    case_check_add_addc(&mut cases);
+    // TODO: "addic"
+    // TODO: "addic."
+    // TODO: "subf"
+    // TODO: "subf."
+    // TODO: "subfo"
+    // TODO: "subfo."
+    // TODO: "subfic"
+    // TODO: "subfc"
+    // TODO: "subfc."
+    // TODO: "subfco"
+    // TODO: "subfco."
+    // TODO: "adde"
+    // TODO: "adde."
+    // TODO: "addeo"
+    // TODO: "addeo."
+    // TODO: "subfe"
+    // TODO: "subfe."
+    // TODO: "subfeo"
+    // TODO: "subfeo."
+    // TODO: "addme"
+    // TODO: "addme."
+    // TODO: "addmeo"
+    // TODO: "addmeo."
+    // TODO: "addze"
+    // TODO: "addze."
+    // TODO: "addzeo"
+    // TODO: "addzeo."
+    // TODO: "subfme"
+    // TODO: "subfme."
+    // TODO: "subfmeo"
+    // TODO: "subfmeo."
+    // TODO: "subfze"
+    // TODO: "subfze."
+    // TODO: "subfzeo"
+    // TODO: "subfzeo."
+    // TODO: "addex"
+    // TODO: "neg"
+    // TODO: "neg."
+    // TODO: "nego"
+    // TODO: "nego."
+    cases
+}
+
+#[derive(Copy, Clone)]
+struct AnyConsts {
+    decoder_first_word_any_const: Expr<UInt<32>>,
+    decoder_has_second_word_any_const: Expr<Bool>,
+    decoder_second_word_any_const: Expr<UInt<32>>,
+    r3_any_const: Expr<UInt<64>>,
+    r4_any_const: Expr<UInt<64>>,
+    pc_any_const: Expr<UInt<64>>,
+    predicted_next_pc_any_const: Expr<UInt<64>>,
+}
+
+impl AnyConsts {
     #[track_caller]
     fn new() -> Self {
         Self {
+            decoder_first_word_any_const: any_const(StaticType::TYPE),
+            decoder_has_second_word_any_const: any_const(StaticType::TYPE),
+            decoder_second_word_any_const: any_const(StaticType::TYPE),
             r3_any_const: any_const(StaticType::TYPE),
             r4_any_const: any_const(StaticType::TYPE),
+            pc_any_const: any_const(StaticType::TYPE),
+            predicted_next_pc_any_const: any_const(StaticType::TYPE),
         }
     }
 }
 
 #[hdl_module]
-fn check_power_isa_add_formal(
+fn check_power_isa_alu_formal(
     config: PhantomConst<CpuConfig>,
-    r3_r4_any_const: Option<R3R4AnyConst>,
+    cases: Cases,
+    any_consts: Option<AnyConsts>,
 ) {
+    #[hdl]
+    let ran: Bool = m.output();
     #[hdl]
     let cd = wire();
     connect(
@@ -133,26 +590,13 @@ fn check_power_isa_add_formal(
     #[hdl]
     let harness = instance(formal_harness(
         config,
-        |args: &DecodeFilterArgs<'_>| args.mnemonic() == "add",
+        |args: &DecodeFilterArgs<'_>| cases.mnemonics.contains(&args.mnemonic()),
         &mut |mop: &SimValue<_>| -> bool {
-            #[hdl(sim)]
-            match mop {
-                UnitMOp::<_, _, _>::AluBranch(mop) =>
-                {
-                    #[hdl(sim)]
-                    match mop {
-                        AluBranchMOp::<_, _>::AddSub(_) => true,
-                        _ => false,
-                    }
-                }
-                _ => false,
-            }
+            cases.need_mop_kinds == cases.need_mop_kinds.or(NeededMOpKinds::new(mop))
         },
     ));
     connect(harness.cd, cd);
     #[hdl]
-    let ran: Bool = m.output();
-    #[hdl]
     let ran_reg = reg_builder().clock_domain(cd).reset(false);
     connect(ran, ran_reg);
     #[hdl]
@@ -162,6 +606,15 @@ fn check_power_isa_add_formal(
     if cycle_count.cmp_ge(5u32) {
         hdl_assert(cd.clk, ran, "");
     }
+    let AnyConsts {
+        decoder_first_word_any_const,
+        decoder_has_second_word_any_const,
+        decoder_second_word_any_const,
+        r3_any_const,
+        r4_any_const,
+        pc_any_const,
+        predicted_next_pc_any_const,
+    } = any_consts.unwrap_or_else(|| AnyConsts::new());
     #[hdl]
     let DecodeAndRunSingleInsnInput::<_, _> {
         decoder_input,
@@ -172,12 +625,66 @@ fn check_power_isa_add_formal(
         regs: input_regs,
         config: _,
     } = harness.input;
-    // add r3, r3, r4
-    connect(decoder_input, (0x7c632214_u32, HdlNone()));
+    #[hdl]
+    let (decoder_first_word, decoder_second_word) = decoder_input;
+    connect(decoder_first_word, decoder_first_word_any_const);
+    connect(decoder_second_word, HdlNone());
+    #[hdl]
+    if decoder_has_second_word_any_const {
+        connect(decoder_second_word, HdlSome(decoder_second_word_any_const));
+    }
     connect(fetch_block_id, 0u8);
     connect(first_id, 0u16);
-    connect(pc, 0x1000_u64);
-    connect(predicted_next_pc, 0x1004_u64);
+    connect(pc, pc_any_const);
+    connect(predicted_next_pc, predicted_next_pc_any_const);
+    #[hdl]
+    let matched_any_case = wire();
+    connect(matched_any_case, false);
+    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(),
+            Bool,
+        );
+        connect(matched_case, false);
+        match *case {
+            Case::Unprefixed {
+                asm: _,
+                encoded,
+                imm_mask,
+                check: _,
+                source_location: _,
+            } => {
+                #[hdl]
+                if !decoder_has_second_word_any_const
+                    & (decoder_first_word & !imm_mask).cmp_eq(encoded)
+                {
+                    connect(matched_any_case, true);
+                    connect(matched_case, true);
+                    hdl_assume(cd.clk, predicted_next_pc.cmp_eq(pc + 0x4u8), "");
+                }
+            }
+            Case::Prefixed {
+                asm: _,
+                encoded: (encoded_prefix, encoded_suffix),
+                imm_mask: (imm_mask_prefix, imm_mask_suffix),
+                check: _,
+                source_location: _,
+            } => {
+                #[hdl]
+                if decoder_has_second_word_any_const
+                    & (decoder_first_word & !imm_mask_prefix).cmp_eq(encoded_prefix)
+                    & (decoder_second_word_any_const & !imm_mask_suffix).cmp_eq(encoded_suffix)
+                {
+                    connect(matched_any_case, true);
+                    connect(matched_case, true);
+                    hdl_assume(cd.clk, predicted_next_pc.cmp_eq(pc + 0x8u8), "");
+                }
+            }
+        }
+        matched_case
+    }));
+    hdl_assume(cd.clk, matched_any_case, "");
     connect(
         input_regs.regs,
         repeat(
@@ -185,10 +692,6 @@ fn check_power_isa_add_formal(
             1 << MOpRegNum::WIDTH,
         ),
     );
-    let R3R4AnyConst {
-        r3_any_const,
-        r4_any_const,
-    } = r3_r4_any_const.unwrap_or_else(|| R3R4AnyConst::new());
     #[hdl]
     let input_r3 = wire();
     connect(input_r3, r3_any_const);
@@ -203,12 +706,18 @@ fn check_power_isa_add_formal(
         input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp,
         input_r4,
     );
+    // a copy of the output so you can see the signal values in formal proof error traces
+    #[hdl]
+    let output_reg = reg_builder()
+        .clock_domain(cd)
+        .no_reset(harness.ty().output.HdlSome);
     #[hdl]
     if let HdlSome(output) = harness.output {
         connect(ran_reg, true);
+        connect(output_reg, output);
         #[hdl]
         let DecodeAndRunSingleInsnOutput::<_, _> {
-            regs,
+            regs: output_regs,
             cancel_and_start_at,
             retired_insns,
             config: _,
@@ -223,59 +732,55 @@ fn check_power_isa_add_formal(
         } = retired_insns[0];
         hdl_assert(cd.clk, call_stack_op.cmp_eq(CallStackOp.None()), "");
         hdl_assert(cd.clk, cond_br_taken.cmp_eq(HdlNone()), "");
-        #[hdl]
-        let expected_regs = wire(regs.ty());
-        for (reg_index, expected) in expected_regs.regs.into_iter().enumerate() {
-            let reg_num = reg_index as u32;
-            if reg_num == MOpRegNum::power_isa_gpr_reg_num(3) {
-                connect(expected.int_fp, (input_r3 + input_r4).cast_to_static());
-                let PRegFlagsPowerISAView {
-                    unused: _,
-                    xer_ca,
-                    xer_ca32,
-                    xer_ov,
-                    xer_ov32,
-                    cr_lt,
-                    cr_gt,
-                    cr_eq,
-                    so,
-                    ..
-                } = PRegFlags::view::<PRegFlagsPowerISA>(expected.flags);
-                let input_r3_s = input_r3.cast_to_static::<SInt<64>>();
-                let input_r4_s = input_r4.cast_to_static::<SInt<64>>();
-                let u64_sum = input_r3 + input_r4;
-                let s64_sum = input_r3_s + input_r4_s;
-                let u32_sum = input_r3.cast_to(UInt[32]) + input_r4.cast_to(UInt[32]);
-                let s32_sum = input_r3.cast_to(SInt[32]) + input_r4.cast_to(SInt[32]);
-                let sum_as_s64 = u64_sum.cast_to(SInt[64]);
-                connect(xer_ca, u64_sum[64]);
-                connect(xer_ca32, u32_sum[32]);
-                connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
-                connect(
-                    xer_ov32,
-                    s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
-                );
-                connect(cr_gt, sum_as_s64.cmp_gt(0i64));
-                connect(cr_lt, sum_as_s64.cmp_lt(0i64));
-                connect(cr_eq, sum_as_s64.cmp_eq(0i64));
-                connect(so, xer_ov); // TODO: also propagate from input SO
-            } else {
-                connect(expected, input_regs.regs[reg_index]);
+        for (case, &matched_case) in cases.cases.iter().zip(&matched_cases) {
+            #[hdl]
+            if matched_case {
+                let mut case_output = CaseOutput {
+                    output,
+                    read_output_regs: BTreeSet::new(),
+                };
+                match *case {
+                    Case::Unprefixed {
+                        asm: _,
+                        encoded: _,
+                        imm_mask: _,
+                        check,
+                        source_location: _,
+                    } => check(cd.clk, harness.input, &mut case_output),
+                    Case::Prefixed {
+                        asm: _,
+                        encoded: _,
+                        imm_mask: _,
+                        check,
+                        source_location: _,
+                    } => check(
+                        cd.clk,
+                        harness.input,
+                        decoder_second_word_any_const,
+                        &mut case_output,
+                    ),
+                }
+                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) {
+                        continue;
+                    }
+                    hdl_assert(cd.clk, output_reg.cmp_eq(input_regs.regs[reg_index]), "");
+                }
             }
         }
-        hdl_assert(cd.clk, expected_regs.cmp_eq(regs), "");
     }
 }
 
 #[test]
-fn test_power_isa_add_formal() {
+fn test_power_isa_add_sub_formal() {
     let config = PhantomConst::new_sized(CpuConfig::new(
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let m = check_power_isa_add_formal(config, None);
+    let m = check_power_isa_alu_formal(config, cases_add_sub(), None);
     assert_formal(
-        "test_power_isa_add_formal",
+        "test_power_isa_add_sub_formal",
         m,
         FormalMode::BMC,
         7,
@@ -294,15 +799,74 @@ fn test_power_isa_add_sim() {
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let r3_r4_any_const = R3R4AnyConst::new();
-    let m = check_power_isa_add_formal(config, Some(r3_r4_any_const));
+    let any_consts = AnyConsts::new();
+    let m = check_power_isa_alu_formal(config, cases_add_sub(), Some(any_consts));
     let mut sim = Simulation::new(m);
     let _checked_vcd_output = cpu::checked_vcd_output!(
         &mut sim,
         "tests/expected/units_formal_power_isa_add_sim.vcd",
     );
-    sim.write(r3_r4_any_const.r3_any_const, 0x1234u64);
-    sim.write(r3_r4_any_const.r4_any_const, 0x2345u64);
+    let AnyConsts {
+        decoder_first_word_any_const,
+        decoder_has_second_word_any_const,
+        decoder_second_word_any_const,
+        r3_any_const,
+        r4_any_const,
+        pc_any_const,
+        predicted_next_pc_any_const,
+    } = any_consts;
+    sim.write(decoder_first_word_any_const, 0x7C63_2214u32); // add 3, 3, 4
+    sim.write(decoder_has_second_word_any_const, false);
+    sim.write(decoder_second_word_any_const, 0u32);
+    sim.write(r3_any_const, 0x1234u64);
+    sim.write(r4_any_const, 0x1234u64);
+    sim.write(pc_any_const, 0x1000u64);
+    sim.write(predicted_next_pc_any_const, 0x1004u64);
+    let clk = formal_global_clock();
+    let rst = formal_reset();
+    sim.write_clock(clk, false);
+    sim.write_reset(rst, true);
+    for cycle in 0..10 {
+        sim.advance_time(SimDuration::from_nanos(500));
+        println!("clock tick: {cycle}");
+        sim.write_clock(clk, true);
+        sim.advance_time(SimDuration::from_nanos(500));
+        sim.write_clock(clk, false);
+        sim.write_reset(rst, false);
+    }
+    assert!(sim.read_bool(sim.io().ran));
+}
+
+#[hdl]
+#[test]
+fn test_power_isa_paddi_sim() {
+    let config = PhantomConst::new_sized(CpuConfig::new(
+        vec![UnitConfig::new(UnitKind::AluBranch)],
+        NonZero::new(20).unwrap(),
+    ));
+    let any_consts = AnyConsts::new();
+    let m = check_power_isa_alu_formal(config, cases_add_sub(), Some(any_consts));
+    let mut sim = Simulation::new(m);
+    let _checked_vcd_output = cpu::checked_vcd_output!(
+        &mut sim,
+        "tests/expected/units_formal_power_isa_paddi_sim.vcd",
+    );
+    let AnyConsts {
+        decoder_first_word_any_const,
+        decoder_has_second_word_any_const,
+        decoder_second_word_any_const,
+        r3_any_const,
+        r4_any_const,
+        pc_any_const,
+        predicted_next_pc_any_const,
+    } = any_consts;
+    sim.write(decoder_first_word_any_const, 0x0600_0000u32);
+    sim.write(decoder_has_second_word_any_const, true);
+    sim.write(decoder_second_word_any_const, 0x3864_1000u32); // paddi 3, 4, 0x1000, 0
+    sim.write(r3_any_const, 0x9907_4F26_0000_0002u64);
+    sim.write(r4_any_const, 0x6000_0424_17DF_FEFDu64);
+    sim.write(pc_any_const, 0x1000u64);
+    sim.write(predicted_next_pc_any_const, 0x1008u64);
     let clk = formal_global_clock();
     let rst = formal_reset();
     sim.write_clock(clk, false);