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         pass
  15     def elaborate(self, platform):
  16         m = Module()
  17         comb = m.d.comb
  18         instruction = Signal(32)
  19
  20         comb += instruction.eq(AnyConst(32))
  21
  22         pdecode = create_pdecode()
  23
  24         m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  25         comb += pdecode2.dec.opcode_in.eq(instruction)
  26
  27         self.test_in1(m, pdecode2, pdecode)
  28
  29         return m
  30
  31     def test_in1(self, m, pdecode2, pdecode):
  32         ra = pdecode.RA[0:-1]
  33         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  34             m.d.comb += Assert(pdecode2.e.read_reg1.data == ra)
  35             m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1)
  36         with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
  37             with m.If(ra == 0):
  38                 m.d.comb += Assert(pdecode2.e.read_reg1.ok == 0)
  39             with m.Else():
  40                 m.d.comb += Assert(pdecode2.e.read_reg1.data == ra)
  41                 m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1)
  42         op = pdecode.op.internal_op
  43         with m.If((op == InternalOp.OP_BC) |
  44                   (op == InternalOp.OP_BCREG)):
  45             with m.If(~pdecode.BO[2]):
  46                 m.d.comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
  47                 m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1)
  48         with m.If((op == InternalOp.OP_MFSPR) |
  49                   (op == InternalOp.OP_MTSPR)):
  50             m.d.comb += Assert(pdecode2.e.read_spr1.data == pdecode.SPR[0:-1])
  51             m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1)
  52
  53
  54 class Decoder2TestCase(FHDLTestCase):
  55     def test_decoder2(self):
  56         module = Driver()
  57         self.assertFormal(module, mode="bmc", depth=4)
  58
  59 if __name__ == '__main__':
  60     unittest.main()