Instructions: * gfbredpoly # sets reducing polynomial SPR `GFBREDPOLY` unless this is an immediate op, mtspr is completely sufficient. * gfbmul RT, RA, RB * gfbmadd RT, RA, RB, RC * gfbtmadd twin for fft * gfbinv rt, ra input 0 gives result 0 even though that is division by zero, that's what's needed for AES. Steps (edit as needed): * TODO: Instruction Encodings * TODO: MSR bit to be reserved to indicate Poly SPR in use (avoids need to save Poly SPR on contextswitch) * basic adaptable modules (probably in nmigen-gf) * DONE: module in nmigen-gf * DONE: gfbmul/gfbmadd * DONE: gfbinv * DONE: unit test * DONE: gfbmul/gfbmadd * DONE: gfbinv * DONE: formal * DONE: gfbmul/gfbmadd * DONE: gfbinv * TODO: add encoding of gfb* to SVP64Asm class (as a 32bit op) * TODO: add gfb* to TBD pipe(s) * TODO: fu unit tests * TODO: fu formal
I'll start working on this today. I'm guessing this may be the last thing I'll have time to do before the grant expires. My plan is to create the hdl in nmigen-gf.git for gfbmul/gfbmadd with formal tests, then work on gfbinv with formal tests, then if there's time, add all that as a new alu/pipeline to soc.git (no MSR bit for now as that's extra complexity). I'm guessing I will have run out of time by then.
actually, nevermind, all budget for bug #782 is already used.
there may be budget available in bug #772 (the top-level bug), icr if we asked NLnet to remove that budget
I implemented the nmigen-gf HDL for gfbmadd/gfbmul, and have unit tests for it. I also discovered bugs in gfbmadd/gfbmul's python reference code, where they accidentally attempt to truncate the clmul output, which I fixed and I made sure the unit tests were adjusted to catch that. I pushed to the bug_785_gfb_insns branch. All tests pass, except some the formal tests, which I cancelled since I didn't want to wait. I'll run a full test after posting this. https://git.libre-soc.org/?p=nmigen-gf.git;a=shortlog;h=fa3842779ffec3ebed85d9118ec56cffe17fe707 commit fa3842779ffec3ebed85d9118ec56cffe17fe707 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Wed May 15 01:03:12 2024 -0700 hdl/gfbmadd: GFBMAddFSMStage works! commit e80ef2e1770b2c81d3c5d8117100c38373de78f6 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Tue May 14 23:23:09 2024 -0700 hdl/gfbmadd.py: add FSM-based reference python code commit caaf4a5d66d519cd3bfe2eb42d65a94aed61a676 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Tue May 14 21:04:49 2024 -0700 add HDL implementation of decode_reducing_polynomial commit 306341e23427fed07f30e839cc19fe358dda93e2 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Tue May 14 23:32:00 2024 -0700 reference/test_cl_gfb_gfp.py: test reducing polynomial that is XLEN+1 bits commit 0df15ec21ff37b03483f9feb94c3c86a5e2c8b0a Author: Jacob Lifshay <programmerjake@gmail.com> Date: Tue May 14 23:21:16 2024 -0700 reference/gfbm[ul/add].py: fix truncation bugs commit a3ec5e652796ff472421cf1b85669a4cfc662fe5 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Tue May 14 23:24:31 2024 -0700 format code
(In reply to Jacob Lifshay from comment #3) > there may be budget available in bug #772 (the top-level bug), there isn't - i prioritised more important work, carryless mul, bug #784, we already got paid.
(In reply to Luke Kenneth Casson Leighton from comment #5) > (In reply to Jacob Lifshay from comment #3) > > there may be budget available in bug #772 (the top-level bug), > > there isn't - i prioritised more important work, carryless mul, bug #784, > we already got paid. yeah, but there's EUR 3000 left on bug #772 that's not assigned to any sub-bugs. Is that still available or did we ask NLnet to remove it?
(In reply to Jacob Lifshay from comment #6) > (In reply to Luke Kenneth Casson Leighton from comment #5) > > (In reply to Jacob Lifshay from comment #3) > > > there may be budget available in bug #772 (the top-level bug), > > > > there isn't - i prioritised more important work, carryless mul, bug #784, > > we already got paid. > > yeah, but there's EUR 3000 left on bug #772 that's not assigned to any > sub-bugs. Is that still available or did we ask NLnet to remove it? going off of the RFP submission page, the EUR 3000 is still available. only EUR 6000 of the EUR 9000 was assigned.
(In reply to Jacob Lifshay from comment #7) > going off of the RFP submission page, the EUR 3000 is still available. only > EUR 6000 of the EUR 9000 was assigned. https://libre-soc.org/task_db/report/ yes you're right, go for it. can i ask you the favour of allocating some for me? be much appreciated.
(In reply to Luke Kenneth Casson Leighton from comment #8) > yes you're right, go for it. can i ask you the favour of allocating > some for me? be much appreciated. I'll wait to see if Cesar wants to work on the GF(p) instructions, if not I'll just allocate all EUR 3000 to this bug. I got gfbinv working: https://git.libre-soc.org/?p=nmigen-gf.git;a=shortlog;h=c7732f5d2c0901cd4d5e30bcf83f56f7b07ea925 commit c7732f5d2c0901cd4d5e30bcf83f56f7b07ea925 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Wed May 15 23:21:04 2024 -0700 hdl/gfbinv: add gfbinv implementation, all tests pass! commit 1cf975b3772cc9e1dd357db6a039ba5ae77413c1 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Wed May 15 23:20:10 2024 -0700 hdl/gfbmadd: fix doc comment commit 1979fd94d6e3cab2e5682e7d34e1eaaec9079336 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Wed May 15 18:59:43 2024 -0700 skip extremely slow tests -- >2hr last I checked
I got the formal proof for gfbinv to work! https://git.libre-soc.org/?p=nmigen-gf.git;a=shortlog;h=35e5f677384814056e63e17e4c5005366017cebf commit 35e5f677384814056e63e17e4c5005366017cebf Author: Jacob Lifshay <programmerjake@gmail.com> Date: Fri May 17 01:16:04 2024 -0700 hdl/test/test_gfbinv: add formal proof for gfbinv commit a3c473b0521038e02f67a899fcaf1795ce3ff295 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Fri May 17 01:15:12 2024 -0700 test DecodeReducingPolynomial exhaustively for small XLEN commit 1b041671a37502608fe577110193398f18b7fee8 Author: Jacob Lifshay <programmerjake@gmail.com> Date: Fri May 17 01:10:57 2024 -0700 change decode_reducing_polynomial definition so it can encode x^XLEN + x + 1 also adds a test that all degree <= XLEN irreducible polynomials can be encoded commit 9d615801f85b1878bc46548bca1479c73438bf8c Author: Jacob Lifshay <programmerjake@gmail.com> Date: Fri May 17 01:09:11 2024 -0700 gf_reference/is_irreducible.py: move is_irreducible() to a separate file commit 68ba5fe8e3ec9f4bd322110e1fc0e4f75906c6df Author: Jacob Lifshay <programmerjake@gmail.com> Date: Thu May 16 22:02:45 2024 -0700 hdl/clmul: split clmuladd hdl out into separate function for ease of use in formal proofs
(In reply to Jacob Lifshay from comment #10) cool! mathematically that's quite a big deal > I got the formal proof for gfbinv to work!
gfbmul/gfbmadd's formal proof works too! Since Bob hasn't responded about when our deadline is, should we consider this done due to running out of time and submit the RFPs? https://git.libre-soc.org/?p=nmigen-gf.git;a=shortlog;h=bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb commit bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb Author: Jacob Lifshay <programmerjake@gmail.com> Date: Fri May 17 17:41:07 2024 -0700 hdl/test/test_gfbmadd: add formal proof of gfbmadd
(In reply to Jacob Lifshay from comment #12) > gfbmul/gfbmadd's formal proof works too! > > Since Bob hasn't responded about when our deadline is, should we consider > this done due to running out of time and submit the RFPs? ohh yes. will have to go at the higher-up bugreport otherwise it will need an update to the json file, and we don't have time. chasing the chain... this one: https://bugs.libre-soc.org/show_bug.cgi?id=772