WIP: add test_power_isa_add_sim

Cargo.lock

@@ -388,7 +388,7 @@ checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6"
 [[package]]
 name = "fayalite"
 version = "0.3.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#ffca1a279d79507c025a8d969bfff18295760c02"
 dependencies = [
  "base64",
  "bitvec",
@@ -417,7 +417,7 @@ dependencies = [
 [[package]]
 name = "fayalite-proc-macros"
 version = "0.3.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#ffca1a279d79507c025a8d969bfff18295760c02"
 dependencies = [
  "fayalite-proc-macros-impl",
 ]
@@ -425,7 +425,7 @@ dependencies = [
 [[package]]
 name = "fayalite-proc-macros-impl"
 version = "0.3.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#ffca1a279d79507c025a8d969bfff18295760c02"
 dependencies = [
  "base16ct 0.2.0",
  "num-bigint",
@@ -440,7 +440,7 @@ dependencies = [
 [[package]]
 name = "fayalite-visit-gen"
 version = "0.3.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#ffca1a279d79507c025a8d969bfff18295760c02"
 dependencies = [
  "indexmap",
  "prettyplease",

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/tests/units_formal.rs

@@ -28,9 +28,7 @@ use std::num::NonZero;
 #[hdl_module]
 fn formal_harness(config: PhantomConst<CpuConfig>) {
     #[hdl]
-    let cd: ClockDomain = m.output();
-    connect(cd.clk, fayalite::formal::formal_global_clock());
-    connect(cd.rst, fayalite::formal::formal_reset().to_reset());
+    let cd: ClockDomain = m.input();
 
     #[hdl]
     let input: DecodeAndRunSingleInsnInput<
@@ -97,11 +95,45 @@ 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(
+    config: PhantomConst<CpuConfig>,
+    r3_r4_any_const: Option<R3R4AnyConst>,
+) {
+    #[hdl]
+    let cd = wire();
+    connect(
+        cd,
+        #[hdl]
+        ClockDomain {
+            clk: formal_global_clock(),
+            rst: formal_reset().to_reset(),
+        },
+    );
     #[hdl]
     let harness = instance(formal_harness(config));
-    let cd = harness.cd;
+    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 DecodeAndRunSingleInsnInput::<_, _> {
         decoder_input,
@@ -125,12 +157,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,
@@ -141,6 +177,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,
@@ -208,11 +245,10 @@ fn test_power_isa_add_formal() {
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let dut = check_power_isa_add_formal(config);
-    println!("starting assert formal");
+    let m = check_power_isa_add_formal(config, None);
     assert_formal(
         "test_power_isa_add_formal",
-        dut,
+        m,
         FormalMode::Prove,
         10,
         None,
@@ -222,3 +258,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));
+}