add module exercising formal verification of memories

Fixes: #4

crates/fayalite/src/cli.rs

@@ -653,21 +653,19 @@ impl FormalArgs {
                 self.sby.display()
             )))
         };
-        if do_cache {
-            fs::write(
-                cache_file,
-                serde_json::to_string_pretty(&FormalCache {
-                    version: FormalCacheVersion::CURRENT,
-                    contents_hash: contents_hash.unwrap(),
-                    stdout_stderr: captured_output,
-                    result: match &result {
-                        Ok(FormalOutput { verilog: _ }) => Ok(FormalCacheOutput {}),
-                        Err(error) => Err(error.to_string()),
-                    },
-                })
-                .expect("serialization shouldn't ever fail"),
-            )?;
-        }
+        fs::write(
+            cache_file,
+            serde_json::to_string_pretty(&FormalCache {
+                version: FormalCacheVersion::CURRENT,
+                contents_hash: contents_hash.unwrap(),
+                stdout_stderr: captured_output,
+                result: match &result {
+                    Ok(FormalOutput { verilog: _ }) => Ok(FormalCacheOutput {}),
+                    Err(error) => Err(error.to_string()),
+                },
+            })
+            .expect("serialization shouldn't ever fail"),
+        )?;
         result
     }
 }

crates/fayalite/src/int.rs

@@ -453,7 +453,10 @@ impl SInt {
                     v.not().bits().checked_add(1).expect("too big")
                 }
                 Sign::NoSign => 0,
-                Sign::Plus => v.bits(),
+                Sign::Plus => {
+                    // account for sign bit
+                    v.bits().checked_add(1).expect("too big")
+                }
             }
             .try_into()
             .expect("too big"),
@@ -693,3 +696,31 @@ impl ToLiteralBits for bool {
         Ok(interned_bit(*self))
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_uint_for_value() {
+        assert_eq!(UInt::for_value(0u8).width, 0);
+        assert_eq!(UInt::for_value(1u8).width, 1);
+        assert_eq!(UInt::for_value(2u8).width, 2);
+        assert_eq!(UInt::for_value(3u8).width, 2);
+        assert_eq!(UInt::for_value(4u8).width, 3);
+    }
+
+    #[test]
+    fn test_sint_for_value() {
+        assert_eq!(SInt::for_value(-5).width, 4);
+        assert_eq!(SInt::for_value(-4).width, 3);
+        assert_eq!(SInt::for_value(-3).width, 3);
+        assert_eq!(SInt::for_value(-2).width, 2);
+        assert_eq!(SInt::for_value(-1).width, 1);
+        assert_eq!(SInt::for_value(0).width, 0);
+        assert_eq!(SInt::for_value(1).width, 2);
+        assert_eq!(SInt::for_value(2).width, 3);
+        assert_eq!(SInt::for_value(3).width, 3);
+        assert_eq!(SInt::for_value(4).width, 4);
+    }
+}

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(),
+        );
+    }
+}