cesar
0 followers · 0 following
  • Joined on 2024-07-18
Repositories
1
 Projects Packages Public activity Starred repositories
cesar commented on pull request libre-chip/fayalite#11 2024-12-29 16:52:38 +00:00
Queue formal proof based on one-entry FIFO equivalence

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…

cesar deleted branch fifo-proof from libre-chip/fayalite 2024-12-29 16:31:52 +00:00
cesar pushed to fifo-proof at cesar/fayalite 2024-12-29 16:30:41 +00:00
3771cea78e Gather the FIFO debug ports in a bundle
dcf865caec Add assertions and debug ports in order for the FIFO to pass induction
31d01046a8 Initial queue formal proof based on one-entry FIFO equivalence
c16726cee6 fix #[hdl]/#[hdl_module] attributes getting the wrong hygiene when processing #[cfg]s
b63676d0ca add test for cfgs
Compare 7 commits »
cesar created branch fifo-proof in libre-chip/fayalite 2024-12-29 16:30:04 +00:00
cesar pushed to fifo-proof at libre-chip/fayalite 2024-12-29 16:30:04 +00:00
3771cea78e Gather the FIFO debug ports in a bundle
dcf865caec Add assertions and debug ports in order for the FIFO to pass induction
31d01046a8 Initial queue formal proof based on one-entry FIFO equivalence
Compare 3 commits »
cesar pushed to fifo-proof at cesar/fayalite 2024-12-26 22:44:17 +00:00
8d7c691002 Grammar fix.
cesar commented on pull request libre-chip/fayalite#11 2024-12-26 22:25:40 +00:00
Queue formal proof based on one-entry FIFO equivalence

Can you 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
…
cesar commented on pull request libre-chip/fayalite#11 2024-12-26 18:27:46 +00:00
Queue formal proof based on one-entry FIFO equivalence

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

cesar pushed to fifo-proof at cesar/fayalite 2024-12-26 18:02:02 +00:00
9f0fb0188a Gather the FIFO debug ports in a bundle
cesar pushed to fifo-proof at cesar/fayalite 2024-12-26 14:02:06 +00:00
ad1101934c Add assertions and debug ports in order for the FIFO to pass induction
cesar created pull request libre-chip/fayalite#11 2024-12-24 11:05:31 +00:00
WIP: Queue formal proof based on one-entry FIFO equivalence
cesar pushed to fifo-proof at cesar/fayalite 2024-12-24 10:08:20 +00:00
fef7fea3ea Initial queue formal proof based on one-entry FIFO equivalence
cesar created branch fifo-proof in cesar/fayalite 2024-12-23 17:27:31 +00:00
cesar pushed to fifo-proof at cesar/fayalite 2024-12-23 17:27:31 +00:00
3dc82c4804 Initial queue formal proof based on one-entry FIFO equivalence
9b06019bf5 make sim::Compiler not print things to stdout unless you ask for it
36bad52978 sim: fix sim.write to struct
21c73051ec sim: add SimValue and reading/writing more than just a scalar
304d8da0e8 Merge remote-tracking branch 'origin/master' into adding-simulator
Compare 10 commits »
cesar created pull request libre-chip/fayalite#7 2024-12-08 20:25:22 +00:00
Add module exercising formal verification of memories
cesar pushed to formal_memories at cesar/fayalite 2024-12-08 20:14:15 +00:00
2e7d685dc7 add module exercising formal verification of memories
cesar created branch formal_memories in cesar/fayalite 2024-12-08 18:27:58 +00:00
cesar pushed to formal_memories at cesar/fayalite 2024-12-08 18:27:58 +00:00
4f6bc1032f add module exercising formal verification of memories
c45624e3c2 Fix SInt::for_value not accounting for sign bit for positive values
3ea0d98924 always write formal cache json
Compare 3 commits »
cesar opened issue libre-chip/fayalite#4 2024-11-26 22:44:21 +00:00
Incorrect number of bits for signed range
cesar pushed to formal_test_case at cesar/fayalite 2024-11-20 21:34:53 +00:00
c1f1a8b749 Add test module exercising formal verification.