From 1891c1bf2b224648c7aa094c17452565d90bf9fd Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 23 Apr 2021 13:30:46 +0100 Subject: [PATCH] add decoder proofs --- src/openpower/decoder/formal/__init__.py | 0 src/openpower/decoder/formal/proof_decoder.py | 128 +++++++++++ .../decoder/formal/proof_decoder2.py | 211 ++++++++++++++++++ 3 files changed, 339 insertions(+) create mode 100644 src/openpower/decoder/formal/__init__.py create mode 100644 src/openpower/decoder/formal/proof_decoder.py create mode 100644 src/openpower/decoder/formal/proof_decoder2.py diff --git a/src/openpower/decoder/formal/__init__.py b/src/openpower/decoder/formal/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/src/openpower/decoder/formal/proof_decoder.py b/src/openpower/decoder/formal/proof_decoder.py new file mode 100644 index 00000000..5abd9182 --- /dev/null +++ b/src/openpower/decoder/formal/proof_decoder.py @@ -0,0 +1,128 @@ +from nmigen import Module, Signal, Elaboratable, Cat +from nmigen.asserts import Assert, AnyConst, Assume +from nmutil.formaltest import FHDLTestCase + +from soc.decoder.power_decoder import create_pdecode, PowerOp +from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel, + OutSel, RC, Form, Function, + LdstLen, CryIn, + MicrOp, SPR, get_csv) +from soc.decoder.power_decoder2 import (PowerDecode2, + Decode2ToExecute1Type) +import unittest +import pdb + +class Driver(Elaboratable): + def __init__(self): + self.instruction = Signal(32, reset_less=True) + self.m = None + self.comb = None + + def elaborate(self, platform): + self.m = Module() + self.comb = self.m.d.comb + self.instruction = Signal(32) + + self.comb += self.instruction.eq(AnyConst(32)) + + pdecode = create_pdecode() + + self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode) + dec1 = pdecode2.dec + self.comb += pdecode2.dec.bigendian.eq(1) # TODO: bigendian=0 + self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction) + + # ignore special decoding of nop + self.comb += Assume(self.instruction != 0x60000000) + + #self.assert_dec1_decode(dec1, dec1.dec) + + self.assert_form(dec1, pdecode2) + return self.m + + def assert_dec1_decode(self, dec1, decoders): + if not isinstance(decoders, list): + decoders = [decoders] + for d in decoders: + print(d.pattern) + opcode_switch = Signal(d.bitsel[1] - d.bitsel[0]) + self.comb += opcode_switch.eq( + self.instruction[d.bitsel[0]:d.bitsel[1]]) + with self.m.Switch(opcode_switch): + self.handle_subdecoders(dec1, d) + for row in d.opcodes: + opcode = row['opcode'] + if d.opint and '-' not in opcode: + opcode = int(opcode, 0) + if not row['unit']: + continue + with self.m.Case(opcode): + self.comb += self.assert_dec1_signals(dec1, row) + with self.m.Default(): + self.comb += Assert(dec.op.internal_op == + MicrOp.OP_ILLEGAL) + + + def handle_subdecoders(self, dec1, decoders): + for dec in decoders.subdecoders: + if isinstance(dec, list): + pattern = dec[0].pattern + else: + pattern = dec.pattern + with self.m.Case(pattern): + self.assert_dec1_decode(dec1, dec) + + def assert_dec1_signals(self, dec, row): + op = dec.op + return [Assert(op.function_unit == Function[row['unit']]), + Assert(op.internal_op == MicrOp[row['internal op']]), + Assert(op.in1_sel == In1Sel[row['in1']]), + Assert(op.in2_sel == In2Sel[row['in2']]), + Assert(op.in3_sel == In3Sel[row['in3']]), + Assert(op.out_sel == OutSel[row['out']]), + Assert(op.ldst_len == LdstLen[row['ldst len']]), + Assert(op.rc_sel == RC[row['rc']]), + Assert(op.cry_in == CryIn[row['cry in']]), + Assert(op.form == Form[row['form']]), + ] + + # This is to assert that the decoder conforms to the table listed + # in PowerISA public spec v3.0B, Section 1.6, page 12 + def assert_form(self, dec, dec2): + with self.m.Switch(dec.op.form): + with self.m.Case(Form.A): + self.comb += Assert(dec.op.in1_sel.matches( + In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO)) + self.comb += Assert(dec.op.in2_sel.matches( + In2Sel.RB, In2Sel.NONE)) + self.comb += Assert(dec.op.in3_sel.matches( + In3Sel.RS, In3Sel.NONE)) + self.comb += Assert(dec.op.out_sel.matches( + OutSel.NONE, OutSel.RT)) + # The table has fields for XO and Rc, but idk what they correspond to + with self.m.Case(Form.B): + pass + with self.m.Case(Form.D): + self.comb += Assert(dec.op.in1_sel.matches( + In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO)) + self.comb += Assert(dec.op.in2_sel.matches( + In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI, + In2Sel.CONST_SI_HI)) + self.comb += Assert(dec.op.out_sel.matches( + OutSel.NONE, OutSel.RT, OutSel.RA)) + with self.m.Case(Form.I): + self.comb += Assert(dec.op.in2_sel.matches( + In2Sel.CONST_LI)) + + def instr_bits(self, start, end=None): + if not end: + end = start + return self.instruction[::-1][start:end+1] + +class DecoderTestCase(FHDLTestCase): + def test_decoder(self): + module = Driver() + self.assertFormal(module, mode="bmc", depth=4) + +if __name__ == '__main__': + unittest.main() diff --git a/src/openpower/decoder/formal/proof_decoder2.py b/src/openpower/decoder/formal/proof_decoder2.py new file mode 100644 index 00000000..b7ac61f7 --- /dev/null +++ b/src/openpower/decoder/formal/proof_decoder2.py @@ -0,0 +1,211 @@ +from nmigen import Module, Signal, Elaboratable, Cat, Repl +from nmigen.asserts import Assert, AnyConst +from nmutil.formaltest import FHDLTestCase + +from soc.decoder.power_decoder import create_pdecode, PowerOp +from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel, + OutSel, RC, Form, + MicrOp, SPR) +from soc.decoder.power_decoder2 import (PowerDecode2, + Decode2ToExecute1Type) +import unittest + +class Driver(Elaboratable): + def __init__(self): + self.m = None + self.comb = None + self.instruction = None + + def elaborate(self, platform): + self.m = Module() + self.comb = self.m.d.comb + self.instruction = Signal(32) + + self.comb += self.instruction.eq(AnyConst(32)) + + pdecode = create_pdecode() + + self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode) + self.comb += pdecode2.dec.bigendian.eq(1) # XXX TODO: bigendian=0 + self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction) + + self.test_in1(pdecode2, pdecode) + self.test_in2() + self.test_in2_fields() + self.test_in3() + self.test_out() + self.test_rc() + self.test_single_bits() + + return self.m + + def test_in1(self, pdecode2, pdecode): + m = self.m + comb = self.comb + ra = self.instr_bits(11, 15) + with m.If(pdecode.op.in1_sel == In1Sel.RA): + comb += Assert(pdecode2.e.read_reg1.data == ra) + comb += Assert(pdecode2.e.read_reg1.ok == 1) + with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO): + with m.If(ra == 0): + comb += Assert(pdecode2.e.read_reg1.ok == 0) + with m.Else(): + comb += Assert(pdecode2.e.read_reg1.data == ra) + comb += Assert(pdecode2.e.read_reg1.ok == 1) + op = pdecode.op.internal_op + with m.If((op == MicrOp.OP_BC) | + (op == MicrOp.OP_BCREG)): + with m.If(~self.instr_bits(8)): + comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR) + comb += Assert(pdecode2.e.read_spr1.ok == 1) + with m.If((op == MicrOp.OP_MFSPR) | + (op == MicrOp.OP_MTSPR)): + comb += Assert(pdecode2.e.read_spr1.data == self.instr_bits(11, 20)) + comb += Assert(pdecode2.e.read_spr1.ok == 1) + + def test_in2(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + dec = pdecode2.dec + with m.If(dec.op.in2_sel == In2Sel.RB): + comb += Assert(pdecode2.e.read_reg2.ok == 1) + comb += Assert(pdecode2.e.read_reg2.data == dec.RB) + with m.Elif(dec.op.in2_sel == In2Sel.NONE): + comb += Assert(pdecode2.e.imm_data.ok == 0) + comb += Assert(pdecode2.e.read_reg2.ok == 0) + with m.Elif(dec.op.in2_sel == In2Sel.SPR): + comb += Assert(pdecode2.e.imm_data.ok == 0) + comb += Assert(pdecode2.e.read_reg2.ok == 0) + comb += Assert(pdecode2.e.read_spr2.ok == 1) + with m.If(dec.fields.FormXL.XO[9]): + comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR) + with m.Else(): + comb += Assert(pdecode2.e.read_spr2.data == SPR.LR) + with m.Else(): + comb += Assert(pdecode2.e.imm_data.ok == 1) + with m.Switch(dec.op.in2_sel): + with m.Case(In2Sel.CONST_UI): + comb += Assert(pdecode2.e.imm_data.data == dec.UI) + with m.Case(In2Sel.CONST_SI): + comb += Assert(pdecode2.e.imm_data.data == + self.exts(dec.SI, 16, 64)) + with m.Case(In2Sel.CONST_UI_HI): + comb += Assert(pdecode2.e.imm_data.data == (dec.UI << 16)) + with m.Case(In2Sel.CONST_SI_HI): + comb += Assert(pdecode2.e.imm_data.data == + self.exts(dec.SI << 16, 32, 64)) + with m.Case(In2Sel.CONST_LI): + comb += Assert(pdecode2.e.imm_data.data == (dec.LI << 2)) + with m.Case(In2Sel.CONST_BD): + comb += Assert(pdecode2.e.imm_data.data == (dec.BD << 2)) + with m.Case(In2Sel.CONST_DS): + comb += Assert(pdecode2.e.imm_data.data == (dec.DS << 2)) + with m.Case(In2Sel.CONST_M1): + comb += Assert(pdecode2.e.imm_data.data == ~0) + with m.Case(In2Sel.CONST_SH): + comb += Assert(pdecode2.e.imm_data.data == dec.sh) + with m.Case(In2Sel.CONST_SH32): + comb += Assert(pdecode2.e.imm_data.data == dec.SH32) + with m.Default(): + comb += Assert(0) + + def exts(self, exts_data, width, fullwidth): + exts_data = exts_data[0:width] + topbit = exts_data[-1] + signbits = Repl(topbit, fullwidth-width) + return Cat(exts_data, signbits) + + def test_in2_fields(self): + m = self.m + comb = self.comb + dec = m.submodules.pdecode2.dec + + comb += Assert(dec.RB == self.instr_bits(16, 20)) + comb += Assert(dec.UI == self.instr_bits(16, 31)) + comb += Assert(dec.SI == self.instr_bits(16, 31)) + comb += Assert(dec.LI == self.instr_bits(6, 29)) + comb += Assert(dec.BD == self.instr_bits(16, 29)) + comb += Assert(dec.DS == self.instr_bits(16, 29)) + comb += Assert(dec.sh == Cat(self.instr_bits(16, 20), + self.instr_bits(30))) + comb += Assert(dec.SH32 == self.instr_bits(16, 20)) + + def test_in3(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS): + comb += Assert(pdecode2.e.read_reg3.ok == 1) + comb += Assert(pdecode2.e.read_reg3.data == self.instr_bits(6,10)) + + def test_out(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + sel = pdecode2.dec.op.out_sel + dec = pdecode2.dec + with m.If(sel == OutSel.SPR): + comb += Assert(pdecode2.e.write_spr.ok == 1) + comb += Assert(pdecode2.e.write_reg.ok == 0) + with m.Elif(sel == OutSel.NONE): + comb += Assert(pdecode2.e.write_spr.ok == 0) + comb += Assert(pdecode2.e.write_reg.ok == 0) + with m.Else(): + comb += Assert(pdecode2.e.write_spr.ok == 0) + comb += Assert(pdecode2.e.write_reg.ok == 1) + data = pdecode2.e.write_reg.data + with m.If(sel == OutSel.RT): + comb += Assert(data == self.instr_bits(6, 10)) + with m.If(sel == OutSel.RA): + comb += Assert(data == self.instr_bits(11, 15)) + + def test_rc(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + sel = pdecode2.dec.op.rc_sel + dec = pdecode2.dec + comb += Assert(pdecode2.e.rc.ok == 1) + with m.If(sel == RC.NONE): + comb += Assert(pdecode2.e.rc.data == 0) + with m.If(sel == RC.ONE): + comb += Assert(pdecode2.e.rc.data == 1) + with m.If(sel == RC.RC): + comb += Assert(pdecode2.e.rc.data == dec.Rc) + comb += Assert(pdecode2.e.oe.ok == 1) + comb += Assert(pdecode2.e.oe.data == dec.OE) + + def test_single_bits(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + dec = pdecode2.dec + e = pdecode2.e + comb += Assert(e.invert_in == dec.op.inv_a) + comb += Assert(e.invert_out == dec.op.inv_out) + comb += Assert(e.input_carry == dec.op.cry_in) + comb += Assert(e.output_carry == dec.op.cry_out) + comb += Assert(e.is_32bit == dec.op.is_32b) + comb += Assert(e.is_signed == dec.op.sgn) + with m.If(dec.op.lk): + comb += Assert(e.lk == self.instr_bits(31)) + comb += Assert(e.byte_reverse == dec.op.br) + comb += Assert(e.sign_extend == dec.op.sgn_ext) + comb += Assert(e.update == dec.op.upd) + comb += Assert(e.input_cr == dec.op.cr_in) + comb += Assert(e.output_cr == dec.op.cr_out) + + def instr_bits(self, start, end=None): + if not end: + end = start + return self.instruction[::-1][start:end+1][::-1] + + +class Decoder2TestCase(FHDLTestCase): + def test_decoder2(self): + module = Driver() + self.assertFormal(module, mode="bmc", depth=4) + +if __name__ == '__main__': + unittest.main() -- 2.30.2