forked from libre-chip/fayalite
296 lines
11 KiB
Rust
296 lines
11 KiB
Rust
// 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_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
|
|
///
|
|
/// 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,
|
|
ExportOptions::default(),
|
|
);
|
|
// here a couple of cycles is enough
|
|
assert_formal(
|
|
"shift_register_with_assertions",
|
|
test_module(WithExtraAssertions),
|
|
FormalMode::Prove,
|
|
2,
|
|
None,
|
|
ExportOptions::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]: <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(),
|
|
);
|
|
}
|
|
}
|