From 14df66427778f20466ecb2ddb6271e7875108bb6 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 2 Jun 2026 01:36:12 -0700
Subject: [PATCH 1/2] update fayalite

---
 Cargo.lock | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 2fb2d97..2223fea 100644
--- a/Cargo.lock
+++ b/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#31353862ceba3d255fd6712813a457688b269358"
 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#31353862ceba3d255fd6712813a457688b269358"
 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#31353862ceba3d255fd6712813a457688b269358"
 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#31353862ceba3d255fd6712813a457688b269358"
 dependencies = [
  "indexmap",
  "prettyplease",

From 241255e12cb85d8ae7ffc4a929d2b6b9ac5b00ed Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 2 Jun 2026 01:38:06 -0700
Subject: [PATCH 2/2] tests/units_formal::test_power_isa_add_formal: formal
 proof actually starts, though it fails BMC

---
 crates/cpu/tests/units_formal.rs | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/crates/cpu/tests/units_formal.rs b/crates/cpu/tests/units_formal.rs
index e84103c..2e1ce03 100644
--- a/crates/cpu/tests/units_formal.rs
+++ b/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<
@@ -99,9 +97,21 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
 
 #[hdl_module]
 fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
+    #[hdl]
+    let clk: Clock = m.input();
+    #[hdl]
+    let cd = wire();
+    connect(
+        cd,
+        #[hdl]
+        ClockDomain {
+            clk,
+            rst: formal_reset().to_reset(),
+        },
+    );
     #[hdl]
     let harness = instance(formal_harness(config));
-    let cd = harness.cd;
+    connect(harness.cd, cd);
     #[hdl]
     let DecodeAndRunSingleInsnInput::<_, _> {
         decoder_input,
@@ -208,11 +218,11 @@ fn test_power_isa_add_formal() {
         vec![UnitConfig::new(UnitKind::AluBranch)],
         NonZero::new(20).unwrap(),
     ));
-    let dut = check_power_isa_add_formal(config);
+    let m = check_power_isa_add_formal(config);
     println!("starting assert formal");
     assert_formal(
         "test_power_isa_add_formal",
-        dut,
+        m,
         FormalMode::Prove,
         10,
         None,