src/soc/decoder/formal/proof_decoder2.py

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