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".
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.
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
One thing that would be useful is testing our decoder against a Power assembler/disassembler (gas, llvm-as, objdump, llvm-objdump)
(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
checking against gas isn't a formal proof, taking this off milestone but not closing