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
  31         return self.m
  32
  33     def test_in1(self, pdecode2, pdecode):
  34         m = self.m
  35         comb = self.comb
  36         ra = pdecode.RA[0:-1]
  37         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  38             comb += Assert(pdecode2.e.read_reg1.data == ra)
  39             comb += Assert(pdecode2.e.read_reg1.ok == 1)
  40         with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
  41             with m.If(ra == 0):
  42                 comb += Assert(pdecode2.e.read_reg1.ok == 0)
  43             with m.Else():
  44                 comb += Assert(pdecode2.e.read_reg1.data == ra)
  45                 comb += Assert(pdecode2.e.read_reg1.ok == 1)
  46                 op = pdecode.op.internal_op
  47         with m.If((op == InternalOp.OP_BC) |
  48                   (op == InternalOp.OP_BCREG)):
  49             with m.If(~pdecode.BO[2]):
  50                 comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
  51                 comb += Assert(pdecode2.e.read_spr1.ok == 1)
  52         with m.If((op == InternalOp.OP_MFSPR) |
  53                   (op == InternalOp.OP_MTSPR)):
  54             comb += Assert(pdecode2.e.read_spr1.data ==
  55                            pdecode.SPR[0:-1])
  56             comb += Assert(pdecode2.e.read_spr1.ok == 1)
  57
  58 class Decoder2TestCase(FHDLTestCase):
  59     def test_decoder2(self):
  60         module = Driver()
  61         self.assertFormal(module, mode="bmc", depth=4)
  62
  63 if __name__ == '__main__':
  64     unittest.main()