add module exercising formal verification of memories

crates/fayalite/tests/formal.rs

@@ -7,12 +7,13 @@ use fayalite::{
     clock::{Clock, ClockDomain},
     expr::{CastTo, HdlPartialEq},
     firrtl::ExportOptions,
-    formal::{any_seq, formal_reset, hdl_assert, hdl_assume},
+    formal::{any_const, any_seq, formal_reset, hdl_assert, hdl_assume},
-    hdl_module,
+    hdl, hdl_module,
-    int::{Bool, UInt},
+    int::{Bool, DynSize, Size, UInt, UIntType},
-    module::{connect, connect_any, reg_builder, wire},
+    module::{connect, connect_any, instance, memory, reg_builder, wire},
     reset::ToReset,
     testing::assert_formal,
+    ty::StaticType,
 };
 
 /// Test hidden state
@@ -131,3 +132,164 @@ mod hidden_state {
         );
     }
 }
+
+/// Formal verification of designs containing memories
+///
+/// There is a trick for memories, described in the [Zipcpu blog].
+/// First, select a fixed but arbitrary memory address, monitoring all reads
+/// and writes made to it. Then, assert that anything read from that location
+/// matches the last stored value.
+///
+/// A difficulty for induction is that the memory represents [hidden_state]. A
+/// solution is to include an additional read port to the memory and assert
+/// that the memory location effectively contains the last stored value.
+/// This additional debug port is present only to assist the proof and is
+/// unused (optimized out) in actual use.
+///
+/// [Zipcpu blog]: <https://zipcpu.com/zipcpu/2018/07/13/memories.html>
+mod memory {
+    use super::*;
+
+    /// Test a simple 8-bit SRAM model
+    #[test]
+    fn test_sram() {
+        #[hdl]
+        struct WritePort<AddrWidth: Size> {
+            addr: UIntType<AddrWidth>,
+            data: UInt<8>,
+            en: Bool,
+        }
+        #[hdl]
+        struct ReadPort<AddrWidth: Size> {
+            addr: UIntType<AddrWidth>,
+            #[hdl(flip)]
+            data: UInt<8>,
+        }
+        /// This debug port is only meant to assist the proof.
+        /// For normal use in a design, a wrapper could be provided,
+        /// omitting this port.
+        /// The implementation is forbidden to use any information
+        /// provided on this port in its internal workings.
+        #[hdl]
+        struct DebugPort<AddrWidth: Size> {
+            selected: UIntType<AddrWidth>,
+            stored: UInt<8>,
+            wrote: Bool,
+        }
+        /// simple 1R1W SRAM model (one asynchronous read port and one
+        /// independent write port) with `n`-bit address width
+        #[hdl_module]
+        fn example_sram(n: usize) {
+            #[hdl]
+            let wr: WritePort<DynSize> = m.input(WritePort[n]);
+            #[hdl]
+            let rd: ReadPort<DynSize> = m.input(ReadPort[n]);
+            #[hdl]
+            let cd: ClockDomain = m.input();
+
+            // declare and connect the backing memory
+            #[hdl]
+            let mut mem = memory();
+            mem.depth(1 << n);
+            let read_port = mem.new_read_port();
+            let write_port = mem.new_write_port();
+            connect(write_port.clk, cd.clk);
+            connect(write_port.addr, wr.addr);
+            connect(write_port.en, wr.en);
+            connect(write_port.data, wr.data);
+            connect(write_port.mask, true);
+            connect(read_port.clk, cd.clk);
+            connect(read_port.addr, rd.addr);
+            connect(read_port.en, true);
+            connect(rd.data, read_port.data);
+
+            // To assist with induction, ensure that the chosen memory location
+            // really contains, always, the last value written to it.
+            #[hdl]
+            let dbg: DebugPort<DynSize> = m.input(DebugPort[n]);
+            let debug_port = mem.new_read_port();
+            connect(debug_port.en, true);
+            connect(debug_port.clk, cd.clk);
+            connect(debug_port.addr, dbg.selected);
+            #[hdl]
+            if dbg.wrote {
+                hdl_assert(cd.clk, debug_port.data.cmp_eq(dbg.stored), "");
+                // Try commenting out the assert above, induction will fail.
+                // Opening the trace, it can be seen that the memory contents
+                // and the stored value don't match, which is an unreachable
+                // state. By asserting the above, it will become invalid
+                // as well, so induction will skip this kind of situation.
+            }
+        }
+
+        /// formal verification of the SRAM module, parametrized by the
+        /// address bit-width
+        #[hdl_module]
+        fn test_module(n: usize) {
+            #[hdl]
+            let clk: Clock = m.input();
+            let cd = #[hdl]
+            ClockDomain {
+                clk,
+                rst: formal_reset().to_reset(),
+            };
+
+            // instantiate the SRAM model, connecting its inputs to
+            // a random sequence
+            #[hdl]
+            let rd: ReadPort<DynSize> = wire(ReadPort[n]);
+            connect(rd.addr, any_seq(UInt[n]));
+            #[hdl]
+            let wr: WritePort<DynSize> = wire(WritePort[n]);
+            connect(wr.addr, any_seq(UInt[n]));
+            connect(wr.data, any_seq(UInt::<8>::TYPE));
+            connect(wr.en, any_seq(Bool));
+            #[hdl]
+            let dut = instance(example_sram(n));
+            connect(dut.cd, cd);
+            connect(dut.rd, rd);
+            connect(dut.wr, wr);
+
+            // select a fixed but arbitrary test address
+            #[hdl]
+            let selected = wire(UInt[n]);
+            connect(selected, any_const(UInt[n]));
+            // store the last value written to that address
+            #[hdl]
+            let stored: UInt<8> = reg_builder().clock_domain(cd).reset(0u8);
+            // since memories are not initialized, track whether we wrote to the
+            // memory at least once
+            #[hdl]
+            let wrote: Bool = reg_builder().clock_domain(cd).reset(false);
+            // on a write, capture the last written value
+            #[hdl]
+            if wr.en & wr.addr.cmp_eq(selected) {
+                connect(stored, wr.data);
+                connect(wrote, true);
+            }
+            // on a read, assert that the read value is the same which was stored
+            #[hdl]
+            if rd.addr.cmp_eq(selected) & wrote {
+                hdl_assert(clk, rd.data.cmp_eq(stored), "");
+            }
+
+            // to assist induction, pass our state to the underlying instance
+            let dbg = #[hdl]
+            DebugPort {
+                selected,
+                stored,
+                wrote,
+            };
+            connect(dut.dbg, dbg);
+        }
+
+        assert_formal(
+            "sram",
+            test_module(8),
+            FormalMode::Prove,
+            2,
+            None,
+            ExportOptions::default(),
+        );
+    }
+}