a MUL pipeline formal correctness proof is needed
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/pipeline.py;h=f5a0f069b94e314fcfe43a74486f9d29b763e3f0;hb=HEAD#l10 samuel try a copy of this, add the extra stage. i believe PipeModBase does the same thing as i described on the list (StageChain) which will have the advantahe you should be able to just drop it in place and use dut.i and dut.o
(In reply to Luke Kenneth Casson Leighton from comment #1) > samuel try a copy of this, add the extra stage. i believe PipeModBase does > the same thing as i described on the list (StageChain) which will have the > advantahe you should be able to just drop it in place and use dut.i and dut.o I spent some time trying to understand what you're suggesting here. I tried to just instantiate a MulBasePipe as the DUT, but I get 13 screensful of errors because it doesn't support the expected interface for .i and .o members. I don't understand how copying the code in that class would help though; can you clarify? Thanks.
(In reply to Samuel A. Falvo II from comment #2) > I don't understand how copying the code in that class would help though; can > you clarify? Thanks. apologies, we need to speed things up, a lot. i will explain why at an appropriate time. https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=d3deda12916c450f05f7d03610f0ef79c9cbdafb i have set up a triple chain using StageChain which you can see was being called from nmutil PipeModBase. i had to work out how to use it because the last time i called StageChain was 18 months ago. a dummy object is set up with a dut.i and dut.o so that the remaining cut/pasted code does not need significant mods. you can go ahead and use dut.i and dut.o as if there was a single combinatorial block between them, from a single module. stage 1 abs's its input stage 2 does the mul stage 3 works out which bits of result to use however with all 3 chained together you can ignore that entirely and implement the OP_MUL* microcode operations in any way you see fit that is preferably simple and clear. however please do not be surprised to find that symbiyosys MUL runs as slow as molasses flowing downhill in arctic winter. there is not a lot we can do about that.
(In reply to Luke Kenneth Casson Leighton from comment #3) > however please do not be surprised to find that symbiyosys MUL runs as slow > as molasses flowing downhill in arctic winter. there is not a lot we can do > about that. Wow, molasses can be scary: https://en.wikipedia.org/wiki/Great_Molasses_Flood
Can someone take a look at my latest commit? I don't know what I'm doing with this, apparently. Maybe I should look into other issues.
(In reply to Samuel A. Falvo II from comment #5) > Can someone take a look at my latest commit? I don't know what I'm doing > with this, apparently. neither do i! i did however veery patiently investigate until i noticed that OP_MUL_H32 is marked in the CSV file (major_31.csv) as being a 32-bit op only, checked in pre_stage.py (eq32(is_32bit, xxx, zzz)) and then realised, "argh, if we try to validate OP_MUL_H32 with is_32bit=False it's not going to produce valid data" so i added this: with m.Case(MicrOp.OP_MUL_H32): comb += Assume(rec.is_32bit) # OP_MUL_H32 is a 32-bit op and it's now "working". i say "working", i mean "running at 100% CPU for the past 10 minutes" > Maybe I should look into other issues. well, here's what i explained to Cole: the most important thing for this project is that people are doing *something*, and *communicating*. you can see how verbose things are on bugreports with Cole, and it took quite a lot of reinforcement that that is *okay*, because talking things things over in "English" is often far better. if you're running into issues, *please don't wait an entire week*! even half an hour is far too long - a week is over 300x that reasonable limit! [as long as it is on-topic] you cannot be too verbose in using the bugtracker to think things through. even if you type it and then find the answer yourself: hit send anyway because it contains a record of your thoughts, which is as useful for you (if they turn out later to be wrong) as it is for project archiving and audit purposes.
commit 2e117c06cb6b147e59e80fcba6d060695c62766e (HEAD -> master, origin/master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Wed Aug 19 07:24:58 2020 +0100 bit of a reorg of mul proof, tracking down missing Assume op.is_32bit == 0 for OP_MUL_H32 ok now we've worked out that OP_MUL_H32 is only suited to 32-bit, the next step is to do the signed multiply. this is the implementation from decode/helpers.py of a python-based signed multiply: # signed version of MUL def MULS(a, b): a_s = a.value & (1 << (a.bits-1)) != 0 b_s = b.value & (1 << (b.bits-1)) != 0 result = abs(a) * abs(b) print("MULS", result, a_s, b_s) if a_s == b_s: return result return -result because - again - OP_MUL_H32 *only* works on 32-bit numbers, we can do: a_s = a[31] b_s = b[31] rather than mungy-mess above (which copes with variable-size numbers)
(In reply to Luke Kenneth Casson Leighton from comment #6) > [as long as it is on-topic] you cannot be too verbose in using the bugtracker > to think things through. even if you type it and then find the answer > yourself: hit send anyway because it contains a record of your thoughts, > which is as useful for you (if they turn out later to be wrong) as it is for > project archiving and audit purposes. They're also useful so others can see the pitfalls you fell into for what they are and avoid them.
it occurs to me that perhaps the error encountered here is the same one as for shift proof.
I *think* I've completed this pipeline proof.
(In reply to Samuel A. Falvo II from comment #10) > I *think* I've completed this pipeline proof. excellent, looks reasonable: i threw some comments in, could you put some comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's doing? and why the abs values are used and why check on sign-comparison? also i believe you missed dut.o.o.ok, there are some other proofs that create a signal named "ok", set it to 1 at the top, then in the "default" of the switch set it to zero. works a treat. need to check xer_ov as well (different method, there) then i think we're good here?
(In reply to Luke Kenneth Casson Leighton from comment #11) > excellent, looks reasonable: i threw some comments in, could you put some > comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's > doing? and why the abs values are used and why check on sign-comparison? Done. > also i believe you missed dut.o.o.ok, there are some other proofs that > create a signal named "ok", set it to 1 at the top, then in the > "default" of the switch set it to zero. works a treat. Thanks for this; FOR NOW, I'd like to delay adding this until I fix the most recent breakage. I just committed my recent changes, which by all accounts should work. However, line 113 (asserting xer_ov_o == dut.i.ctx.xer_ov) consistently fails **as long as** I assign the convenience variable xer_ov_o = dut.o.xer_ov.data. If I replace xer_ov_o with the referent dut.o.xer_ov.data, it consistently works. I cannot explain this behavior. Why should this ever be the case? > need to check xer_ov as well (different method, there) Not sure what you mean here? Can you clarify?
(In reply to Samuel A. Falvo II from comment #12) > (In reply to Luke Kenneth Casson Leighton from comment #11) > > excellent, looks reasonable: i threw some comments in, could you put some > > comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's > > doing? and why the abs values are used and why check on sign-comparison? > > Done. > > > also i believe you missed dut.o.o.ok, there are some other proofs that > > create a signal named "ok", set it to 1 at the top, then in the > > "default" of the switch set it to zero. works a treat. > > Thanks for this; FOR NOW, I'd like to delay adding this until I fix the most > recent breakage. I just committed my recent changes, which by all accounts > should work. However, line 113 (asserting xer_ov_o == dut.i.ctx.xer_ov) > consistently fails **as long as** I assign the convenience variable xer_ov_o > = dut.o.xer_ov.data. If I replace xer_ov_o with the referent > dut.o.xer_ov.data, it consistently works. oink. > I cannot explain this behavior. Why should this ever be the case? no idea. sounds like a bug that needs raising (on nmigen). > > need to check xer_ov as well (different method, there) > > Not sure what you mean here? Can you clarify? xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually write the result. if they are not checked then there is the possibility that whilst data is produced it never actually hits the regfile. therefore Assert(dut.o.o.ok == something) and Assert(dut.o.xer_ov.ok == something) are needed.
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/post_stage.py;h=dbe560e96e61c5ffbd2897e8d8345529aa101bad;hb=HEAD#l42 but, first, these need fixing. * o.ok should never be set unconditionally. this says "results are being produced all the time" which is Bad. * xer_ov.ok should only be set if there is the possibility of an overflow: on MUL L64 will raise as a new bug
(In reply to Luke Kenneth Casson Leighton from comment #13) > oink. Fixed! > xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually > write the result. Right. That's what I thought, but wasn't 100% sure.
(In reply to Samuel A. Falvo II from comment #15) > (In reply to Luke Kenneth Casson Leighton from comment #13) > > oink. > > Fixed! > > > xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually > > write the result. > > Right. That's what I thought, but wasn't 100% sure. ok you implemented something slightly differently, checking the OE flag (this is output_stage.py's job, which is not part of the chain). we chained these together: pipe1 = MulMainStage1(pspec) pipe2 = MulMainStage2(pspec) pipe3 = MulMainStage3(pspec) where in fu/mul/pipeline.py you can see that OE checking is handled here: out = DivMulOutputStage(self.pspec) # do CR, XER and out-invert etc. so any Assertions involving OE would be erroneous. the xer_ov.ok flag (and o.ok flag) are quite simple, they just tell the Register Files, "results are available if you want them". there does exist a Formal Correctness Proof for OutputStage, it does need updating.
commit d8d6b488a97e638fdf497da3a2c1622937243a82 (HEAD -> master, origin/master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Sun Aug 30 11:00:37 2020 +0100 tidyup on mul proof
Thanks for cleaning up the code; it reads a lot better. I do have some questions though. (In reply to Luke Kenneth Casson Leighton from comment #16) > the xer_ov.ok flag (and o.ok flag) are quite simple, they just tell the > Register Files, "results are available if you want them". Can you help me understand why xer_ov.ok is reset only in the default case? As I understand the ISA specs, xer_ov.ok should only be set when OE=1. I feel like I'm missing something. > there does exist a Formal Correctness Proof for OutputStage, it does need > updating. I looked in the fu/mul hierarchy for this correctness proof, but did not find it. Are you perhaps referring to alu/formal/proof_output_stage.py ?
(In reply to Samuel A. Falvo II from comment #18) > Thanks for cleaning up the code; it reads a lot better. I do have some > questions though. > Can you help me understand why xer_ov.ok is reset only in the default case? > As I understand the ISA specs, xer_ov.ok should only be set when OE=1. I > feel like I'm missing something. OutputStage, which is *not included in the chain in this proof*, handles OE checking. check for yourself: https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/formal/proof_main_stage.py;h=0cf767f341668663a4f4c736af5aea5625c1c0d2;hb=HEAD#l88 is OutputStage in that chain? no it is not. therefore trying to Assert things that *are not part of the test* is simply never going to work, is it? > > there does exist a Formal Correctness Proof for OutputStage, it does need > > updating. > > I looked in the fu/mul hierarchy for this correctness proof, but did not > find it. yes. it's in the alu dir. > Are you perhaps referring to alu/formal/proof_output_stage.py ? yes. if we were to include OutputStage in the chain at line 88, then the contents of alu proof_output_stage.py would need to be duplicated in their entirety in mul proof, wouldn't they? which would be a waste of effort. therefore we don't do that.
(In reply to Luke Kenneth Casson Leighton from comment #19) > therefore trying to Assert things that *are not part of the test* is simply > never going to work, is it? I'm just going by what is in the instruction documentation. I think I see now, though; in OutputStage.py, there's a block of code which tests for the OE flag, and sets *its own* ov.ok output to 1 if set. It completely ignores any ov.ok signal from previous stages. Apologies if this all seems like I'm being daft; I'm just trying to get a grasp of the bigger picture.