forked from libre-chip/fayalite
3dc82c4804
For now, only check that the basic properties work in bounded model check mode, leave the induction proof for later. Partially replace the previously existing proof. Remove earlier assumptions and bounds that don't apply for this proof. Use parameterized types instead of hard-coded types.
476 lines
16 KiB
Rust
476 lines
16 KiB
Rust
// SPDX-License-Identifier: LGPL-3.0-or-later
|
|
// See Notices.txt for copyright information
|
|
use crate::{memory::splat_mask, prelude::*};
|
|
use std::num::NonZeroUsize;
|
|
|
|
#[hdl]
|
|
pub struct ReadyValid<T> {
|
|
pub data: HdlOption<T>,
|
|
#[hdl(flip)]
|
|
pub ready: Bool,
|
|
}
|
|
|
|
impl<T: Type> ReadyValid<T> {
|
|
#[hdl]
|
|
pub fn firing(expr: Expr<Self>) -> Expr<Bool> {
|
|
#[hdl]
|
|
let firing: Bool = wire();
|
|
#[hdl]
|
|
match expr.data {
|
|
HdlNone => connect(firing, false),
|
|
HdlSome(_) => connect(firing, expr.ready),
|
|
}
|
|
firing
|
|
}
|
|
#[hdl]
|
|
pub fn firing_data(expr: impl ToExpr<Type = Self>) -> Expr<HdlOption<T>> {
|
|
let expr = expr.to_expr();
|
|
let option_ty = Expr::ty(expr).data;
|
|
#[hdl]
|
|
let firing_data = wire(option_ty);
|
|
connect(firing_data, option_ty.HdlNone());
|
|
#[hdl]
|
|
if expr.ready {
|
|
connect(firing_data, expr.data);
|
|
}
|
|
firing_data
|
|
}
|
|
#[hdl]
|
|
pub fn map<R: Type>(
|
|
expr: Expr<Self>,
|
|
f: impl FnOnce(Expr<T>) -> Expr<R>,
|
|
) -> Expr<ReadyValid<R>> {
|
|
let data = HdlOption::map(expr.data, f);
|
|
#[hdl]
|
|
let mapped = wire(ReadyValid[Expr::ty(data).HdlSome]);
|
|
connect(mapped.data, data);
|
|
connect(expr.ready, mapped.ready);
|
|
mapped
|
|
}
|
|
}
|
|
|
|
#[hdl_module]
|
|
pub fn queue<T: Type>(
|
|
ty: T,
|
|
capacity: NonZeroUsize,
|
|
inp_ready_is_comb: bool,
|
|
out_valid_is_comb: bool,
|
|
) {
|
|
let count_ty = UInt::range_inclusive(0..=capacity.get());
|
|
let index_ty = UInt::range(0..capacity.get());
|
|
|
|
#[hdl]
|
|
let cd: ClockDomain = m.input();
|
|
#[hdl]
|
|
let inp: ReadyValid<T> = m.input(ReadyValid[ty]);
|
|
#[hdl]
|
|
let out: ReadyValid<T> = m.output(ReadyValid[ty]);
|
|
#[hdl]
|
|
let count: UInt = m.output(count_ty);
|
|
|
|
#[hdl]
|
|
let inp_index_reg = reg_builder().clock_domain(cd).reset(0.cast_to(index_ty));
|
|
#[hdl]
|
|
let out_index_reg = reg_builder().clock_domain(cd).reset(0.cast_to(index_ty));
|
|
#[hdl]
|
|
let maybe_full_reg = reg_builder().clock_domain(cd).reset(false);
|
|
|
|
#[hdl]
|
|
let mut mem = memory(ty);
|
|
mem.depth(capacity.get());
|
|
let read_port = mem.new_read_port();
|
|
let write_port = mem.new_write_port();
|
|
|
|
#[hdl]
|
|
let inp_firing: Bool = wire();
|
|
connect(inp_firing, ReadyValid::firing(inp));
|
|
#[hdl]
|
|
let out_firing: Bool = wire();
|
|
connect(out_firing, ReadyValid::firing(out));
|
|
#[hdl]
|
|
let indexes_equal: Bool = wire();
|
|
connect(indexes_equal, inp_index_reg.cmp_eq(out_index_reg));
|
|
#[hdl]
|
|
let empty: Bool = wire();
|
|
connect(empty, indexes_equal & !maybe_full_reg);
|
|
#[hdl]
|
|
let full: Bool = wire();
|
|
connect(full, indexes_equal & maybe_full_reg);
|
|
|
|
connect(read_port.addr, out_index_reg);
|
|
connect(read_port.en, true);
|
|
connect(read_port.clk, cd.clk);
|
|
connect(write_port.addr, inp_index_reg);
|
|
connect(write_port.en, inp_firing);
|
|
connect(write_port.clk, cd.clk);
|
|
connect(write_port.data, HdlOption::unwrap_or(inp.data, ty.uninit()));
|
|
connect(write_port.mask, splat_mask(ty, true.to_expr()));
|
|
|
|
connect(inp.ready, !full);
|
|
if inp_ready_is_comb {
|
|
#[hdl]
|
|
if out.ready {
|
|
connect(inp.ready, true);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if !empty {
|
|
connect(out.data, HdlSome(read_port.data));
|
|
} else {
|
|
if out_valid_is_comb {
|
|
connect(out.data, inp.data);
|
|
} else {
|
|
connect(out.data, HdlOption[ty].HdlNone());
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if inp_firing.cmp_ne(out_firing) {
|
|
connect(maybe_full_reg, inp_firing);
|
|
}
|
|
|
|
#[hdl]
|
|
if inp_firing {
|
|
#[hdl]
|
|
if inp_index_reg.cmp_eq(capacity.get() - 1) {
|
|
connect_any(inp_index_reg, 0_hdl_u0);
|
|
} else {
|
|
connect_any(inp_index_reg, inp_index_reg + 1_hdl_u1);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if out_firing {
|
|
#[hdl]
|
|
if out_index_reg.cmp_eq(capacity.get() - 1) {
|
|
connect_any(out_index_reg, 0_hdl_u0);
|
|
} else {
|
|
connect_any(out_index_reg, out_index_reg + 1_hdl_u1);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if indexes_equal {
|
|
#[hdl]
|
|
if maybe_full_reg {
|
|
connect_any(count, capacity);
|
|
} else {
|
|
connect_any(count, 0_hdl_u0);
|
|
}
|
|
} else {
|
|
if capacity.is_power_of_two() {
|
|
debug_assert_eq!(count_ty.width(), index_ty.width() + 1);
|
|
#[hdl]
|
|
let count_lower = wire(index_ty);
|
|
connect(
|
|
count_lower,
|
|
(inp_index_reg - out_index_reg).cast_to(index_ty),
|
|
); // wrap
|
|
connect(count, count_lower.cast_to(count_ty));
|
|
} else {
|
|
debug_assert_eq!(count_ty.width(), index_ty.width());
|
|
#[hdl]
|
|
if inp_index_reg.cmp_lt(out_index_reg) {
|
|
connect(count, inp_index_reg + capacity - out_index_reg);
|
|
} else {
|
|
connect(count, inp_index_reg - out_index_reg);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
#[cfg(test)]
|
|
mod tests {
|
|
use super::*;
|
|
use crate::{
|
|
cli::FormalMode, firrtl::ExportOptions,
|
|
module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
|
|
ty::StaticType,
|
|
};
|
|
use std::num::NonZero;
|
|
|
|
#[track_caller]
|
|
fn test_queue(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
|
|
assert_formal(
|
|
format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"),
|
|
queue_test(capacity, inp_ready_is_comb, out_valid_is_comb),
|
|
FormalMode::BMC,
|
|
14,
|
|
None,
|
|
ExportOptions {
|
|
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
|
|
..ExportOptions::default()
|
|
},
|
|
);
|
|
/// Formal verification of the FIFO queue
|
|
///
|
|
/// The strategy derives from the observation that, if we filter its
|
|
/// input and output streams to consider just one in every N reads and
|
|
/// writes (where N is the FIFO capacity), then the FIFO effectively
|
|
/// behaves as an one-entry FIFO.
|
|
///
|
|
/// In particular, any counterexample of the full FIFO behaving badly
|
|
/// will also be caught by one of the filtered versions (one which
|
|
/// happens to be in phase with the offending input or output).
|
|
///
|
|
/// Interestingly, this strategy seems to be simpler than the one
|
|
/// described on the [Asynchronous FIFO] and the [FIFO tutorial]
|
|
/// articles of the ZipCPU blog, which considers two adjacent writes
|
|
/// and reads.
|
|
///
|
|
/// [Asynchronous FIFO]: https://zipcpu.com/blog/2018/07/06/afifo.html#fifo-contract
|
|
/// [FIFO tutorial]: https://zipcpu.com/tutorial/lsn-10-fifo.pdf
|
|
#[hdl_module]
|
|
fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
|
|
#[hdl]
|
|
let clk: Clock = m.input();
|
|
#[hdl]
|
|
let cd = wire();
|
|
connect(
|
|
cd,
|
|
#[hdl]
|
|
ClockDomain {
|
|
clk,
|
|
rst: formal_reset().to_reset(),
|
|
},
|
|
);
|
|
|
|
// random input data
|
|
#[hdl]
|
|
let inp_data: HdlOption<UInt<8>> = wire();
|
|
#[hdl]
|
|
if any_seq(Bool) {
|
|
connect(inp_data, HdlSome(any_seq(UInt::<8>::TYPE)));
|
|
} else {
|
|
connect(inp_data, HdlNone());
|
|
}
|
|
|
|
// assert output ready at random
|
|
#[hdl]
|
|
let out_ready: Bool = wire();
|
|
connect(out_ready, any_seq(Bool));
|
|
|
|
// The current number of elements in the FIFO ranges from zero to
|
|
// maximum capacity, inclusive.
|
|
let count_ty = UInt::range_inclusive(0..=capacity.get());
|
|
// type for counters that wrap around at the FIFO capacity
|
|
let index_ty = UInt::range(0..capacity.get());
|
|
|
|
// among all entries of the FIFO internal circular memory, choose
|
|
// one at random to check
|
|
#[hdl]
|
|
let index_to_check = wire(index_ty);
|
|
connect(index_to_check, any_const(index_ty));
|
|
|
|
// instantiate and connect the queue
|
|
#[hdl]
|
|
let dut = instance(queue(
|
|
UInt[ConstUsize::<8>],
|
|
capacity,
|
|
inp_ready_is_comb,
|
|
out_valid_is_comb,
|
|
));
|
|
connect(dut.cd, cd);
|
|
connect(dut.inp.data, inp_data);
|
|
connect(dut.out.ready, out_ready);
|
|
|
|
// Keep an independent count of words in the FIFO. Ensure that
|
|
// it's always correct, and never overflows.
|
|
#[hdl]
|
|
let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero());
|
|
#[hdl]
|
|
if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) {
|
|
hdl_assert(clk, expected_count_reg.cmp_ne(capacity.get()), "");
|
|
connect_any(expected_count_reg, expected_count_reg + 1u8);
|
|
} else if !ReadyValid::firing(dut.inp) & ReadyValid::firing(dut.out) {
|
|
hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), "");
|
|
connect_any(expected_count_reg, expected_count_reg - 1u8);
|
|
}
|
|
hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), "");
|
|
|
|
// keep an independent write index into the FIFO's circular buffer
|
|
#[hdl]
|
|
let inp_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
|
|
#[hdl]
|
|
if ReadyValid::firing(dut.inp) {
|
|
#[hdl]
|
|
if inp_index_reg.cmp_ne(capacity.get() - 1) {
|
|
connect_any(inp_index_reg, inp_index_reg + 1u8);
|
|
} else {
|
|
connect_any(inp_index_reg, 0_hdl_u0);
|
|
}
|
|
}
|
|
|
|
// keep an independent read index into the FIFO's circular buffer
|
|
#[hdl]
|
|
let out_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
|
|
#[hdl]
|
|
if ReadyValid::firing(dut.out) {
|
|
#[hdl]
|
|
if out_index_reg.cmp_ne(capacity.get() - 1) {
|
|
connect_any(out_index_reg, out_index_reg + 1u8);
|
|
} else {
|
|
connect_any(out_index_reg, 0_hdl_u0);
|
|
}
|
|
}
|
|
|
|
// filter the input data stream, predicated by the read index
|
|
// matching the chosen position in the FIFO's circular buffer
|
|
#[hdl]
|
|
let inp_index_matches = wire();
|
|
connect(inp_index_matches, inp_index_reg.cmp_eq(index_to_check));
|
|
#[hdl]
|
|
let inp_firing_data = wire();
|
|
connect(inp_firing_data, HdlNone());
|
|
#[hdl]
|
|
if inp_index_matches {
|
|
connect(inp_firing_data, ReadyValid::firing_data(dut.inp));
|
|
}
|
|
|
|
// filter the output data stream, predicated by the write index
|
|
// matching the chosen position in the FIFO's circular buffer
|
|
#[hdl]
|
|
let out_index_matches = wire();
|
|
connect(out_index_matches, out_index_reg.cmp_eq(index_to_check));
|
|
#[hdl]
|
|
let out_firing_data = wire();
|
|
connect(out_firing_data, HdlNone());
|
|
#[hdl]
|
|
if out_index_matches {
|
|
connect(out_firing_data, ReadyValid::firing_data(dut.out));
|
|
}
|
|
|
|
// Implement an one-entry FIFO and ensure its equivalence to the
|
|
// filtered FIFO.
|
|
//
|
|
// the holding register for our one-entry FIFO
|
|
#[hdl]
|
|
let stored_reg = reg_builder().clock_domain(cd).reset(HdlNone());
|
|
#[hdl]
|
|
match stored_reg {
|
|
// If the holding register is empty...
|
|
HdlNone => {
|
|
#[hdl]
|
|
match inp_firing_data {
|
|
// ... and we are not receiving data, then we must not
|
|
// transmit any data.
|
|
HdlNone => hdl_assert(clk, HdlOption::is_none(out_firing_data), ""),
|
|
// If we are indeed receiving some data...
|
|
HdlSome(data_in) => {
|
|
#[hdl]
|
|
match out_firing_data {
|
|
// ... and transmitting at the same time, we
|
|
// must be transmitting the input data itself,
|
|
// since the holding register is empty.
|
|
HdlSome(data_out) => hdl_assert(clk, data_out.cmp_eq(data_in), ""),
|
|
// If we are receiving, but not transmitting,
|
|
// store the received data in the holding
|
|
// register.
|
|
HdlNone => connect(stored_reg, HdlSome(data_in)),
|
|
}
|
|
}
|
|
}
|
|
}
|
|
// If there is some value stored in the holding register...
|
|
HdlSome(stored) => {
|
|
#[hdl]
|
|
match out_firing_data {
|
|
// ... and we are not transmitting it, we cannot
|
|
// receive any more data.
|
|
HdlNone => hdl_assert(clk, HdlOption::is_none(inp_firing_data), ""),
|
|
// If we are transmitting a previously stored value...
|
|
HdlSome(data_out) => {
|
|
// ... it must be the same data we stored earlier.
|
|
hdl_assert(clk, data_out.cmp_eq(stored), "");
|
|
// Also, accept new data, if any. Otherwise,
|
|
// let the holding register become empty.
|
|
connect(stored_reg, inp_firing_data);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn test_1_false_false() {
|
|
test_queue(NonZero::new(1).unwrap(), false, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_1_false_true() {
|
|
test_queue(NonZero::new(1).unwrap(), false, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_1_true_false() {
|
|
test_queue(NonZero::new(1).unwrap(), true, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_1_true_true() {
|
|
test_queue(NonZero::new(1).unwrap(), true, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_2_false_false() {
|
|
test_queue(NonZero::new(2).unwrap(), false, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_2_false_true() {
|
|
test_queue(NonZero::new(2).unwrap(), false, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_2_true_false() {
|
|
test_queue(NonZero::new(2).unwrap(), true, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_2_true_true() {
|
|
test_queue(NonZero::new(2).unwrap(), true, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_3_false_false() {
|
|
test_queue(NonZero::new(3).unwrap(), false, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_3_false_true() {
|
|
test_queue(NonZero::new(3).unwrap(), false, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_3_true_false() {
|
|
test_queue(NonZero::new(3).unwrap(), true, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_3_true_true() {
|
|
test_queue(NonZero::new(3).unwrap(), true, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_4_false_false() {
|
|
test_queue(NonZero::new(4).unwrap(), false, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_4_false_true() {
|
|
test_queue(NonZero::new(4).unwrap(), false, true);
|
|
}
|
|
|
|
#[test]
|
|
fn test_4_true_false() {
|
|
test_queue(NonZero::new(4).unwrap(), true, false);
|
|
}
|
|
|
|
#[test]
|
|
fn test_4_true_true() {
|
|
test_queue(NonZero::new(4).unwrap(), true, true);
|
|
}
|
|
}
|