src/soc/decoder/formal/proof_decoder.py

   1 from nmigen import Module, Signal, Elaboratable, Cat
   2 from nmigen.asserts import Assert, AnyConst, Assume
   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, Form, Function,
   8                                      LdstLen, CryIn,
   9                                      InternalOp, SPR, get_csv)
  10 from soc.decoder.power_decoder2 import (PowerDecode2,
  11                                         Decode2ToExecute1Type)
  12 import unittest
  13 import pdb
  14
  15 class Driver(Elaboratable):
  16     def __init__(self):
  17         self.instruction = Signal(32, reset_less=True)
  18         self.m = None
  19         self.comb = None
  20
  21     def elaborate(self, platform):
  22         self.m = Module()
  23         self.comb = self.m.d.comb
  24         self.instruction = Signal(32)
  25
  26         self.comb += self.instruction.eq(AnyConst(32))
  27
  28         pdecode = create_pdecode()
  29
  30         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
  31         dec1 = pdecode2.dec
  32         self.comb += pdecode2.dec.opcode_in.eq(self.instruction)
  33
  34         # ignore special decoding of nop
  35         self.comb += Assume(self.instruction != 0x60000000)
  36
  37         #self.assert_dec1_decode(dec1, dec1.dec)
  38
  39         self.assert_form(dec1, pdecode2)
  40         return self.m
  41
  42     def assert_dec1_decode(self, dec1, decoders):
  43         if not isinstance(decoders, list):
  44             decoders = [decoders]
  45         for d in decoders:
  46             print(d.pattern)
  47             opcode_switch = Signal(d.bitsel[1] - d.bitsel[0])
  48             self.comb += opcode_switch.eq(
  49                 self.instruction[d.bitsel[0]:d.bitsel[1]])
  50             with self.m.Switch(opcode_switch):
  51                 self.handle_subdecoders(dec1, d)
  52                 for row in d.opcodes:
  53                     opcode = row['opcode']
  54                     if d.opint and '-' not in opcode:
  55                         opcode = int(opcode, 0)
  56                     if not row['unit']:
  57                         continue
  58                     with self.m.Case(opcode):
  59                         self.comb += self.assert_dec1_signals(dec1, row)
  60
  61     def handle_subdecoders(self, dec1, decoders):
  62         for dec in decoders.subdecoders:
  63             if isinstance(dec, list):
  64                 pattern = dec[0].pattern
  65             else:
  66                 pattern = dec.pattern
  67             with self.m.Case(pattern):
  68                 self.assert_dec1_decode(dec1, dec)
  69
  70     def assert_dec1_signals(self, dec, row):
  71         op = dec.op
  72         return [Assert(op.function_unit == Function[row['unit']]),
  73                 Assert(op.internal_op == InternalOp[row['internal op']]),
  74                 Assert(op.in1_sel == In1Sel[row['in1']]),
  75                 Assert(op.in2_sel == In2Sel[row['in2']]),
  76                 Assert(op.in3_sel == In3Sel[row['in3']]),
  77                 Assert(op.out_sel == OutSel[row['out']]),
  78                 Assert(op.ldst_len == LdstLen[row['ldst len']]),
  79                 Assert(op.rc_sel == RC[row['rc']]),
  80                 Assert(op.cry_in == CryIn[row['cry in']]),
  81                 Assert(op.form == Form[row['form']]),
  82                 ]
  83
  84     def assert_form(self, dec, dec2):
  85         with self.m.Switch(dec.op.form):
  86             with self.m.Case(Form.A):
  87                 self.comb += Assert(dec2.e.write_reg.data ==
  88                                     self.instr_bits(6, 10))
  89                 self.comb += Assert(dec2.e.read_reg1.data ==
  90                                     self.instr_bits(11, 15))
  91                 self.comb += Assert(dec2.e.read_reg2.data ==
  92                                     self.instr_bits(16, 20))
  93                 # The table has fields for XO and Rc, but idk what they correspond to
  94             with self.m.Case(Form.B):
  95                 pass
  96             with self.m.Case(Form.D):
  97                 self.comb += Assert(dec.op.in1_sel.matches(
  98                     In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
  99                 self.comb += Assert(dec.op.in2_sel.matches(
 100                     In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
 101                     In2Sel.CONST_SI_HI))
 102                 self.comb += Assert(dec.op.out_sel.matches(
 103                     OutSel.NONE, OutSel.RT, OutSel.RA))
 104
 105
 106
 107
 108     def instr_bits(self, start, end=None):
 109         if not end:
 110             end = start
 111         return self.instruction[::-1][start:end+1]
 112
 113 class DecoderTestCase(FHDLTestCase):
 114     def test_decoder(self):
 115         module = Driver()
 116         self.assertFormal(module, mode="bmc", depth=4)
 117
 118 if __name__ == '__main__':
 119     unittest.main()