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

cesar · 2024-12-24T11:05:29Z

cesar commented

2024-12-24 11:05:29 +00:00

As it turns out, by filtering the observed input and output streams of a FIFO to consider just one in every N reads and writes (where N is the FIFO capacity), we can indeed reduce it to an one-entry FIFO, which is much easier to verify.

In particular, any counterexample of the FIFO behaving badly would be caught by one of the filtered versions (one which happens to be in phase with the offending input or output).

I do think the idea would be better explained in more details in a separate web page, instead of terse comments in the source code.

In this branch, I'm rewriting the existing FIFO proof to use this method. Or, maybe we could keep both versions? I do expect it to complete much faster, though.

Also, I replaced the hard-coded maximum bit-length of indices and counters (32 bits) by parameterized ones, I see no reason not to.

For now, I only checked the proof in Bounded Model Check mode. I'll start on Induction next. Like all designs involving memory, I'm expecting it to be somewhat intrusive to the queue module, unless we move the full proof inside of it.

As it turns out, by filtering the observed input and output streams of a FIFO to consider just one in every N reads and writes (where N is the FIFO capacity), we can indeed reduce it to an one-entry FIFO, which is much easier to verify. In particular, any counterexample of the FIFO behaving badly would be caught by one of the filtered versions (one which happens to be in phase with the offending input or output). I do think the idea would be better explained in more details in a separate web page, instead of terse comments in the source code. In this branch, I'm rewriting the existing FIFO proof to use this method. Or, maybe we could keep both versions? I do expect it to complete much faster, though. Also, I replaced the hard-coded maximum bit-length of indices and counters (32 bits) by parameterized ones, I see no reason not to. For now, I only checked the proof in Bounded Model Check mode. I'll start on Induction next. Like all designs involving memory, I'm expecting it to be somewhat intrusive to the queue module, unless we move the full proof inside of it.

cesar added 1 commit 2024-12-24 11:05:31 +00:00

Initial queue formal proof based on one-entry FIFO equivalence

/ deps (pull_request) Successful in 18s

Details

/ test (pull_request) Successful in 4m48s

Details

fef7fea3ea

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.

programmerjake reviewed 2024-12-24 17:42:36 +00:00

crates/fayalite/src/util/ready_valid.rs Outdated

					
				@ -196,3 +196,3 @@

				            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,

				            FormalMode::BMC,

programmerjake commented

2024-12-24 17:42:36 +00:00

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

programmerjake marked this conversation as resolved

programmerjake commented

2024-12-24 17:52:06 +00:00

if you're going to change the queue module's interface (adding more outputs for tests), please mark them with #[cfg(test)] and #[doc(hidden)] since they aren't intended to be available when just using the queue

if you're going to change the queue module's interface (adding more outputs for tests), please mark them with `#[cfg(test)]` and `#[doc(hidden)]` since they aren't intended to be available when just using the queue

cesar added 1 commit 2024-12-26 14:02:07 +00:00

Add assertions and debug ports in order for the FIFO to pass induction

/ deps (pull_request) Successful in 21s

Details

/ test (pull_request) Successful in 3m32s

Details

ad1101934c

As some proofs involving memories, it is necessary to add more ports to
the queue interface, to sync state. These changes are predicated on the
test environment, so normal use is not affected.

Since some speedup is achieved, use the saved time to test with a deeper
FIFO.

cesar added 1 commit 2024-12-26 18:02:03 +00:00

Gather the FIFO debug ports in a bundle

/ deps (pull_request) Successful in 18s

Details

/ test (pull_request) Successful in 3m32s

Details

9f0fb0188a

For some reason, can't mark QueueDebugPort as #[cfg(test)].

cesar changed title from ~~WIP: Queue formal proof based on one-entry FIFO equivalence~~ to Queue formal proof based on one-entry FIFO equivalence

2024-12-26 18:08:03 +00:00

cesar commented

2024-12-26 18:27:46 +00:00

The induction proof works! I think my work is complete on this branch.

programmerjake requested changes 2024-12-26 21:20:12 +00:00

programmerjake left a comment

nice! there's some minor issues then I think it's ready to merge!

crates/fayalite/src/util/ready_valid.rs Outdated

					
				@ -52,0 +52,4 @@

				/// This debug port is only meant to assist the formal proof of the queue.

				#[doc(hidden)]

				#[hdl]

				pub struct QueueDebugPort<Element, Index> {

programmerjake commented

2024-12-26 21:07:54 +00:00

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

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

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

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

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

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

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.

programmerjake marked this conversation as resolved

crates/fayalite/src/util/ready_valid.rs Outdated

					
				@ -206,0 +235,4 @@

				        /// 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.

programmerjake commented

2024-12-26 21:18:57 +00:00

here use a one-entry -- the o makes a w sound so is treated as a consonant for a vs. an

here use `a one-entry` -- [the `o` makes a `w` sound so is treated as a consonant for `a` vs. `an`](https://owl.purdue.edu/owl/general_writing/grammar/articles_a_versus_an.html#:~:text=or%20%22o%22%20makes%20the%20same%20sound%20as%20%22w%22%20in%20%22won%2C)

programmerjake marked this conversation as resolved

crates/fayalite/src/util/ready_valid.rs Outdated

					
				@ -318,0 +361,4 @@

				                connect(out_firing_data, ReadyValid::firing_data(dut.out));

				            }

				            // Implement an one-entry FIFO and ensure its equivalence to the