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                                      InternalOp, SPR)
   8 from soc.decoder.power_decoder2 import (PowerDecode2,
   9                                         Decode2ToExecute1Type)
  10 import unittest
  11
  12 class Driver(Elaboratable):
  13     def __init__(self):
  14         self.m = None
  15         self.comb = None
  16
  17     def elaborate(self, platform):
  18         self.m = Module()
  19         self.comb = self.m.d.comb
  20         instruction = Signal(32)
  21
  22         self.comb += instruction.eq(AnyConst(32))
  23
  24         pdecode = create_pdecode()
  25
  26         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  27         self.comb += pdecode2.dec.opcode_in.eq(instruction)
  28
  29         self.test_in1(pdecode2, pdecode)
  30         self.test_in2()
  31         self.test_in3()
  32
  33         return self.m
  34
  35     def test_in1(self, pdecode2, pdecode):
  36         m = self.m
  37         comb = self.comb
  38         ra = pdecode.RA[0:-1]
  39         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  40             comb += Assert(pdecode2.e.read_reg1.data == ra)
  41             comb += Assert(pdecode2.e.read_reg1.ok == 1)
  42         with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
  43             with m.If(ra == 0):
  44                 comb += Assert(pdecode2.e.read_reg1.ok == 0)
  45             with m.Else():
  46                 comb += Assert(pdecode2.e.read_reg1.data == ra)
  47                 comb += Assert(pdecode2.e.read_reg1.ok == 1)
  48                 op = pdecode.op.internal_op
  49         with m.If((op == InternalOp.OP_BC) |
  50                   (op == InternalOp.OP_BCREG)):
  51             with m.If(~pdecode.BO[2]):
  52                 comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
  53                 comb += Assert(pdecode2.e.read_spr1.ok == 1)
  54         with m.If((op == InternalOp.OP_MFSPR) |
  55                   (op == InternalOp.OP_MTSPR)):
  56             comb += Assert(pdecode2.e.read_spr1.data ==
  57                            pdecode.SPR[0:-1])
  58             comb += Assert(pdecode2.e.read_spr1.ok == 1)
  59
  60     def test_in2(self):
  61         m = self.m
  62         comb = self.comb
  63         pdecode2 = m.submodules.pdecode2
  64         dec = pdecode2.dec
  65         with m.If(dec.op.in2_sel == In2Sel.RB):
  66             comb += Assert(pdecode2.e.read_reg2.ok == 1)
  67             comb += Assert(pdecode2.e.read_reg2.data ==
  68                            dec.RB[0:-1])
  69         with m.Elif(dec.op.in2_sel == In2Sel.NONE):
  70             comb += Assert(pdecode2.e.imm_data.ok == 0)
  71             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  72         with m.Elif(dec.op.in2_sel == In2Sel.SPR):
  73             comb += Assert(pdecode2.e.imm_data.ok == 0)
  74             comb += Assert(pdecode2.e.read_reg2.ok == 0)
  75             comb += Assert(pdecode2.e.read_spr2.ok == 1)
  76             with m.If(dec.FormXL.XO[9]):
  77                 comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR)
  78             with m.Else():
  79                 comb += Assert(pdecode2.e.read_spr2.data == SPR.LR)
  80         with m.Else():
  81             comb += Assert(pdecode2.e.imm_data.ok == 1)
  82             with m.Switch(dec.op.in2_sel):
  83                 with m.Case(In2Sel.CONST_UI):
  84                     comb += Assert(pdecode2.e.imm_data.data == dec.UI[0:-1])
  85                 with m.Case(In2Sel.CONST_SI):
  86                     comb += Assert(pdecode2.e.imm_data.data == dec.SI[0:-1])
  87                 with m.Case(In2Sel.CONST_UI_HI):
  88                     comb += Assert(pdecode2.e.imm_data.data ==
  89                                    (dec.UI[0:-1] << 4))
  90                 with m.Case(In2Sel.CONST_SI_HI):
  91                     comb += Assert(pdecode2.e.imm_data.data ==
  92                                    (dec.SI[0:-1] << 4))
  93                 with m.Case(In2Sel.CONST_LI):
  94                     comb += Assert(pdecode2.e.imm_data.data ==
  95                                    (dec.LI[0:-1] << 2))
  96                 with m.Case(In2Sel.CONST_BD):
  97                     comb += Assert(pdecode2.e.imm_data.data ==
  98                                    (dec.BD[0:-1] << 2))
  99                 with m.Case(In2Sel.CONST_DS):
 100                     comb += Assert(pdecode2.e.imm_data.data ==
 101                                    (dec.DS[0:-1] << 2))
 102                 with m.Case(In2Sel.CONST_M1):
 103                     comb += Assert(pdecode2.e.imm_data.data == ~0)
 104                 with m.Case(In2Sel.CONST_SH):
 105                     comb += Assert(pdecode2.e.imm_data.data == dec.sh[0:-1])
 106                 with m.Case(In2Sel.CONST_SH32):
 107                     comb += Assert(pdecode2.e.imm_data.data == dec.SH32[0:-1])
 108                 with m.Default():
 109                     comb += Assert(0)
 110
 111     def test_in3(self):
 112         m = self.m
 113         comb = self.comb
 114         pdecode2 = m.submodules.pdecode2
 115         with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS):
 116             comb += Assert(pdecode2.e.read_reg3.ok == 1)
 117             comb += Assert(pdecode2.e.read_reg3.data ==
 118                            pdecode2.dec.RS[0:-1])
 119
 120
 121 class Decoder2TestCase(FHDLTestCase):
 122     def test_decoder2(self):
 123         module = Driver()
 124         self.assertFormal(module, mode="bmc", depth=4)
 125
 126 if __name__ == '__main__':
 127     unittest.main()