cesar
0 followers · 0 following
  • Joined on 2024-07-18
Repositories
1
 Projects Packages Public activity Starred repositories
cesar deleted branch rocq_playground from cesar/fayalite 2025-12-26 11:10:42 +00:00
cesar pushed to master at libre-chip/fayalite 2025-12-24 20:09:12 +00:00
a398f8f185 Define design safety, and prove it for 1-step and 2-step induction.
4fd4371054 Spelling.
Compare 2 commits »
cesar merged pull request libre-chip/fayalite#59 2025-12-24 20:09:11 +00:00
Formally define design safety, and prove it for 1-step and 2-step induction
cesar created pull request libre-chip/fayalite#59 2025-12-23 01:53:46 +00:00
Formally define design safety, and prove it for 1-step and 2-step induction
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-23 01:33:16 +00:00
a398f8f185 Define design safety, and prove it for 1-step and 2-step induction.
4fd4371054 Spelling.
c97b44d9d6 simplify SimValue Debug format, making complex structures much easier to read
fbe4585578 add FillInDefaultedGenerics<Type = Self> bound for SizeType
Compare 4 commits »
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-09 10:48:04 +00:00
e4210a672f Check copyright header in Rocq files.
cesar created pull request libre-chip/fayalite#56 2025-12-09 01:11:41 +00:00
Initial work on representing HDL and formal verification in Rocq.
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-09 01:01:04 +00:00
e54558d848 Demonstrates state with multiple variables and hidden state.
cesar pushed to rocq_playground at cesar/fayalite 2025-12-09 00:51:10 +00:00
c32cdee4f7 Format,
02de335e46 Demonstrate a preliminary mapping from HDL to Rocq.
Compare 2 commits »
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-09 00:43:10 +00:00
a6302867d7 Demonstrates state with multiple variables and hidden state.
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-08 22:32:36 +00:00
46f3519c76 Demonstrate a preliminary mapping from HDL to Rocq.
cesar created branch rocq_hdl in cesar/fayalite 2025-12-08 22:29:56 +00:00
cesar pushed to rocq_hdl at cesar/fayalite 2025-12-08 22:29:56 +00:00
02de335e46 Demonstrate a preliminary mapping from HDL to Rocq.
cesar commented on pull request libre-chip/website#1 2025-11-30 14:04:12 +00:00
add grant proposal: Libre-Chip's CPU with a Programmable Decoder to Run Multiple ISAs at Full Speed

Suggestion: "€ 10000 Get the fallback emulator to work" -> "€ 10000 Get the fallback software decoder and the software instruction emulator to work"

Otherwise looks good.

cesar created branch rocq_playground in cesar/fayalite 2025-11-25 01:01:59 +00:00
cesar pushed to rocq_playground at cesar/fayalite 2025-11-25 01:01:59 +00:00
17964b6224 WIP
9e803223d0 support operations directly on SimValue, UIntValue, and SIntValue, and shared references to those
2a65aa2bd5 fix DynShr[SU]'s literal bits to properly shift right instead of left
2817cd3d58 support Rust's default binding modes when destructuring with #[hdl(sim)] let/match
053c1b2b10 implement Display for SimValue<T>
Compare 10 commits »
cesar commented on issue libre-chip/grant-tracking#7 2025-09-10 17:12:29 +00:00
NLnet 2024-12-324 Add to the simulator in Fayalite the ability to transfer non-HDL data (e.g. HashMap) through the digital signalling mechanism, this allows using those data types when writing procedural models.

Looks good to me. CI passes, good. There is a test, which also serves as an example. In the RfP, I suggest linking directly to the pull request (which has a link to the CI), instead of this…

cesar commented on pull request libre-chip/grant-tracking#1 2025-08-25 16:50:22 +00:00
fill out grant tracking structure

@programmerjake wrote in libre-chip/grant-tracking#1 (comment):

@cesar what do you think of having an issue on this repo for each subtask?

Sure, go for it.

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