Bug 211 - formal proof of PowerDecoder stage2 needed
Summary: formal proof of PowerDecoder stage2 needed
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 158 195 198 186
  Show dependency treegraph
 
Reported: 2020-03-09 12:30 GMT by Luke Kenneth Casson Leighton
Modified: 2020-12-02 14:52 GMT (History)
3 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 200
budget (EUR) for this task, excluding subtasks' budget: 200
parent task for budget allocation: 198
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-03-09 12:30:28 GMT
using the power_fields.py field decoder *in combination* with the
csv decoder, formally prove that the decoder generates correct bitfield
decoders for all fields for all opcodes, in power_decoder2.py.
also critical to ensure that anything not covered is correctly registered
as "illegal opcode".
Comment 1 Michael Nolan 2020-03-09 14:03:03 GMT
I'm somewhat hesitant to try and prove the stage-1 decoder, since the proof would essentially be making a duplicate of the decoder separately, and checking that the two are equivalent. I'm not entirely sure how useful that would be.

A formal proof for stage-2 on the other hand seems much more straightforward, and would be more useful.
Comment 2 Luke Kenneth Casson Leighton 2020-03-09 15:54:08 GMT
ok yes.

the decode_fields.py code has two tables that it reads: the FormX etc etc which extracts the formats, however the useful bit is the actual form (XFX etc).

i *manually* added those as an extra column to the CSV files.

therefore, where they match, we need to ensure that the decoded fields (register, immediate, SPR, OE, LK etc) are all correctly lined up.

later we will need to add FP fields and args, possibly extra entries to the CSV files to get at extra fields, have to see
Comment 3 Jacob Lifshay 2020-03-09 16:50:02 GMT
One thing that would be useful is testing our decoder against a Power assembler/disassembler (gas, llvm-as, objdump, llvm-objdump)
Comment 4 Luke Kenneth Casson Leighton 2020-03-09 19:35:10 GMT
(In reply to Jacob Lifshay from comment #3)
> One thing that would be useful is testing our decoder against a Power
> assembler/disassembler (gas, llvm-as, objdump, llvm-objdump)

ooo that's a neat idea. see #212