src/openpower/decoder/formal/test_decoder.py

   1 from nmigen import Module, Signal, Elaboratable, Cat
   2 from nmigen.asserts import Assert, AnyConst, Assume
   3 from nmutil.formaltest import FHDLTestCase
   4
   5 from openpower.decoder.power_decoder import create_pdecode, PowerOp
   6 from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
   7                                            OutSel, RCOE, Form, Function,
   8                                            LdstLen, CryIn,
   9                                            MicrOp, get_csv)
  10 from openpower.decoder.power_decoder2 import (PowerDecode2,
  11                                               Decode2ToExecute1Type)
  12 import unittest
  13 import pdb
  14
  15
  16 class Driver(Elaboratable):
  17     def __init__(self):
  18         self.instruction = Signal(32, reset_less=True)
  19         self.m = None
  20         self.comb = None
  21
  22     def elaborate(self, platform):
  23         self.m = Module()
  24         self.comb = self.m.d.comb
  25         self.instruction = Signal(32)
  26
  27         self.comb += self.instruction.eq(AnyConst(32))
  28
  29         pdecode = create_pdecode()
  30
  31         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  32         dec1 = pdecode2.dec
  33         self.comb += pdecode2.dec.bigendian.eq(1)  # TODO: bigendian=0
  34         self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
  35
  36         # ignore special decoding of nop
  37         self.comb += Assume(self.instruction != 0x60000000)
  38
  39         #self.assert_dec1_decode(dec1, dec1.dec)
  40
  41         self.assert_form(dec1, pdecode2)
  42         return self.m
  43
  44     def assert_dec1_decode(self, dec1, decoders):
  45         if not isinstance(decoders, list):
  46             decoders = [decoders]
  47         for d in decoders:
  48             print(d.pattern)
  49             opcode_switch = Signal(d.bitsel[1] - d.bitsel[0])
  50             self.comb += opcode_switch.eq(
  51                 self.instruction[d.bitsel[0]:d.bitsel[1]])
  52             with self.m.Switch(opcode_switch):
  53                 self.handle_subdecoders(dec1, d)
  54                 for row in d.opcodes:
  55                     opcode = row['opcode']
  56                     if d.opint and '-' not in opcode:
  57                         opcode = int(opcode, 0)
  58                     if not row['unit']:
  59                         continue
  60                     with self.m.Case(opcode):
  61                         self.comb += self.assert_dec1_signals(dec1, row)
  62                 with self.m.Default():
  63                     self.comb += Assert(dec.op.internal_op ==
  64                                         MicrOp.OP_ILLEGAL)
  65
  66     def handle_subdecoders(self, dec1, decoders):
  67         for dec in decoders.subdecoders:
  68             if isinstance(dec, list):
  69                 pattern = dec[0].pattern
  70             else:
  71                 pattern = dec.pattern
  72             with self.m.Case(pattern):
  73                 self.assert_dec1_decode(dec1, dec)
  74
  75     def assert_dec1_signals(self, dec, row):
  76         op = dec.op
  77         return [Assert(op.function_unit == Function[row['unit']]),
  78                 Assert(op.internal_op == MicrOp[row['internal op']]),
  79                 Assert(op.in1_sel == In1Sel[row['in1']]),
  80                 Assert(op.in2_sel == In2Sel[row['in2']]),
  81                 Assert(op.in3_sel == In3Sel[row['in3']]),
  82                 Assert(op.out_sel == OutSel[row['out']]),
  83                 Assert(op.ldst_len == LdstLen[row['ldst len']]),
  84                 Assert(op.rc_sel == RCOE[row['rc']]),
  85                 Assert(op.cry_in == CryIn[row['cry in']]),
  86                 Assert(op.form == Form[row['form']]),
  87                 ]
  88
  89     # This is to assert that the decoder conforms to the table listed
  90     # in PowerISA public spec v3.0B, Section 1.6, page 12
  91     def assert_form(self, dec, dec2):
  92         with self.m.Switch(dec.op.form):
  93             with self.m.Case(Form.A):
  94                 self.comb += Assert(dec.op.in1_sel.matches(
  95                     In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
  96                 self.comb += Assert(dec.op.in2_sel.matches(
  97                     In2Sel.RB, In2Sel.NONE))
  98                 self.comb += Assert(dec.op.in3_sel.matches(
  99                     In3Sel.RS, In3Sel.NONE))
 100                 self.comb += Assert(dec.op.out_sel.matches(
 101                     OutSel.NONE, OutSel.RT))
 102                 # The table has fields for XO and Rc, what do they match to?
 103             with self.m.Case(Form.B):
 104                 pass
 105             with self.m.Case(Form.D):
 106                 self.comb += Assert(dec.op.in1_sel.matches(
 107                     In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
 108                 self.comb += Assert(dec.op.in2_sel.matches(
 109                     In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
 110                     In2Sel.CONST_SI_HI))
 111                 self.comb += Assert(dec.op.out_sel.matches(
 112                     OutSel.NONE, OutSel.RT, OutSel.RA, OutSel.SPR,
 113                     OutSel.RT_OR_ZERO, OutSel.FRT, OutSel.FRS))
 114             with self.m.Case(Form.I):
 115                 self.comb += Assert(dec.op.in2_sel.matches(
 116                     In2Sel.CONST_LI))
 117
 118     def instr_bits(self, start, end=None):
 119         if not end:
 120             end = start
 121         return self.instruction[::-1][start:end+1]
 122
 123
 124 class DecoderTestCase(FHDLTestCase):
 125     @unittest.expectedFailure  # FIXME: proof failed:
 126     # needs to have all the enum entries added, TODO there
 127     # has to be an automated way to do that
 128     # self.comb += Assert(dec.op.in2_sel.matches(
 129     #    In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
 130     #    In2Sel.CONST_SI_HI))
 131     def test_decoder(self):
 132         module = Driver()
 133         self.assertFormal(module, mode="bmc", depth=4)
 134
 135
 136 if __name__ == '__main__':
 137     unittest.main()