Add test module exercising formal verification.

crates/fayalite/tests/formal.rs

@@ -95,13 +95,12 @@ mod hidden_state {
             hdl_assert(clk, o, "");
 
             // additional terms below are only needed to assist with the induction proof
-            match constraint_mode {
-                WithExtraAssertions => {
+            if let WithExtraAssertions = constraint_mode {
                 // "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), "");
             }
-                WithExtraAssumptions => {
+            if let WithExtraAssumptions = constraint_mode {
                 // Break the loop, do not allow "en" to remain low forever
                 #[hdl]
                 let past_en_reg = reg_builder().clock_domain(cd).reset(false);
@@ -109,7 +108,6 @@ 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(