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

add cpu::test::decode_and_run_single_insn and some formal tests of running PowerISA instructions #15

Merged
programmerjake merged 17 commits from programmerjake/cpu:decode-and-test-harness into master 2026-06-19 03:57:09 +00:00
Conversation 0 Commits 17 Files changed 39 +855063 -110566
programmerjake commented 2026-06-01 08:11:18 +00:00
Owner
Copy link

Add a simple HDL module that decodes a single instruction and then runs it one µOp at a time, intended for testing the Units in formal proofs.

Contains a bug fix for unit::alu_branch::add_sub: actually add in carry_in

Formal tests for instructions so far:

  • addi 3, 4, imm
  • paddi 3, 4, imm, R
  • addis 3, 4, imm
  • addpcis 3, imm
  • add[c|e][o][.] 3, 3, 4
  • subf[c|e][o][.] 3, 3, 4
  • addic[.] 3, 4, imm
  • subfic 3, 4, imm
  • addme[o][.] 3, 4
  • addze[o][.] 3, 4
  • subfme[o][.] 3, 4
  • subfze[o][.] 3, 4
  • neg[o][.] 3, 4
Add a simple HDL module that decodes a single instruction and then runs it one µOp at a time, intended for testing the Units in formal proofs. Contains a bug fix for `unit::alu_branch::add_sub`: actually add in `carry_in` Formal tests for instructions so far: * `addi 3, 4, imm` * `paddi 3, 4, imm, R` * `addis 3, 4, imm` * `addpcis 3, imm` * `add[c|e][o][.] 3, 3, 4` * `subf[c|e][o][.] 3, 3, 4` * `addic[.] 3, 4, imm` * `subfic 3, 4, imm` * `addme[o][.] 3, 4` * `addze[o][.] 3, 4` * `subfme[o][.] 3, 4` * `subfze[o][.] 3, 4` * `neg[o][.] 3, 4`
programmerjake added 4 commits 2026-06-01 08:11:18 +00:00
programmerjake added 3 commits 2026-06-02 08:39:21 +00:00
programmerjake force-pushed decode-and-test-harness from 241255e12c to 9cc556c988 2026-06-05 08:38:06 +00:00 Compare
programmerjake force-pushed decode-and-test-harness from 9cc556c988 to ef30d325d5 2026-06-06 02:47:14 +00:00 Compare
programmerjake added 2 commits 2026-06-14 08:47:59 +00:00
update generated vcd
All checks were successful
/ test (pull_request) Successful in 22m39s
Details
999860b507
programmerjake added 1 commit 2026-06-15 02:26:54 +00:00
update fayalite to speed up big formal proofs
All checks were successful
/ test (pull_request) Successful in 10m58s
Details
51d71c56f6
programmerjake added 1 commit 2026-06-17 04:12:03 +00:00
tests/units_formal: prove more addition instructions -- [p]addi and add[c][o][.]
All checks were successful
/ test (pull_request) Successful in 24m28s
Details
ebd69089c5
programmerjake added 3 commits 2026-06-18 03:34:19 +00:00
tests/units_formal: test more instructions
All checks were successful
/ test (pull_request) Successful in 20m39s
Details
af87d52bf7
programmerjake force-pushed decode-and-test-harness from af87d52bf7 to ad9ec46aca 2026-06-18 07:16:17 +00:00 Compare
programmerjake added 1 commit 2026-06-19 02:21:19 +00:00
tests/units_formal: split up tests in hopes of making them run faster
All checks were successful
/ test (pull_request) Successful in 23m24s
Details
b6bbc97990
programmerjake added 1 commit 2026-06-19 03:27:42 +00:00
tests/units_formal: implement tests for rest of AddSub[I] instructions
All checks were successful
/ test (pull_request) Successful in 29m20s
Details
/ test (push) Successful in 30m13s
Details
fb0b07fbb2
programmerjake changed title from WIP: add cpu::test::decode_and_run_single_insn and some formal tests of running PowerISA instructions to add cpu::test::decode_and_run_single_insn and some formal tests of running PowerISA instructions 2026-06-19 03:45:10 +00:00
programmerjake scheduled this pull request to auto merge when all checks succeed 2026-06-19 03:49:01 +00:00
programmerjake merged commit fb0b07fbb2 into master 2026-06-19 03:57:09 +00:00
programmerjake deleted branch decode-and-test-harness 2026-06-19 03:57:12 +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
1 participant
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/cpu#15
No description provided.
Delete branch "programmerjake/cpu:decode-and-test-harness"

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?