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
  36         return self.m
  37
  38     def test_in1(self, pdecode2, pdecode):
  39         m = self.m
  40         comb = self.comb
  41         ra = pdecode.RA[0:-1]
  42         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  43             comb += Assert(pdecode2.e.read_reg1.data == ra)
  44             comb += Assert(pdecode2.e.read_reg1.ok == 1)
  45         with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
  46             with m.If(ra == 0):
  47                 comb += Assert(pdecode2.e.read_reg1.ok == 0)
  48             with m.Else():
  49                 comb += Assert(pdecode2.e.read_reg1.data == ra)
  50                 comb += Assert(pdecode2.e.read_reg1.ok == 1)
  51                 op = pdecode.op.internal_op
  52         with m.If((op == InternalOp.OP_BC) |
  53                   (op == InternalOp.OP_BCREG)):
  54             with m.If(~pdecode.BO[2]):
  55                 comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
  56                 comb += Assert(pdecode2.e.read_spr1.ok == 1)
  57         with m.If((op == InternalOp.OP_MFSPR) |
  58                   (op == InternalOp.OP_MTSPR)):
  59             comb += Assert(pdecode2.e.read_spr1.data ==
  60                            pdecode.SPR[0:-1])
  61             comb += Assert(pdecode2.e.read_spr1.ok == 1)
  62
  63     def test_in2(self):
  64         m = self.m
  65         comb = self.comb
  66         pdecode2 = m.submodules.pdecode2
  67         dec = pdecode2.dec
  68         with m.If(dec.op.in2_sel == In2Sel.RB):
  69             comb += Assert(pdecode2.e.read_reg2.ok == 1)
  70             comb += Assert(pdecode2.e.read_reg2.data ==
  71                            dec.RB[0:-1])
  72         with m.Elif(dec.op.in2_sel == In2Sel.NONE):
  73             comb += Assert(pdecode2.e.imm_data.ok == 0)
  74             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  75         with m.Elif(dec.op.in2_sel == In2Sel.SPR):
  76             comb += Assert(pdecode2.e.imm_data.ok == 0)
  77             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  78             comb += Assert(pdecode2.e.read_spr2.ok == 1)
  79             with m.If(dec.FormXL.XO[9]):
  80                 comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR)
  81             with m.Else():
  82                 comb += Assert(pdecode2.e.read_spr2.data == SPR.LR)
  83         with m.Else():
  84             comb += Assert(pdecode2.e.imm_data.ok == 1)
  85             with m.Switch(dec.op.in2_sel):
  86                 with m.Case(In2Sel.CONST_UI):
  87                     comb += Assert(pdecode2.e.imm_data.data == dec.UI[0:-1])
  88                 with m.Case(In2Sel.CONST_SI):
  89                     comb += Assert(pdecode2.e.imm_data.data == dec.SI[0:-1])
  90                 with m.Case(In2Sel.CONST_UI_HI):
  91                     comb += Assert(pdecode2.e.imm_data.data ==
  92                                    (dec.UI[0:-1] << 4))
  93                 with m.Case(In2Sel.CONST_SI_HI):
  94                     comb += Assert(pdecode2.e.imm_data.data ==
  95                                    (dec.SI[0:-1] << 4))
  96                 with m.Case(In2Sel.CONST_LI):
  97                     comb += Assert(pdecode2.e.imm_data.data ==
  98                                    (dec.LI[0:-1] << 2))
  99                 with m.Case(In2Sel.CONST_BD):
 100                     comb += Assert(pdecode2.e.imm_data.data ==
 101                                    (dec.BD[0:-1] << 2))
 102                 with m.Case(In2Sel.CONST_DS):
 103                     comb += Assert(pdecode2.e.imm_data.data ==
 104                                    (dec.DS[0:-1] << 2))
 105                 with m.Case(In2Sel.CONST_M1):
 106                     comb += Assert(pdecode2.e.imm_data.data == ~0)
 107                 with m.Case(In2Sel.CONST_SH):
 108                     comb += Assert(pdecode2.e.imm_data.data == dec.sh[0:-1])
 109                 with m.Case(In2Sel.CONST_SH32):
 110                     comb += Assert(pdecode2.e.imm_data.data == dec.SH32[0:-1])
 111                 with m.Default():
 112                     comb += Assert(0)
 113
 114     def test_in3(self):
 115         m = self.m
 116         comb = self.comb
 117         pdecode2 = m.submodules.pdecode2
 118         with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS):
 119             comb += Assert(pdecode2.e.read_reg3.ok == 1)
 120             comb += Assert(pdecode2.e.read_reg3.data ==
 121                            pdecode2.dec.RS[0:-1])
 122
 123     def test_out(self):
 124         m = self.m
 125         comb = self.comb
 126         pdecode2 = m.submodules.pdecode2
 127         sel = pdecode2.dec.op.out_sel
 128         dec = pdecode2.dec
 129         with m.If(sel == OutSel.SPR):
 130             comb += Assert(pdecode2.e.write_spr.ok == 1)
 131             comb += Assert(pdecode2.e.write_reg.ok == 0)
 132         with m.Elif(sel == OutSel.NONE):
 133             comb += Assert(pdecode2.e.write_spr.ok == 0)
 134             comb += Assert(pdecode2.e.write_reg.ok == 0)
 135         with m.Else():
 136             comb += Assert(pdecode2.e.write_spr.ok == 0)
 137             comb += Assert(pdecode2.e.write_reg.ok == 1)
 138             data = pdecode2.e.write_reg.data
 139             with m.If(sel == OutSel.RT):
 140                 comb += Assert(data == dec.RT[0:-1])
 141             with m.If(sel == OutSel.RA):
 142                 comb += Assert(data == dec.RA[0:-1])
 143
 144     def test_rc(self):
 145         m = self.m
 146         comb = self.comb
 147         pdecode2 = m.submodules.pdecode2
 148         sel = pdecode2.dec.op.rc_sel
 149         dec = pdecode2.dec
 150         comb += Assert(pdecode2.e.rc.ok == 1)
 151         with m.If(sel == RC.NONE):
 152             comb += Assert(pdecode2.e.rc.data == 0)
 153         with m.If(sel == RC.ONE):
 154             comb += Assert(pdecode2.e.rc.data == 1)
 155         with m.If(sel == RC.RC):
 156             comb += Assert(pdecode2.e.rc.data == dec.Rc[0:-1])
 157
 158
 159
 160 class Decoder2TestCase(FHDLTestCase):
 161     def test_decoder2(self):
 162         module = Driver()
 163         self.assertFormal(module, mode="bmc", depth=4)
 164
 165 if __name__ == '__main__':
 166     unittest.main()