src/openpower/decoder/formal/proof_decoder2.py

   1 from nmigen import Module, Signal, Elaboratable, Cat, Repl
   2 from nmigen.asserts import Assert, AnyConst
   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, RC, Form,
   8                                            MicrOp, SPRfull as SPR)
   9 from openpower.decoder.power_decoder2 import (PowerDecode2,
  10                                               Decode2ToExecute1Type)
  11 import unittest
  12
  13
  14 class Driver(Elaboratable):
  15     def __init__(self):
  16         self.m = None
  17         self.comb = None
  18         self.instruction = None
  19
  20     def elaborate(self, platform):
  21         self.m = Module()
  22         self.comb = self.m.d.comb
  23         self.instruction = Signal(32)
  24
  25         self.comb += self.instruction.eq(AnyConst(32))
  26
  27         pdecode = create_pdecode()
  28
  29         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  30         self.comb += pdecode2.dec.bigendian.eq(1)  # XXX TODO: bigendian=0
  31         self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
  32
  33         self.test_in1(pdecode2, pdecode)
  34         self.test_in2()
  35         self.test_in2_fields()
  36         self.test_in3()
  37         self.test_out()
  38         self.test_rc()
  39         self.test_single_bits()
  40
  41         return self.m
  42
  43     def test_in1(self, pdecode2, pdecode):
  44         m = self.m
  45         comb = self.comb
  46         ra = self.instr_bits(11, 15)
  47         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  48             comb += Assert(pdecode2.e.read_reg1.data == ra)
  49             comb += Assert(pdecode2.e.read_reg1.ok == 1)
  50         with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
  51             with m.If(ra == 0):
  52                 comb += Assert(pdecode2.e.read_reg1.ok == 0)
  53             with m.Else():
  54                 comb += Assert(pdecode2.e.read_reg1.data == ra)
  55                 comb += Assert(pdecode2.e.read_reg1.ok == 1)
  56                 op = pdecode.op.internal_op
  57         with m.If((op == MicrOp.OP_BC) |
  58                   (op == MicrOp.OP_BCREG)):
  59             with m.If(~self.instr_bits(8)):
  60                 comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
  61                 comb += Assert(pdecode2.e.read_spr1.ok == 1)
  62         with m.If((op == MicrOp.OP_MFSPR) |
  63                   (op == MicrOp.OP_MTSPR)):
  64             comb += Assert(pdecode2.e.read_spr1.data ==
  65                            self.instr_bits(11, 20))
  66             comb += Assert(pdecode2.e.read_spr1.ok == 1)
  67
  68     def test_in2(self):
  69         m = self.m
  70         comb = self.comb
  71         pdecode2 = m.submodules.pdecode2
  72         dec = pdecode2.dec
  73         with m.If(dec.op.in2_sel == In2Sel.RB):
  74             comb += Assert(pdecode2.e.read_reg2.ok == 1)
  75             comb += Assert(pdecode2.e.read_reg2.data == dec.RB)
  76         with m.Elif(dec.op.in2_sel == In2Sel.NONE):
  77             comb += Assert(pdecode2.e.imm_data.ok == 0)
  78             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  79         with m.Elif(dec.op.in2_sel == In2Sel.SPR):
  80             comb += Assert(pdecode2.e.imm_data.ok == 0)
  81             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  82             comb += Assert(pdecode2.e.read_spr2.ok == 1)
  83             with m.If(dec.fields.FormXL.XO[9]):
  84                 comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR)
  85             with m.Else():
  86                 comb += Assert(pdecode2.e.read_spr2.data == SPR.LR)
  87         with m.Else():
  88             comb += Assert(pdecode2.e.imm_data.ok == 1)
  89             with m.Switch(dec.op.in2_sel):
  90                 with m.Case(In2Sel.CONST_UI):
  91                     comb += Assert(pdecode2.e.imm_data.data == dec.UI)
  92                 with m.Case(In2Sel.CONST_SI):
  93                     comb += Assert(pdecode2.e.imm_data.data ==
  94                                    self.exts(dec.SI, 16, 64))
  95                 with m.Case(In2Sel.CONST_UI_HI):
  96                     comb += Assert(pdecode2.e.imm_data.data == (dec.UI << 16))
  97                 with m.Case(In2Sel.CONST_SI_HI):
  98                     comb += Assert(pdecode2.e.imm_data.data ==
  99                                    self.exts(dec.SI << 16, 32, 64))
 100                 with m.Case(In2Sel.CONST_LI):
 101                     comb += Assert(pdecode2.e.imm_data.data == (dec.LI << 2))
 102                 with m.Case(In2Sel.CONST_BD):
 103                     comb += Assert(pdecode2.e.imm_data.data == (dec.BD << 2))
 104                 with m.Case(In2Sel.CONST_DS):
 105                     comb += Assert(pdecode2.e.imm_data.data == (dec.DS << 2))
 106                 with m.Case(In2Sel.CONST_M1):
 107                     comb += Assert(pdecode2.e.imm_data.data == ~0)
 108                 with m.Case(In2Sel.CONST_SH):
 109                     comb += Assert(pdecode2.e.imm_data.data == dec.sh)
 110                 with m.Case(In2Sel.CONST_SH32):
 111                     comb += Assert(pdecode2.e.imm_data.data == dec.SH32)
 112                 with m.Case(In2Sel.CONST_XBI):
 113                     comb += Assert(pdecode2.e.imm_data.data == dec.FormXB.XBI)
 114                 with m.Default():
 115                     comb += Assert(0)
 116
 117     def exts(self, exts_data, width, fullwidth):
 118         exts_data = exts_data[0:width]
 119         topbit = exts_data[-1]
 120         signbits = Repl(topbit, fullwidth-width)
 121         return Cat(exts_data, signbits)
 122
 123     def test_in2_fields(self):
 124         m = self.m
 125         comb = self.comb
 126         dec = m.submodules.pdecode2.dec
 127
 128         comb += Assert(dec.RB == self.instr_bits(16, 20))
 129         comb += Assert(dec.UI == self.instr_bits(16, 31))
 130         comb += Assert(dec.SI == self.instr_bits(16, 31))
 131         comb += Assert(dec.LI == self.instr_bits(6, 29))
 132         comb += Assert(dec.BD == self.instr_bits(16, 29))
 133         comb += Assert(dec.DS == self.instr_bits(16, 29))
 134         comb += Assert(dec.sh == Cat(self.instr_bits(16, 20),
 135                                      self.instr_bits(30)))
 136         comb += Assert(dec.SH32 == self.instr_bits(16, 20))
 137
 138     def test_in3(self):
 139         m = self.m
 140         comb = self.comb
 141         pdecode2 = m.submodules.pdecode2
 142         with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS):
 143             comb += Assert(pdecode2.e.read_reg3.ok == 1)
 144             comb += Assert(pdecode2.e.read_reg3.data == self.instr_bits(6, 10))
 145
 146     def test_out(self):
 147         m = self.m
 148         comb = self.comb
 149         pdecode2 = m.submodules.pdecode2
 150         sel = pdecode2.dec.op.out_sel
 151         dec = pdecode2.dec
 152         with m.If(sel == OutSel.SPR):
 153             comb += Assert(pdecode2.e.write_spr.ok == 1)
 154             comb += Assert(pdecode2.e.write_reg.ok == 0)
 155         with m.Elif(sel == OutSel.NONE):
 156             comb += Assert(pdecode2.e.write_spr.ok == 0)
 157             comb += Assert(pdecode2.e.write_reg.ok == 0)
 158         with m.Else():
 159             comb += Assert(pdecode2.e.write_spr.ok == 0)
 160             comb += Assert(pdecode2.e.write_reg.ok == 1)
 161             data = pdecode2.e.write_reg.data
 162             with m.If(sel == OutSel.RT):
 163                 comb += Assert(data == self.instr_bits(6, 10))
 164             with m.If(sel == OutSel.RA):
 165                 comb += Assert(data == self.instr_bits(11, 15))
 166
 167     def test_rc(self):
 168         m = self.m
 169         comb = self.comb
 170         pdecode2 = m.submodules.pdecode2
 171         sel = pdecode2.dec.op.rc_sel
 172         dec = pdecode2.dec
 173         comb += Assert(pdecode2.e.rc.ok == 1)
 174         with m.If(sel == RC.NONE):
 175             comb += Assert(pdecode2.e.rc.data == 0)
 176         with m.If(sel == RC.ONE):
 177             comb += Assert(pdecode2.e.rc.data == 1)
 178         with m.If(sel == RC.RC):
 179             comb += Assert(pdecode2.e.rc.data == dec.Rc)
 180             comb += Assert(pdecode2.e.oe.ok == 1)
 181             comb += Assert(pdecode2.e.oe.data == dec.OE)
 182
 183     def test_single_bits(self):
 184         m = self.m
 185         comb = self.comb
 186         pdecode2 = m.submodules.pdecode2
 187         dec = pdecode2.dec
 188         e = pdecode2.e
 189         comb += Assert(e.invert_in == dec.op.inv_a)
 190         comb += Assert(e.invert_out == dec.op.inv_out)
 191         comb += Assert(e.input_carry == dec.op.cry_in)
 192         comb += Assert(e.output_carry == dec.op.cry_out)
 193         comb += Assert(e.is_32bit == dec.op.is_32b)
 194         comb += Assert(e.is_signed == dec.op.sgn)
 195         with m.If(dec.op.lk):
 196             comb += Assert(e.lk == self.instr_bits(31))
 197         comb += Assert(e.byte_reverse == dec.op.br)
 198         comb += Assert(e.sign_extend == dec.op.sgn_ext)
 199         comb += Assert(e.update == dec.op.upd)
 200         comb += Assert(e.input_cr == dec.op.cr_in)
 201         comb += Assert(e.output_cr == dec.op.cr_out)
 202
 203     def instr_bits(self, start, end=None):
 204         if not end:
 205             end = start
 206         return self.instruction[::-1][start:end+1][::-1]
 207
 208
 209 class Decoder2TestCase(FHDLTestCase):
 210     def test_decoder2(self):
 211         module = Driver()
 212         self.assertFormal(module, mode="bmc", depth=4)
 213
 214
 215 if __name__ == '__main__':
 216     unittest.main()