[Libre-soc-bugs] [Bug 421] TRAP pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #3)
>     comb += msr_o.data[MSR.ME].eq((msr_i[MSR.HV] & srr1_i[MSR.HV]) |
>                                   (~msr_i[MSR.HV] & srr1_i[MSR.HV]))
> 
> 
> Per DeMorgan's Theorems, isn't this statement the same as:
> 
>     comb += msr_o.data[MSR.ME].eq(srr1_i[MSR.HV])
> 
> ?

that's a bug, yay!  spec - in the pseudo-code - is this:

    MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
    MSR[3] <- (MSR[3] & SRR1[3])

but the words say this:

    If MSR3=1 then bits 3 and 51 of SRR1 are placed into
    the corresponding bits of the MSR.

do those look consistent to you? (nobody has really properly
reviewed the pseudocode in the spec so inconsistencies are
expected)

i've updated main_stage.py to use an if statement rather
than the & / | masking for bits 51 and 3.

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