Bug 211

Summary:	formal proof of PowerDecoder stage2 needed
Product:	Libre-SOC's first SoC	Reporter:	Luke Kenneth Casson Leighton <lkcl>
Component:	Formal Verification	Assignee:	Luke Kenneth Casson Leighton <lkcl>
Status:	CONFIRMED ---
Severity:	enhancement	CC:	libre-soc-bugs, mtnolan2640, programmerjake
Priority:	---
Version:	unspecified
Hardware:	PC
OS:	Linux
See Also:	http://bugs.libre-riscv.org/show_bug.cgi?id=212 https://bugs.libre-soc.org/show_bug.cgi?id=577
NLnet milestone:	---	total budget (EUR) for completion of task and all subtasks:	0
budget (EUR) for this task, excluding subtasks' budget:	0	parent task for budget allocation:
child tasks for budget allocation:		The table of payments (in EUR) for this task; TOML format:
Bug Depends on:
Bug Blocks:	158, 186, 195, 198

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

Comment 5 Luke Kenneth Casson Leighton 2022-08-26 14:28:41 BST

checking against gas isn't a formal proof,
taking this off milestone but not closing