Add test module exercising formal verification.

crates/fayalite/tests/formal.rs

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