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

Formally define design safety, and prove it for 1-step and 2-step induction #59

Merged
cesar merged 2 commits from cesar/fayalite:rocq_hdl into master 2025-12-24 20:09:11 +00:00
Conversation 2 Commits 2 Files changed 1 +220 -6
cesar commented 2025-12-23 01:53:46 +00:00
Owner
Copy link

Continuing from the simple earlier designs, I remove a limitation in that I proved the base and inductive cases for those designs, but didn't actually proved them to be safe (or even defined in Rocq what it meant to be safe). It also opens an opportunity to prove safety in other possible ways maybe. As an example, I prove soundness of the algorithm, which is used in Symbiyosys, for the particular cases of 1-step and 2-step induction.

Continuing from the simple earlier designs, I remove a limitation in that I proved the base and inductive cases for those designs, but didn't actually proved them to be safe (or even defined in Rocq what it meant to be safe). It also opens an opportunity to prove safety in other possible ways maybe. As an example, I prove soundness of the algorithm, which is used in Symbiyosys, for the particular cases of 1-step and 2-step induction.
cesar added 2 commits 2025-12-23 01:53:46 +00:00
Define design safety, and prove it for 1-step and 2-step induction.
All checks were successful
/ test (pull_request) Successful in 4m8s
Details
/ test (push) Successful in 4m35s
Details
a398f8f185
programmerjake approved these changes 2025-12-23 01:59:30 +00:00
programmerjake left a comment
Owner
Copy link

It'd be nice to add running Rocq to CI, but that can be left for a future PR

It'd be nice to add running Rocq to CI, but that can be left for a future PR
programmerjake commented 2025-12-24 15:39:24 +00:00
Owner
Copy link

so I'm clear, I approved this PR which I intend to mean that, if you think the current changes are good, feel free to merge them by clicking the "fast-forward" button.

so I'm clear, I approved this PR which I intend to mean that, if you think the current changes are good, feel free to merge them by clicking the "fast-forward" button.
👍 1
cesar merged commit a398f8f185 into master 2025-12-24 20:09:11 +00:00
Sign in to join this conversation.
Reviewers
No reviewers
programmerjake
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: libre-chip/fayalite#59
No description provided.
Delete branch "cesar/fayalite:rocq_hdl"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?