[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 #26 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #24)
> 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 return 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 *DecodeFields*.

or, i don't mind this - at all:

    sc_fields = decoder.fields.FormSC
    LEV = sc_fields.LEV[0:-1]
    comb += lev.eq(LEV)
    comb += Assert(op.insn[31-20:31-27] == lev) # check lev gets correct bits

followed by using *lev* in the ongoing assertions, likewise for TO.

that i like.

but referring directly to the bits themselves such that information and
clarity is completely lost, when people like myself have had huge difficulty
working with PowerISA bit-numbering?  mmm... no.

you can see even in the example above, i got it wrong, because i forgot
that the fields are in *PowerISA* order, which is, according to p4 section
1.3.2 Notation, in the ***REVERSE*** order from normal conventions.

bit 0 is the **MSB** in PowerISA notation.

the use of FieldSelectableInt (which is behind the Decoder Fields) takes
care of that automatically for us.

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