From: Jacob Lifshay Date: Fri, 2 Sep 2022 06:06:56 +0000 (-0700) Subject: rename proof_decoder*.py -> test_decoder*.py so it gets run by pytest X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e046240f50d54cc997cf57bb28ae163cb9776d9;p=openpower-isa.git rename proof_decoder*.py -> test_decoder*.py so it gets run by pytest --- diff --git a/src/openpower/decoder/formal/proof_decoder.py b/src/openpower/decoder/formal/proof_decoder.py deleted file mode 100644 index ae53efb5..00000000 --- a/src/openpower/decoder/formal/proof_decoder.py +++ /dev/null @@ -1,128 +0,0 @@ -from nmigen import Module, Signal, Elaboratable, Cat -from nmigen.asserts import Assert, AnyConst, Assume -from nmutil.formaltest import FHDLTestCase - -from openpower.decoder.power_decoder import create_pdecode, PowerOp -from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel, - OutSel, RC, Form, Function, - LdstLen, CryIn, - MicrOp, get_csv) -from openpower.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 deleted file mode 100644 index 87f6919b..00000000 --- a/src/openpower/decoder/formal/proof_decoder2.py +++ /dev/null @@ -1,216 +0,0 @@ -from nmigen import Module, Signal, Elaboratable, Cat, Repl -from nmigen.asserts import Assert, AnyConst -from nmutil.formaltest import FHDLTestCase - -from openpower.decoder.power_decoder import create_pdecode, PowerOp -from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel, - OutSel, RC, Form, - MicrOp, SPRfull as SPR) -from openpower.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.Case(In2Sel.CONST_XBI): - comb += Assert(pdecode2.e.imm_data.data == dec.FormXB.XBI) - 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() diff --git a/src/openpower/decoder/formal/test_decoder.py b/src/openpower/decoder/formal/test_decoder.py new file mode 100644 index 00000000..ae53efb5 --- /dev/null +++ b/src/openpower/decoder/formal/test_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 openpower.decoder.power_decoder import create_pdecode, PowerOp +from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel, + OutSel, RC, Form, Function, + LdstLen, CryIn, + MicrOp, get_csv) +from openpower.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/test_decoder2.py b/src/openpower/decoder/formal/test_decoder2.py new file mode 100644 index 00000000..87f6919b --- /dev/null +++ b/src/openpower/decoder/formal/test_decoder2.py @@ -0,0 +1,216 @@ +from nmigen import Module, Signal, Elaboratable, Cat, Repl +from nmigen.asserts import Assert, AnyConst +from nmutil.formaltest import FHDLTestCase + +from openpower.decoder.power_decoder import create_pdecode, PowerOp +from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel, + OutSel, RC, Form, + MicrOp, SPRfull as SPR) +from openpower.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.Case(In2Sel.CONST_XBI): + comb += Assert(pdecode2.e.imm_data.data == dec.FormXB.XBI) + 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()