[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 #24 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
https://libre-soc.org/openpower/isatables/fields.text

hi samuel, trap proof progressing well. comments:

         with m.If(field(op.insn, 20, 26) == 1):

please don't do this.  use the fields/forms.  without the fields/forms it is
impossible to read the proof and crossreference it to the spec.

the only locations where this practice is still used is where microwatt code
has not yet had the field/form identified.

now to retun back to the field/form, you will find this extremely difficult
because the raw bits *contain no information*.

this difficulty is precisely why the decision to use fields/forms was made.

in addition some fields are not contiguous, they are spread across *multiple
bits* in a non-obvious order.

the last thing we need is "manual construction" duplicating exactly what
DecodeFields *already does*.

if this is of concern then we should have a proof of *DecofeFields*.

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