[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 #17 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #15)
> OK, new commit pushed; I reworked the SC properties and implemented the RFID
> properties following the documented pseudocode.  Looks like bits 29-31 of
> MSR is not set right when executing RFID.  Is this another bug?

let's check.

  87                 with m.If((field(dut.i.msr, 29, 31) != 0b010) |
  88                           (field(dut.i.msr, 29, 31) != 0b000)):
  89                     comb += Assert(field(msr_o.data, 29, 31) ==
field(srr1_i, 29, 31))

first, is an "Else" is missing there?


let's grab the pseudocode

if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
    MSR[29:31] <- SRR1[29:31]

ah! the 2nd comparison, line 88, should be dut.i.srr1 != 0b000

you have dut.i.msr != 0b000

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