libre-chip/fayalite
2
0
Fork 2
Code Issues 1 Pull requests Actions Packages Projects Releases Wiki Activity

Queue formal proof based on one-entry FIFO equivalence #11

Merged
programmerjake merged 3 commits from cesar/fayalite:fifo-proof into master 2024-12-29 21:05:26 +00:00
Conversation 3 Commits 3 Files changed 1 +22 -18
1 changed files with 22 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files
Showing only changes of commit 3771cea78e - Show all commits

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

@ -49,6 +49,18 @@ impl<T: Type> ReadyValid<T> {
}
}
/// This debug port is only meant to assist the formal proof of the queue.
#[cfg(test)]
#[doc(hidden)]
#[hdl]
programmerjake marked this conversation as resolved Outdated
programmerjake commented 2024-12-26 21:07:54 +00:00
Outdated
Review
Copy link

this should also be marked #[cfg(test)] since it only needs to be there when running the tests.

this should also be marked `#[cfg(test)]` since it only needs to be there when running the tests.
cesar commented 2024-12-26 22:25:40 +00:00
Outdated
Review
Copy link

Could you please try it on your end? If I do it, cargo check gives me an error:

error[E0412]: cannot find type `QueueDebugPort` in this scope
   --> crates/fayalite/src/util/ready_valid.rs:198:18
    |
198 |         let dbg: QueueDebugPort<T, UInt> = m.output(QueueDebugPort[ty][index_ty]);
    |                  ^^^^^^^^^^^^^^ not found in this scope

Note that the above code is also in a #[cfg(test)] block, the error makes no sense to me.

Could you please try it on your end? If I do it, `cargo check` gives me an error: ``` error[E0412]: cannot find type `QueueDebugPort` in this scope --> crates/fayalite/src/util/ready_valid.rs:198:18 | 198 | let dbg: QueueDebugPort<T, UInt> = m.output(QueueDebugPort[ty][index_ty]); | ^^^^^^^^^^^^^^ not found in this scope ``` Note that the above code is also in a `#[cfg(test)]` block, the error makes no sense to me.
programmerjake commented 2024-12-26 22:36:25 +00:00
Outdated
Review
Copy link

ah, the #[hdl_module] macro doesn't properly handle additional attributes on IO ports...i'll work on fixing that soon, probably today. basically it generates an #[hdl] struct from the list of IO ports but doesn't copy attributes to that struct's fields. though, i think the #[hdl] macro doesn't handle #[cfg(...)] on fields either...i'll fix that too.

ah, the `#[hdl_module]` macro doesn't properly handle additional attributes on IO ports...i'll work on fixing that soon, probably today. basically it generates an `#[hdl] struct` from the list of IO ports but doesn't copy attributes to that struct's fields. though, i think the `#[hdl]` macro doesn't handle `#[cfg(...)]` on fields either...i'll fix that too.
programmerjake commented 2024-12-26 22:38:43 +00:00
Outdated
Review
Copy link

if you fix the grammar mistakes, i'll merge this (edit: nvm it's broken due to #[cfg(...)] not working correctly) and will fix the #[cfg(...)] stuff later when i fix the #[hdl] and #[hdl_module] attribute macros.

if you fix the grammar mistakes, i'll merge this (edit: nvm it's broken due to `#[cfg(...)]` not working correctly) and will fix the `#[cfg(...)]` stuff later when i fix the `#[hdl]` and `#[hdl_module]` attribute macros.
programmerjake commented 2024-12-26 22:44:58 +00:00
Outdated
Review
Copy link

actually, since it doesn't properly handle #[cfg(...)], the #[cfg(test)] block will make queue unusable outside of running fayalite's tests, since the generated struct will still have the debugging port's field, but the module's body won't so it'll cause an assertion failure if you try to use the module.
so, i'll wait on merging this until the #[cfg(...)] stuff gets fixed. sorry

actually, since it doesn't properly handle `#[cfg(...)]`, the `#[cfg(test)]` block will make `queue` unusable outside of running `fayalite`'s tests, since the generated struct will still have the debugging port's field, but the module's body won't so it'll cause an assertion failure if you try to use the module. so, i'll wait on merging this until the `#[cfg(...)]` stuff gets fixed. sorry
programmerjake commented 2024-12-29 09:54:54 +00:00
Outdated
Review
Copy link

ok, I got it to work when adding #[cfg(test)] and merging in the latest master. if you want to rebase on master, i can merge this.

ok, I got it to work when adding `#[cfg(test)]` and merging in the latest master. if you want to rebase on master, i can merge this.
cesar commented 2024-12-29 16:52:38 +00:00
Outdated
Review
Copy link

ok, I got it to work when adding #[cfg(test)] and merging in the latest master. if you want to rebase on master, i can merge this.

Rebased on master. Took the opportunity to fix the issues directly on the commits that introduced them.

Ended up pushing a "fifo-proof" branch on the main repository by mistake, sorry about that. Already deleted the branch. Master was not affected.

> ok, I got it to work when adding `#[cfg(test)]` and merging in the latest master. if you want to rebase on master, i can merge this. Rebased on master. Took the opportunity to fix the issues directly on the commits that introduced them. Ended up pushing a "fifo-proof" branch on the main repository by mistake, sorry about that. Already deleted the branch. Master was not affected.
pub struct QueueDebugPort<Element, Index> {
#[hdl(flip)]
index_to_check: Index,
stored: Element,
inp_index: Index,
out_index: Index,
}
#[hdl_module]
pub fn queue<T: Type>(
ty: T,
@ -180,27 +192,19 @@ pub fn queue<T: Type>(
}
// These debug ports expose some internal state during the Induction phase
// of Formal Verification. They are not present in normal use.
//
// TODO: gather the new debug ports in a bundle
#[cfg(test)]
{
#[hdl]
let dbg: QueueDebugPort<T, UInt> = m.output(QueueDebugPort[ty][index_ty]);
programmerjake marked this conversation as resolved Outdated
programmerjake commented 2024-12-24 17:42:36 +00:00
Outdated
Review
Copy link

imo this should be changed this back to Prove before merging. ah, you already said that...

imo this should be changed this back to Prove before merging. ah, you already said that...
// read the memory word currently stored at some fixed index
let debug_port = mem.new_read_port();
#[hdl]
let dbg_index_to_check: UInt = m.input(index_ty);
#[hdl]
let dbg_stored: T = m.output(ty);
connect(debug_port.addr, dbg_index_to_check);
connect(debug_port.addr, dbg.index_to_check);
connect(debug_port.en, true);
connect(debug_port.clk, cd.clk);
connect(dbg_stored, debug_port.data);
connect(dbg.stored, debug_port.data);
// also expose the current read and write indices
#[hdl]
let dbg_inp_index: UInt = m.output(index_ty);
#[hdl]
let dbg_out_index: UInt = m.output(index_ty);
connect(dbg_inp_index, inp_index_reg);
connect(dbg_out_index, out_index_reg);
connect(dbg.inp_index, inp_index_reg);
connect(dbg.out_index, out_index_reg);
}
}
@ -412,15 +416,15 @@ mod tests {
// sync the holding register, when it's occupied, to the
// corresponding entry in the FIFO's circular buffer
connect(dut.dbg_index_to_check, index_to_check);
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(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(clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
hdl_assert(clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
// the indices should never go past the capacity, but induction
// doesn't know that...