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 from soc.decoder.power_decoder2 import (PowerDecode2,
   8                                         Decode2ToExecute1Type)
   9 import unittest
  10
  11 class Driver(Elaboratable):
  12     def __init__(self):
  13         pass
  14     def elaborate(self, platform):
  15         m = Module()
  16         comb = m.d.comb
  17         instruction = Signal(32)
  18
  19         comb += instruction.eq(AnyConst(32))
  20
  21         pdecode = create_pdecode()
  22
  23         m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  24         comb += pdecode2.dec.opcode_in.eq(instruction)
  25
  26         self.test_in1(m, pdecode2, pdecode)
  27
  28         return m
  29
  30     def test_in1(self, m, pdecode2, pdecode):
  31         with m.If(pdecode.op.in1_sel == In1Sel.RA):
  32             m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1)
  33
  34
  35 class Decoder2TestCase(FHDLTestCase):
  36     def test_decoder2(self):
  37         module = Driver()
  38         self.assertFormal(module, mode="bmc", depth=4)
  39
  40 if __name__ == '__main__':
  41     unittest.main()