[Libre-soc-bugs] [Bug 419] MUL pipeline formal proof needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=419

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.