Add test module exercising formal verification.

crates/fayalite/tests/formal.rs

@@ -0,0 +1,131 @@
+// SPDX-License-Identifier: LGPL-3.0-or-later
+// See Notices.txt for copyright information
+//! Formal tests in Fayalite
+
+use fayalite::{
+    cli::FormalMode,
+    clock::{Clock, ClockDomain},
+    expr::{CastTo, HdlPartialEq},
+    firrtl::ExportOptions,
+    formal::{any_seq, formal_reset, hdl_assert, hdl_assume},
+    hdl_module,
+    int::{Bool, UInt},
+    module::{connect, connect_any, reg_builder, wire},
+    reset::ToReset,
+    testing::assert_formal,
+};
+
+/// Test hidden state
+///
+/// Hidden state can cause problems for induction, since the formal engine
+/// can assign invalid values to the state registers, making it traverse
+/// valid but unreachable states.
+///
+/// One solution is to go sufficiently in the past so the engine is forced
+/// to eventually take a reachable state. This may be hampered by
+/// existence of loops, then assumptions may be added to break them.
+///
+/// Another solution is to "open the black box" and add additional
+/// assertions involving the hidden state, so that the unreachable states
+/// become invalid as well.
+///
+/// Both approaches are taken here.
+///
+/// See [Claire Wolf's presentation] and [Zipcpu blog article].
+///
+/// [Claire Wolf's presentation]: https://web.archive.org/web/20200115081517fw_/http://www.clifford.at/papers/2017/smtbmc-sby/
+/// [Zipcpu blog article]: https://zipcpu.com/blog/2018/03/10/induction-exercise.html
+mod hidden_state {
+    use super::*;
+    /// Test hidden state by shift registers
+    ///
+    /// The code implement the ideas from an article in the [Zipcpu blog]. Two
+    /// shift registers are fed from the same input, so they should always have
+    /// the same value. However the only observable is a comparison of their
+    /// last bit, all the others are hidden. To complicate matters, an enable
+    /// signal causes a loop in state space.
+    ///
+    /// [Zipcpu blog]: https://zipcpu.com/blog/2018/03/10/induction-exercise.html
+    #[test]
+    fn shift_register() {
+        enum ConstraintMode {
+            WithExtraAssertions,
+            WithExtraAssumptions,
+        }
+        use ConstraintMode::*;
+        #[hdl_module]
+        fn test_module(constraint_mode: ConstraintMode) {
+            #[hdl]
+            let clk: Clock = m.input();
+            #[hdl]
+            let cd = wire();
+            connect(
+                cd,
+                #[hdl]
+                ClockDomain {
+                    clk,
+                    rst: formal_reset().to_reset(),
+                },
+            );
+            // input signal for the shift registers
+            #[hdl]
+            let i: Bool = wire();
+            connect(i, any_seq(Bool));
+            // shift enable signal
+            #[hdl]
+            let en: Bool = wire();
+            connect(en, any_seq(Bool));
+            // comparison output
+            #[hdl]
+            let o: Bool = wire();
+            // shift registers, with enable
+            #[hdl]
+            let r1 = reg_builder().clock_domain(cd).reset(0u8);
+            #[hdl]
+            let r2 = reg_builder().clock_domain(cd).reset(0u8);
+            #[hdl]
+            if en {
+                connect_any(r1, (r1 << 1) | i.cast_to(UInt[1]));
+                connect_any(r2, (r2 << 1) | i.cast_to(UInt[1]));
+            }
+            // compare last bits of both shift registers
+            connect(o, r1[7].cmp_eq(r2[7]));
+
+            // what we want to prove: last bits are always equal
+            hdl_assert(clk, o, "");
+
+            // additional terms below are only needed to assist with the induction proof
+            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), "");
+            }
+            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);
+                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,
+        // given that we are allowed to disable the shift once every two cycles.
+        assert_formal(
+            "shift_register_with_assumptions",
+            test_module(WithExtraAssumptions),
+            FormalMode::Prove,
+            16,
+            None,
+            ExportOptions::default(),
+        );
+        // here a couple of cycles is enough
+        assert_formal(
+            "shift_register_with_assertions",
+            test_module(WithExtraAssertions),
+            FormalMode::Prove,
+            2,
+            None,
+            ExportOptions::default(),
+        );
+    }
+}