// SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information //! Formal tests in Fayalite use fayalite::prelude::*; /// 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 match constraint_mode { WithExtraAssertions => { // "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 => { // 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, Default::default(), ); // here a couple of cycles is enough assert_formal( "shift_register_with_assertions", test_module(WithExtraAssertions), FormalMode::Prove, 2, None, Default::default(), ); } } /// 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]: mod memory { use super::*; /// Test a simple 8-bit SRAM model #[test] fn test_sram() { #[hdl] struct WritePort { addr: UIntType, data: UInt<8>, en: Bool, } #[hdl] struct ReadPort { addr: UIntType, #[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 { selected: UIntType, 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 = m.input(WritePort[n]); #[hdl] let rd: ReadPort = 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 = 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 = wire(ReadPort[n]); connect(rd.addr, any_seq(UInt[n])); #[hdl] let wr: WritePort = wire(WritePort[n]); connect(wr.addr, any_seq(UInt[n])); connect(wr.data, any_seq(UInt::<8>::new_static())); 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, Default::default(), ); } }