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

Initial work on representing HDL and formal verification in Rocq. #56

Merged
programmerjake merged 3 commits from cesar/fayalite:rocq_hdl into master 2025-12-09 16:34:36 +00:00
Conversation 1 Commits 3 Files changed 2 +175
cesar commented 2025-12-09 01:11:40 +00:00
Owner
Copy link

I guess I'm ready to push my work on Rocq so far.

I guess I'm ready to push my work on Rocq so far.
cesar added 2 commits 2025-12-09 01:11:41 +00:00 
Starts with a very simple example, including a proof by induction.
Demonstrates state with multiple variables and hidden state.
Some checks failed
/ test (pull_request) Failing after 22s
Details
e54558d848
programmerjake commented 2025-12-09 01:18:05 +00:00
Owner
Copy link

as you probably saw, you'll also need to add the code for checking for copyright headers to
scripts/check-copyright.sh

as you probably saw, you'll also need to add the code for checking for copyright headers to `scripts/check-copyright.sh`
cesar added 1 commit 2025-12-09 10:48:05 +00:00
Check copyright header in Rocq files.
All checks were successful
/ test (pull_request) Successful in 4m4s
Details
/ test (push) Successful in 4m39s
Details
e4210a672f 
If we ever add Verilog files, we can "or" both results, I guess.
programmerjake merged commit e4210a672f into master 2025-12-09 16:34:36 +00:00
Sign in to join this conversation.
Reviewers
No reviewers
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#56
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?