419 lines
12 KiB
Rust
419 lines
12 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 fire(expr: Expr<Self>) -> Expr<Bool> {
|
|
#[hdl]
|
|
let fire: Bool = wire();
|
|
#[hdl]
|
|
match expr.data {
|
|
HdlNone => connect(fire, false),
|
|
HdlSome(_) => connect(fire, expr.ready),
|
|
}
|
|
fire
|
|
}
|
|
#[hdl]
|
|
pub fn fire_data(expr: impl ToExpr<Type = Self>) -> Expr<HdlOption<T>> {
|
|
let expr = expr.to_expr();
|
|
let option_ty = Expr::ty(expr).data;
|
|
#[hdl]
|
|
let fire_data = wire(option_ty);
|
|
connect(fire_data, option_ty.HdlNone());
|
|
#[hdl]
|
|
if expr.ready {
|
|
connect(fire_data, expr.data);
|
|
}
|
|
fire_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_builder().clock_domain(cd).reset(0.cast_to(index_ty));
|
|
#[hdl]
|
|
let out_index = reg_builder().clock_domain(cd).reset(0.cast_to(index_ty));
|
|
#[hdl]
|
|
let maybe_full = 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_fire: Bool = wire();
|
|
connect(inp_fire, ReadyValid::fire(inp));
|
|
#[hdl]
|
|
let out_fire: Bool = wire();
|
|
connect(out_fire, ReadyValid::fire(out));
|
|
#[hdl]
|
|
let indexes_equal: Bool = wire();
|
|
connect(indexes_equal, inp_index.cmp_eq(out_index));
|
|
#[hdl]
|
|
let empty: Bool = wire();
|
|
connect(empty, indexes_equal & !maybe_full);
|
|
#[hdl]
|
|
let full: Bool = wire();
|
|
connect(full, indexes_equal & maybe_full);
|
|
|
|
connect(read_port.addr, out_index);
|
|
connect(read_port.en, true);
|
|
connect(read_port.clk, cd.clk);
|
|
connect(write_port.addr, inp_index);
|
|
connect(write_port.en, inp_fire);
|
|
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_fire.cmp_ne(out_fire) {
|
|
connect(maybe_full, inp_fire);
|
|
}
|
|
|
|
#[hdl]
|
|
if inp_fire {
|
|
#[hdl]
|
|
if inp_index.cmp_eq(capacity.get() - 1) {
|
|
connect_any(inp_index, 0_hdl_u0);
|
|
} else {
|
|
connect_any(inp_index, inp_index + 1_hdl_u1);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if out_fire {
|
|
#[hdl]
|
|
if out_index.cmp_eq(capacity.get() - 1) {
|
|
connect_any(out_index, 0_hdl_u0);
|
|
} else {
|
|
connect_any(out_index, out_index + 1_hdl_u1);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if indexes_equal {
|
|
#[hdl]
|
|
if maybe_full {
|
|
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 - out_index).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.cmp_lt(out_index) {
|
|
connect(count, inp_index + capacity - out_index);
|
|
} else {
|
|
connect(count, inp_index - out_index);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
#[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::Prove,
|
|
14,
|
|
None,
|
|
ExportOptions {
|
|
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
|
|
..ExportOptions::default()
|
|
},
|
|
);
|
|
#[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(),
|
|
},
|
|
);
|
|
#[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());
|
|
}
|
|
#[hdl]
|
|
let out_ready: Bool = wire();
|
|
connect(out_ready, any_seq(Bool));
|
|
let index_ty: UInt<32> = UInt::TYPE;
|
|
#[hdl]
|
|
let index_to_check = wire();
|
|
connect(index_to_check, any_const(index_ty));
|
|
let index_max = !index_ty.zero();
|
|
// we saturate at index_max, so only check indexes where we properly maintain position
|
|
hdl_assume(clk, index_to_check.cmp_ne(index_max), "");
|
|
#[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);
|
|
hdl_assume(
|
|
clk,
|
|
index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()),
|
|
"",
|
|
);
|
|
|
|
#[hdl]
|
|
let expected_count = reg_builder().clock_domain(cd).reset(0u32);
|
|
#[hdl]
|
|
let next_expected_count = wire();
|
|
connect(next_expected_count, expected_count);
|
|
connect(expected_count, next_expected_count);
|
|
#[hdl]
|
|
if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) {
|
|
connect_any(next_expected_count, expected_count + 1u8);
|
|
} else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) {
|
|
connect_any(next_expected_count, expected_count - 1u8);
|
|
}
|
|
hdl_assert(cd.clk, expected_count.cmp_eq(dut.count), "");
|
|
|
|
#[hdl]
|
|
let prev_out_ready = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
|
|
connect_any(
|
|
prev_out_ready,
|
|
(prev_out_ready << 1) | out_ready.cast_to(UInt[1]),
|
|
);
|
|
#[hdl]
|
|
let prev_inp_valid = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
|
|
connect_any(
|
|
prev_inp_valid,
|
|
(prev_inp_valid << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]),
|
|
);
|
|
hdl_assume(clk, (prev_out_ready & prev_inp_valid).cmp_ne(0u8), "");
|
|
|
|
#[hdl]
|
|
let inp_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
|
|
#[hdl]
|
|
let stored_inp_data = reg_builder().clock_domain(cd).reset(0u8);
|
|
|
|
#[hdl]
|
|
if let HdlSome(data) = ReadyValid::fire_data(dut.inp) {
|
|
#[hdl]
|
|
if inp_index.cmp_lt(index_max) {
|
|
connect_any(inp_index, inp_index + 1u8);
|
|
#[hdl]
|
|
if inp_index.cmp_eq(index_to_check) {
|
|
connect(stored_inp_data, data);
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if inp_index.cmp_lt(index_to_check) {
|
|
hdl_assert(clk, stored_inp_data.cmp_eq(0u8), "");
|
|
}
|
|
|
|
#[hdl]
|
|
let out_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
|
|
#[hdl]
|
|
let stored_out_data = reg_builder().clock_domain(cd).reset(0u8);
|
|
|
|
#[hdl]
|
|
if let HdlSome(data) = ReadyValid::fire_data(dut.out) {
|
|
#[hdl]
|
|
if out_index.cmp_lt(index_max) {
|
|
connect_any(out_index, out_index + 1u8);
|
|
#[hdl]
|
|
if out_index.cmp_eq(index_to_check) {
|
|
connect(stored_out_data, data);
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
if out_index.cmp_lt(index_to_check) {
|
|
hdl_assert(clk, stored_out_data.cmp_eq(0u8), "");
|
|
}
|
|
|
|
hdl_assert(clk, inp_index.cmp_ge(out_index), "");
|
|
|
|
#[hdl]
|
|
if inp_index.cmp_lt(index_max) & out_index.cmp_lt(index_max) {
|
|
hdl_assert(clk, expected_count.cmp_eq(inp_index - out_index), "");
|
|
} else {
|
|
hdl_assert(clk, expected_count.cmp_ge(inp_index - out_index), "");
|
|
}
|
|
|
|
#[hdl]
|
|
if inp_index.cmp_gt(index_to_check) & out_index.cmp_gt(index_to_check) {
|
|
hdl_assert(clk, stored_inp_data.cmp_eq(stored_out_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);
|
|
}
|
|
}
|