src/soc/decoder/formal/proof_decoder2.py

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