cesar/fayalite
1
0
Fork 0
forked from libre-chip/fayalite
Code Pull requests Activity Actions

switch ready_valid::queue formal proofs to use formal_global_clock

Browse source
This commit is contained in:
Jacob Lifshay 2026-06-05 00:41:51 -07:00
parent d4d9706798
commit ffca1a279d
Signed by: programmerjake
SSH key fingerprint: SHA256:HnFTLGpSm4Q4Fj502oCFisjZSoakwEuTsJJMSke63RQ
1 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

34
crates/fayalite/src/util/ready_valid.rs
View file

@ -241,15 +241,13 @@ mod tests {
/// happens to be in phase with the offending input or output).
#[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,
clk: formal_global_clock(),
rst: formal_reset().to_reset(),
},
);
@ -280,7 +278,7 @@ mod tests {
#[hdl]
let index_to_check = wire(index_ty);
connect(index_to_check, any_const(index_ty));
hdl_assume(clk, index_to_check.cmp_lt(capacity.get()), "");
hdl_assume(cd.clk, index_to_check.cmp_lt(capacity.get()), "");
// instantiate and connect the queue
#[hdl]
@ -300,13 +298,13 @@ mod tests {
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()), "");
hdl_assert(cd.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()), "");
hdl_assert(cd.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), "");
hdl_assert(cd.clk, expected_count_reg.cmp_eq(dut.count), "");
// keep an independent write index into the FIFO's circular buffer
#[hdl]
@ -374,7 +372,7 @@ mod tests {
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), ""),
HdlNone => hdl_assert(cd.clk, HdlOption::is_none(out_firing_data), ""),
// If we are indeed receiving some data...
HdlSome(data_in) => {
#[hdl]
@ -382,7 +380,9 @@ mod tests {
// ... 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), ""),
HdlSome(data_out) => {
hdl_assert(cd.clk, data_out.cmp_eq(data_in), "")
}
// If we are receiving, but not transmitting,
// store the received data in the holding
// register.
@ -397,11 +397,11 @@ mod tests {
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), ""),
HdlNone => hdl_assert(cd.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), "");
hdl_assert(cd.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);
@ -417,17 +417,17 @@ mod tests {
connect(dut.dbg.index_to_check, index_to_check);
#[hdl]
if let HdlSome(stored) = stored_reg {
hdl_assert(clk, stored.cmp_eq(dut.dbg.stored), "");
hdl_assert(cd.clk, stored.cmp_eq(dut.dbg.stored), "");
}
// sync the read and write indices
hdl_assert(clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
hdl_assert(clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
hdl_assert(cd.clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
hdl_assert(cd.clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
// the indices should never go past the capacity, but induction
// doesn't know that...
hdl_assert(clk, inp_index_reg.cmp_lt(capacity.get()), "");
hdl_assert(clk, out_index_reg.cmp_lt(capacity.get()), "");
hdl_assert(cd.clk, inp_index_reg.cmp_lt(capacity.get()), "");
hdl_assert(cd.clk, out_index_reg.cmp_lt(capacity.get()), "");
// strongly constrain the state of the holding register
//
@ -455,7 +455,7 @@ mod tests {
connect(expected_stored, pending_reads.cmp_lt(dut.count));
// sync with the state of the holding register
hdl_assert(
clk,
cd.clk,
expected_stored.cmp_eq(HdlOption::is_some(stored_reg)),
"",
);