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

Author	SHA1	Message	Date
Jacob Lifshay	fb0b07fbb2	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	2026-06-18 20:09:55 -07:00
Jacob Lifshay	b6bbc97990	tests/units_formal: split up tests in hopes of making them run faster All checks were successful / test (pull_request) Successful in 23m24s Details	2026-06-18 19:20:15 -07:00
Jacob Lifshay	ad9ec46aca	tests/units_formal: test more instructions All checks were successful / test (pull_request) Successful in 56m57s Details	2026-06-18 00:15:58 -07:00
Jacob Lifshay	d38bc786a7	unit::alu_branch::add_sub: bug fix: actually add in carry_in	2026-06-17 20:32:30 -07:00
Jacob Lifshay	6ee0d4265c	switch to using fayalite version of checked_vcd_output instead of cpu::util	2026-06-17 18:22:33 -07:00
Jacob Lifshay	ebd69089c5	tests/units_formal: prove more addition instructions -- [p]addi and add[c][o][.] All checks were successful / test (pull_request) Successful in 24m28s Details	2026-06-16 21:10:54 -07:00
Jacob Lifshay	51d71c56f6	update fayalite to speed up big formal proofs All checks were successful / test (pull_request) Successful in 10m58s Details	2026-06-14 19:26:23 -07:00
Jacob Lifshay	999860b507	update generated vcd All checks were successful / test (pull_request) Successful in 22m39s Details	2026-06-14 01:46:50 -07:00
Jacob Lifshay	9d9a755d99	update fayalite to get cmp_eq optimizations	2026-06-14 01:46:10 -07:00
Jacob Lifshay	ef30d325d5	formal proof works! also add test_power_isa_add_sim Some checks failed / test (pull_request) Failing after 22m21s Details	2026-06-05 19:46:24 -07:00
Jacob Lifshay	1bc59716c5	tests/units_formal::test_power_isa_add_formal: formal proof actually starts, though it fails BMC	2026-06-05 01:11:27 -07:00
Jacob Lifshay	70bd4ae851	update fayalite	2026-06-05 01:11:27 -07:00
Jacob Lifshay	f5d8486d81	decoder/simple_power_isa: fix wires being used outside of the if they're declared in, also add TraceAsString	2026-06-02 00:50:17 -07:00
Jacob Lifshay	93e948115d	added test::decode_and_run_single_insn and tests/units_formal, the new test takes a long time to run so idk if it works Some checks failed / test (pull_request) Failing after 3m0s Details	2026-06-01 01:02:57 -07:00
Jacob Lifshay	29622be160	ExecuteToUnitInterface: add guarantee that if `unit_outputs_ready` is false, then `enqueue.data` is HdlNone	2026-05-31 20:30:59 -07:00
Jacob Lifshay	7fc205e583	ArrayVec::map: actually connect to all output elements	2026-05-29 01:31:29 -07:00
Jacob Lifshay	9cecc6aaa0	rename_execute_retire::MOpInstance: use FETCH_BLOCK_ID_WIDTH	2026-05-29 01:30:42 -07:00