diff --git a/crates/fayalite/tests/formal.rs b/crates/fayalite/tests/formal.rs
index 46b8292..7684d0d 100644
--- a/crates/fayalite/tests/formal.rs
+++ b/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},
- hdl_module,
- int::{Bool, UInt},
- module::{connect, connect_any, reg_builder, wire},
+ formal::{any_const, any_seq, formal_reset, hdl_assert, hdl_assume},
+ hdl, hdl_module,
+ int::{Bool, DynSize, Size, UInt, UIntType},
+ module::{connect, connect_any, instance, memory, reg_builder, wire},
reset::ToReset,
testing::assert_formal,
+ ty::StaticType,
};
/// Test hidden state
@@ -131,3 +132,160 @@ 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 {
+ // try commenting out the assert below, induction will fail
+ hdl_assert(cd.clk, debug_port.data.cmp_eq(dbg.stored), "");
+ }
+ }
+
+ /// 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(),
+ );
+ }
+}