Add test module exercising formal verification.

crates/fayalite/tests/formal.rs

@@ -95,17 +95,19 @@ mod hidden_state {
             hdl_assert(clk, o, "");
 
             // additional terms below are only needed to assist with the induction proof
-            if let WithExtraAssertions = constraint_mode {
+            match constraint_mode {
-                // "Open the box": add assertions about hidden state.
+                WithExtraAssertions => {
-                // In this case, the hidden bits are also always equal.
+                    // "Open the box": add assertions about hidden state.
-                hdl_assert(clk, r1.cmp_eq(r2), "");
+                    // In this case, the hidden bits are also always equal.
-            }
+                    hdl_assert(clk, r1.cmp_eq(r2), "");
-            if let WithExtraAssumptions = constraint_mode {
+                }
-                // Break the loop, do not allow "en" to remain low forever
+                WithExtraAssumptions => {
-                #[hdl]
+                    // Break the loop, do not allow "en" to remain low forever
-                let past_en_reg = reg_builder().clock_domain(cd).reset(false);
+                    #[hdl]
-                connect(past_en_reg, en);
+                    let past_en_reg = reg_builder().clock_domain(cd).reset(false);
-                hdl_assume(clk, past_en_reg | en, "");
+                    connect(past_en_reg, en);
+                    hdl_assume(clk, past_en_reg | en, "");
+                }
             }
         }
         // we need a minimum of 16 steps so we can constrain all eight shift register bits,