formal proof works! also add test_power_isa_add_sim

crates/cpu/src/decoder/simple_power_isa.rs

@@ -2745,8 +2745,35 @@ const DECODE_FNS: &[(&[&str], DecodeFn)] = &[
 
 const MAX_MOPS_PER_INSN: usize = 3;
 
+#[derive(Debug)]
+pub struct DecodeFilterArgs<'a> {
+    mnemonic: &'a str,
+}
+
+impl DecodeFilterArgs<'_> {
+    pub fn mnemonic(&self) -> &str {
+        self.mnemonic
+    }
+}
+
+pub trait DecodeFilter {
+    fn should_include(&mut self, args: &DecodeFilterArgs<'_>) -> bool;
+}
+
+impl<T: ?Sized + FnMut(&DecodeFilterArgs<'_>) -> bool> DecodeFilter for T {
+    fn should_include(&mut self, args: &DecodeFilterArgs<'_>) -> bool {
+        self(args)
+    }
+}
+
+impl DecodeFilter for () {
+    fn should_include(&mut self, _args: &DecodeFilterArgs<'_>) -> bool {
+        true
+    }
+}
+
 #[hdl_module]
-pub fn decode_one_insn() {
+pub fn decode_one_insn(mut filter: impl DecodeFilter) {
     #[hdl]
     let output: ArrayVec<TraceAsString<MOp>, ConstUsize<{ MAX_MOPS_PER_INSN }>> = m.output();
     #[hdl]
@@ -2816,6 +2843,7 @@ pub fn decode_one_insn() {
                 let Some(decode_fn) = decode_fns.get(mnemonic) else {
                     panic!("unhandled mnemonic: {mnemonic:?}");
                 };
+                if filter.should_include(&DecodeFilterArgs { mnemonic }) {
                     decode_fn(&mut DecodeState {
                         mnemonic,
                         arguments,
@@ -2834,6 +2862,7 @@ pub fn decode_one_insn() {
             }
         }
     }
+}
 
 impl DecodeOneInsn for decode_one_insn {
     type Input = (UInt<32>, HdlOption<UInt<32>>);

crates/cpu/src/instruction.rs

@@ -40,6 +40,8 @@ impl<T: MOpTrait> MOpInto<T> for T {
     }
 }
 
+pub trait MOpLeaf<Target: MOpTrait>: MOpInto<Target> {}
+
 pub trait MOpVariantVisitOps {
     type MOp: MOpTrait<
             DestReg = <Self::Target as MOpTrait>::DestReg,
@@ -714,6 +716,35 @@ pub const COMMON_MOP_2_IMM_WIDTH: usize = common_mop_max_imm_size(2);
 pub const COMMON_MOP_3_IMM_WIDTH: usize = common_mop_max_imm_size(3);
 
 macro_rules! common_mop_struct {
+    (
+        #[leaf]
+        $(#[debug($($debug:tt)*)])?
+        #[mapped(<$NewDestReg:ident, $NewSrcReg:ident> $mapped_ty:ty)]
+        $(#[$struct_meta:meta])*
+        $vis:vis struct $MOp:ident<$DestReg:ident: $DestRegBound:ident, $SrcReg:ident: $SrcRegBound:ident $(, $Generic:ident: $GenericBound:ident)* $(,)?> {
+            $($body:tt)*
+        }
+    ) => {
+        common_mop_struct! {
+            $(#[debug($($debug)*)])?
+            #[mapped(<$NewDestReg, $NewSrcReg> $mapped_ty)]
+            $(#[$struct_meta])*
+            $vis struct $MOp<$DestReg: $DestRegBound, $SrcReg: $SrcRegBound $(, $Generic: $GenericBound)*> {
+                $($body)*
+            }
+        }
+
+        impl<
+            $DestReg: $DestRegBound,
+            $SrcReg: $SrcRegBound,
+            $($Generic: $GenericBound,)*
+            Target: MOpTrait,
+        > MOpLeaf<Target> for $MOp<$DestReg, $SrcReg, $($Generic),*>
+        where
+            Self: MOpInto<Target>,
+        {
+        }
+    };
     (
         #[debug($(#[$debug_hdl:ident])? |$debug_value:ident, $debug_f:ident| $debug_block:block $(where $($debug_where:tt)*)?)]
         #[mapped(<$NewDestReg:ident, $SrcReg:ident> $mapped_ty:ty)]
@@ -1322,6 +1353,7 @@ macro_rules! maybe_write_comma_flag {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let AddSubMOp::<_, _, _> {
@@ -1909,6 +1941,7 @@ impl LogicalFlagsMOpImm {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let LogicalFlagsMOp::<_, _> {
@@ -2073,6 +2106,7 @@ impl<DestReg: Type, SrcReg: Type> LogicalFlagsMOp<DestReg, SrcReg> {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let LogicalMOp::<_, _, _> {
@@ -2350,6 +2384,7 @@ impl SimValueDebug for ShiftRotateMOpImm {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let ShiftRotateMOp::<_, _> {
@@ -2465,6 +2500,7 @@ impl CompareMode {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let CompareMOp::<_, _, _> {
@@ -2569,6 +2605,7 @@ impl ConditionMode {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let BranchMOp::<_, _, _> {
@@ -2736,6 +2773,7 @@ pub enum ReadSpecialMOpImm {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let ReadSpecialMOp::<_, _> {
@@ -2826,6 +2864,7 @@ impl SimValueDebug for L2RegNum {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let ReadL2RegMOp::<_, _> {
@@ -2868,6 +2907,7 @@ impl<DestReg: Type, SrcReg: Type> ReadL2RegMOp<DestReg, SrcReg> {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let WriteL2RegMOp::<_, _> {
@@ -3014,6 +3054,7 @@ impl<DestReg: Type, SrcReg: Type, SrcCount: KnownSize>
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let LoadMOp::<_, _> {
@@ -3062,6 +3103,7 @@ impl<DestReg: Type, SrcReg: Type> LoadMOp<DestReg, SrcReg> {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let StoreMOp::<_, _> {
@@ -3120,6 +3162,7 @@ mop_enum! {
 }
 
 common_mop_struct! {
+    #[leaf]
     #[debug(#[hdl] |this, f| {
         #[hdl(sim)]
         let MoveRegMOp::<_, _> {

crates/cpu/src/test/decode_and_run_single_insn.rs

@@ -937,6 +937,7 @@ pub fn decode_and_run_single_insn<C: Type + PhantomConstCpuConfig, D: Type + Dec
         connect(output.data, output.ty().data.HdlNone());
         #[hdl]
         if let HdlSome(input) = input.data {
+            connect(decoder_input, input.decoder_input);
             connect(
                 state_reg,
                 HdlSome(DecodeAndRunSingleInsnState::new(

crates/cpu/src/unit.rs

@@ -4,7 +4,7 @@
 use crate::{
     config::CpuConfig,
     instruction::{
-        AluBranchMOp, LoadStoreMOp, MOp, MOpDestReg, MOpInto, MOpRegNum, MOpTrait,
+        AluBranchMOp, LoadStoreMOp, MOp, MOpDestReg, MOpInto, MOpLeaf, MOpRegNum, MOpTrait,
         MOpVariantVisitOps, MOpVariantVisitor, MOpVisitVariants, RenamedMOp, mop_enum,
     },
     rename_execute_retire::ExecuteToUnitInterface,
@@ -45,9 +45,9 @@ macro_rules! all_units {
         }
 
         impl $UnitKind {
-            pub fn unit(self, config: PhantomConst<CpuConfig>, unit_index: usize) -> DynUnit {
+            pub fn unit(self, config: PhantomConst<CpuConfig>, unit_index: usize, filter: &mut impl RenamedMOpFilter) -> DynUnit {
                 match self {
-                    $($UnitKind::$Unit => $create_dyn_unit_fn(config, unit_index),)*
+                    $($UnitKind::$Unit => $create_dyn_unit_fn(config, unit_index, filter),)*
                 }
             }
         }
@@ -326,19 +326,67 @@ all_units! {
             this.TransformedMove.mapped_ty(new_dest_reg, new_src_reg)
         })] TransformedMoveOp: Type
     > {
-        #[create_dyn_unit_fn = |config, unit_index| alu_branch::AluBranch::new(config, unit_index).to_dyn()]
+        #[create_dyn_unit_fn = |config, unit_index, filter| alu_branch::AluBranch::new(config, unit_index, filter).to_dyn()]
         #[extract(alu_branch_mop, alu_branch_mop_sim, alu_branch_mop_sim_ref, alu_branch_mop_sim_mut)]
         AluBranch(AluBranchMOp<DestReg, SrcReg>),
         #[transformed_move]
-        #[create_dyn_unit_fn = |config, unit_index| todo!()]
+        #[create_dyn_unit_fn = |config, unit_index, filter| todo!()]
         #[extract(transformed_move_mop, transformed_move_mop_sim, transformed_move_mop_sim_ref, transformed_move_mop_sim_mut)]
         TransformedMove(TransformedMoveOp),
-        #[create_dyn_unit_fn = |config, unit_index| todo!()]
+        #[create_dyn_unit_fn = |config, unit_index, filter| todo!()]
         #[extract(load_store_mop, load_store_mop_sim, load_store_mop_sim_ref, load_store_mop_sim_mut)]
         LoadStore(LoadStoreMOp<DestReg, SrcReg>),
     }
 }
 
+pub trait RenamedMOpFilter {
+    fn should_include(
+        &mut self,
+        mop: &SimValue<crate::rename_execute_retire::RenamedMOp<PhantomConst<CpuConfig>>>,
+    ) -> bool;
+    fn should_include_ty<
+        T: MOpLeaf<crate::rename_execute_retire::RenamedMOp<PhantomConst<CpuConfig>>>,
+    >(
+        &mut self,
+        ty: T,
+    ) -> bool
+    where
+        Self: Sized,
+    {
+        self.should_include(
+            &T::mop_into(
+                UInt::new_dyn(ty.canonical().bit_width())
+                    .zero()
+                    .to_expr()
+                    .cast_bits_to(ty),
+            )
+            .to_sim_value(),
+        )
+    }
+}
+
+impl<
+    T: ?Sized
+        + FnMut(&SimValue<crate::rename_execute_retire::RenamedMOp<PhantomConst<CpuConfig>>>) -> bool,
+> RenamedMOpFilter for T
+{
+    fn should_include(
+        &mut self,
+        mop: &SimValue<crate::rename_execute_retire::RenamedMOp<PhantomConst<CpuConfig>>>,
+    ) -> bool {
+        self(mop)
+    }
+}
+
+impl RenamedMOpFilter for () {
+    fn should_include(
+        &mut self,
+        _mop: &SimValue<crate::rename_execute_retire::RenamedMOp<PhantomConst<CpuConfig>>>,
+    ) -> bool {
+        true
+    }
+}
+
 pub trait UnitTrait:
     'static + Send + Sync + std::fmt::Debug + fayalite::intern::SupportsPtrEqWithTypeId
 {

crates/cpu/src/unit/alu_branch.rs

@@ -18,7 +18,7 @@ use crate::{
         ExecuteToUnitInterface, GlobalState, NextPcPredictorOp, RenamedMOp, UnitCausedCancel,
         UnitFinishCauseCancel, UnitInputsReady, UnitOutputReady,
     },
-    unit::{DynUnit, DynUnitWrapper, UnitKind, UnitTrait},
+    unit::{DynUnit, DynUnitWrapper, RenamedMOpFilter, UnitKind, UnitTrait},
 };
 use fayalite::{
     expr::CastToImpl,
@@ -1235,7 +1235,11 @@ fn read_special<C: Type + PhantomConstCpuConfig>(config: C) {
 }
 
 #[hdl_module]
-pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
+pub fn alu_branch(
+    config: PhantomConst<CpuConfig>,
+    unit_index: usize,
+    filter: &mut impl RenamedMOpFilter,
+) {
     #[hdl]
     let from_execute: ExecuteToUnitInterface<PhantomConst<CpuConfig>> =
         m.input(ExecuteToUnitInterface[config]);
@@ -1294,6 +1298,7 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                 #[hdl]
                 match mop {
                     AluBranchMOp::<_, _>::AddSub(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let add_sub = instance(add_sub(config));
                             #[hdl]
@@ -1309,8 +1314,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::AddSubI(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let add_sub_i = instance(add_sub(config));
                             #[hdl]
@@ -1326,8 +1335,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::LogicalFlags(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let logical_flags = instance(logical_flags(config));
                             #[hdl]
@@ -1341,8 +1354,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::Logical(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let logical = instance(logical(config));
                             #[hdl]
@@ -1356,8 +1373,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::LogicalI(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let logical_i = instance(logical(config));
                             #[hdl]
@@ -1371,8 +1392,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::ShiftRotate(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let shift_rotate = instance(shift_rotate(config));
                             #[hdl]
@@ -1386,8 +1411,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::Compare(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let compare = instance(compare(config));
                             #[hdl]
@@ -1401,8 +1430,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::CompareI(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let compare_i = instance(compare(config));
                             #[hdl]
@@ -1416,8 +1449,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::Branch(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let branch = instance(branch(config));
                             #[hdl]
@@ -1441,8 +1478,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(dest_value, output);
                             connect(predictor_op, predictor_op_);
                             connect(caused_cancel, caused_cancel_);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::BranchI(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let branch_i = instance(branch(config));
                             #[hdl]
@@ -1466,8 +1507,12 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(dest_value, output);
                             connect(predictor_op, predictor_op_);
                             connect(caused_cancel, caused_cancel_);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                     AluBranchMOp::<_, _>::ReadSpecial(mop) => {
+                        if filter.should_include_ty(mop.ty()) {
                             #[hdl]
                             let read_special = instance(read_special(config));
                             #[hdl]
@@ -1481,6 +1526,9 @@ pub fn alu_branch(config: PhantomConst<CpuConfig>, unit_index: usize) {
                             connect(*mop_, mop);
                             connect(src_values_, src_values);
                             connect(dest_value, output);
+                        } else {
+                            connect(*dest_value, PRegValue::zeroed());
+                        }
                     }
                 }
                 connect(
@@ -1530,10 +1578,14 @@ pub struct AluBranch {
 }
 
 impl AluBranch {
-    pub fn new(config: PhantomConst<CpuConfig>, unit_index: usize) -> Self {
+    pub fn new(
+        config: PhantomConst<CpuConfig>,
+        unit_index: usize,
+        filter: &mut impl RenamedMOpFilter,
+    ) -> Self {
         Self {
             config,
-            module: alu_branch(config, unit_index),
+            module: alu_branch(config, unit_index, filter),
         }
     }
 }

crates/cpu/tests/rename_execute_retire.rs

@@ -4079,7 +4079,7 @@ fn rename_execute_retire_test_harness<#[hdl(skip)] MI: MakeInsns>(
                 AluBranchKind::Real => {
                     let unit = instance_with_loc(
                         &dut.ty().to_units.unit_field_name(unit_index),
-                        cpu::unit::alu_branch::alu_branch(config, unit_index),
+                        cpu::unit::alu_branch::alu_branch(config, unit_index, &mut ()),
                         SourceLocation::caller(),
                     );
                     connect(unit.from_execute, to_unit);

crates/cpu/tests/simple_power_isa_decoder/main.rs

@@ -126,7 +126,7 @@ fn test_test_cases_assembly() -> std::io::Result<()> {
 #[test]
 fn test_decode_insn() {
     let _n = SourceLocation::normalize_files_for_tests();
-    let m = decode_one_insn();
+    let m = decode_one_insn(());
     let mut sim = Simulation::new(m);
     let _checked_vcd_output = checked_vcd_output!(
         &mut sim,

crates/cpu/tests/units_formal.rs

@@ -3,8 +3,8 @@
 
 use cpu::{
     config::{CpuConfig, UnitConfig},
-    decoder::simple_power_isa,
+    decoder::simple_power_isa::{self, DecodeFilter, DecodeFilterArgs},
-    instruction::MOpRegNum,
+    instruction::{AluBranchMOp, MOpRegNum},
     next_pc::CallStackOp,
     register::{FlagsMode, PRegFlags, PRegFlagsPowerISA, PRegFlagsPowerISAView, PRegValue},
     rename_execute_retire::{
@@ -14,7 +14,7 @@ use cpu::{
         DecodeAndRunSingleInsnInput, DecodeAndRunSingleInsnOutput, DecodeOneInsnInput,
         DecodeOneInsnMaxMOpCount, decode_and_run_single_insn,
     },
-    unit::{UnitKind, UnitTrait},
+    unit::{RenamedMOpFilter, UnitKind, UnitMOp, UnitTrait},
     util::array_vec::ArrayVec,
 };
 use fayalite::{
@@ -26,7 +26,11 @@ use fayalite::{
 use std::num::NonZero;
 
 #[hdl_module]
-fn formal_harness(config: PhantomConst<CpuConfig>) {
+fn formal_harness(
+    config: PhantomConst<CpuConfig>,
+    decode_filter: impl DecodeFilter,
+    renamed_mop_filter: &mut impl RenamedMOpFilter,
+) {
     #[hdl]
     let cd: ClockDomain = m.input();
 
@@ -47,7 +51,7 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
     #[hdl]
     let decode_and_run = instance(decode_and_run_single_insn(
         config,
-        simple_power_isa::decode_one_insn(),
+        simple_power_isa::decode_one_insn(decode_filter),
     ));
     connect(decode_and_run.cd, cd);
     #[hdl]
@@ -78,7 +82,7 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
     connect(decode_and_run.output.ready, true);
     connect(output, decode_and_run.output.data);
     for (unit_index, unit) in config.get().units.iter().enumerate() {
-        let dyn_unit = unit.kind.unit(config, unit_index);
+        let dyn_unit = unit.kind.unit(config, unit_index, renamed_mop_filter);
         let unit = instance_with_loc(
             &decode_and_run.ty().to_units.unit_field_name(unit_index),
             dyn_unit.module(),
@@ -95,24 +99,70 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
     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>>,
+}
+
+impl R3R4AnyConst {
+    #[track_caller]
+    fn new() -> Self {
+        Self {
+            r3_any_const: any_const(StaticType::TYPE),
+            r4_any_const: any_const(StaticType::TYPE),
+        }
+    }
+}
+
 #[hdl_module]
-fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
+fn check_power_isa_add_formal(
-    #[hdl]
+    config: PhantomConst<CpuConfig>,
-    let clk: Clock = m.input();
+    r3_r4_any_const: Option<R3R4AnyConst>,
+) {
     #[hdl]
     let cd = wire();
     connect(
         cd,
         #[hdl]
         ClockDomain {
-            clk,
+            clk: formal_global_clock(),
             rst: formal_reset().to_reset(),
         },
     );
     #[hdl]
-    let harness = instance(formal_harness(config));
+    let harness = instance(formal_harness(
+        config,
+        |args: &DecodeFilterArgs<'_>| args.mnemonic() == "add",
+        &mut |mop: &SimValue<_>| -> bool {
+            #[hdl(sim)]
+            match mop {
+                UnitMOp::<_, _, _>::AluBranch(mop) =>
+                {
+                    #[hdl(sim)]
+                    match mop {
+                        AluBranchMOp::<_, _>::AddSub(_) => true,
+                        _ => false,
+                    }
+                }
+                _ => false,
+            }
+        },
+    ));
     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]
+    let cycle_count = reg_builder().clock_domain(cd).reset(0u32);
+    connect_any(cycle_count, cycle_count + 1u32);
+    #[hdl]
+    if cycle_count.cmp_ge(5u32) {
+        hdl_assert(cd.clk, ran, "");
+    }
+    #[hdl]
     let DecodeAndRunSingleInsnInput::<_, _> {
         decoder_input,
         fetch_block_id,
@@ -135,12 +185,16 @@ fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
             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, any_const(StaticType::TYPE));
+    connect(input_r3, r3_any_const);
     #[hdl]
     let input_r4 = wire();
-    connect(input_r4, any_const(StaticType::TYPE));
+    connect(input_r4, r4_any_const);
     connect(
         input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp,
         input_r3,
@@ -151,6 +205,7 @@ fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
     );
     #[hdl]
     if let HdlSome(output) = harness.output {
+        connect(ran_reg, true);
         #[hdl]
         let DecodeAndRunSingleInsnOutput::<_, _> {
             regs,
@@ -218,13 +273,12 @@ fn test_power_isa_add_formal() {
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let m = check_power_isa_add_formal(config);
+    let m = check_power_isa_add_formal(config, None);
-    println!("starting assert formal");
     assert_formal(
         "test_power_isa_add_formal",
         m,
-        FormalMode::Prove,
+        FormalMode::BMC,
-        10,
+        7,
         None,
         ExportOptions {
             simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
@@ -232,3 +286,34 @@ fn test_power_isa_add_formal() {
         },
     );
 }
+
+#[hdl]
+#[test]
+fn test_power_isa_add_sim() {
+    let config = PhantomConst::new_sized(CpuConfig::new(
+        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 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 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));
+}