Add test module exercising formal verification.

crates/fayalite/tests/formal.rs

@@ -95,12 +95,13 @@ 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 {
+                WithExtraAssertions => {
                     // "Open the box": add assertions about hidden state.
                     // In this case, the hidden bits are also always equal.
                     hdl_assert(clk, r1.cmp_eq(r2), "");
                 }
-            if let WithExtraAssumptions = constraint_mode {
+                WithExtraAssumptions => {
                     // Break the loop, do not allow "en" to remain low forever
                     #[hdl]
                     let past_en_reg = reg_builder().clock_domain(cd).reset(false);
@@ -108,6 +109,7 @@ mod hidden_state {
                     hdl_assume(clk, past_en_reg | en, "");
                 }
             }
+        }
         // we need a minimum of 16 steps so we can constrain all eight shift register bits,
         // given that we are allowed to disable the shift once every two cycles.
         assert_formal(