fayalite

Define design safety, and prove it for 1-step and 2-step induction.

test.yml #350 -Commit a398f8f185 pushed by cesar

master

2025-12-24 20:13:49 +00:00

4m36s

Define design safety, and prove it for 1-step and 2-step induction.

test.yml #349 -Commit a398f8f185 pushed by cesar

#59

2025-12-23 01:57:56 +00:00

4m8s

Check copyright header in Rocq files.

test.yml #341 -Commit e4210a672f pushed by cesar

#56

2025-12-09 10:52:10 +00:00

4m4s

Demonstrates state with multiple variables and hidden state.

test.yml #340 -Commit e54558d848 pushed by cesar

#56

2025-12-09 01:12:08 +00:00

24s

Gather the FIFO debug ports in a bundle

test.yml #220 -Commit 3771cea78e pushed by cesar

#11

2024-12-29 16:37:56 +00:00

3m53s

Gather the FIFO debug ports in a bundle

test.yml #219 -Commit 3771cea78e pushed by cesar

fifo-proof

2024-12-29 16:34:03 +00:00

3m57s

Grammar fix.

test.yml #212 -Commit 8d7c691002 pushed by cesar

#11

2024-12-26 22:48:13 +00:00

3m53s

Gather the FIFO debug ports in a bundle

test.yml #211 -Commit 9f0fb0188a pushed by cesar

#11

2024-12-26 18:06:00 +00:00

3m54s

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

test.yml #210 -Commit ad1101934c pushed by cesar

#11

2024-12-26 14:06:06 +00:00

3m57s

Initial queue formal proof based on one-entry FIFO equivalence

test.yml #209 -Commit fef7fea3ea pushed by cesar

#11

2024-12-24 11:10:43 +00:00

5m10s

add module exercising formal verification of memories

test.yml #180 -Commit 2e7d685dc7 pushed by cesar

#7

2024-12-08 20:52:04 +00:00

17m31s

Add test module exercising formal verification.

test.yml #126 -Commit c1f1a8b749 pushed by cesar

#2

2024-11-20 21:40:00 +00:00

5m6s

Add test module exercising formal verification.

test.yml #124 -Commit 39d895764a pushed by cesar

#2

2024-11-20 21:11:40 +00:00

5m8s