src/soc/experiment/formal/proof_alu_fsm.py

   1 import unittest
   2 import os
   3
   4 from nmigen import Elaboratable, Signal, Module
   5 from nmigen.asserts import Assume, Cover, Past, Stable
   6 from nmigen.cli import rtlil
   7
   8 from nmutil.formaltest import FHDLTestCase
   9 from nmutil.gtkw import write_gtkw
  10
  11 from soc.experiment.alu_fsm import Shifter
  12
  13
  14 # This defines a module to drive the device under test and assert
  15 # properties about its outputs
  16 class Driver(Elaboratable):
  17     def __init__(self):
  18         # inputs and outputs
  19         pass
  20
  21     @staticmethod
  22     def elaborate(_):
  23         m = Module()
  24         comb = m.d.comb
  25         sync = m.d.sync
  26
  27         m.submodules.dut = dut = Shifter(8)
  28         # Coverage condition (one bit for each coverage case)
  29         cov = Signal(8)
  30         # input data to the shifter
  31         data_i = Signal(8)
  32         shift_i = Signal(8)
  33         op_sdir = Signal()
  34         # transaction count for each port
  35         write_cnt = Signal(4)
  36         read_cnt = Signal(4)
  37         # keep data and valid stable, until accepted
  38         with m.If(Past(dut.p.valid_i) & ~Past(dut.p.ready_o)):
  39             comb += [
  40                 Assume(Stable(dut.op.sdir)),
  41                 Assume(Stable(dut.p.data_i.data)),
  42                 Assume(Stable(dut.p.data_i.shift)),
  43                 Assume(Stable(dut.p.valid_i)),
  44             ]
  45         # capture transferred input data
  46         with m.If(dut.p.ready_o & dut.p.valid_i):
  47             sync += [
  48                 data_i.eq(dut.p.data_i.data),
  49                 shift_i.eq(dut.p.data_i.shift),
  50                 op_sdir.eq(dut.op.sdir),
  51                 # increment write counter
  52                 write_cnt.eq(write_cnt + 1),
  53             ]
  54         # check coverage as output data is accepted
  55         with m.If(dut.n.ready_i & dut.n.valid_o):
  56             # increment read counter
  57             sync += read_cnt.eq(read_cnt + 1)
  58             # cover zero data, with zero and non-zero shift
  59             # (any direction)
  60             with m.If(data_i == 0):
  61                 with m.If(shift_i == 0):
  62                     sync += cov[0].eq(1)
  63                 with m.If(shift_i[0:2].any() & ~shift_i[3]):
  64                     sync += cov[1].eq(1)
  65             # cover non-zero data, with zero and non-zero shift
  66             # (both directions)
  67             with m.If(data_i != 0):
  68                 with m.If(shift_i == 0):
  69                     sync += cov[2].eq(1)
  70                 with m.If(shift_i[0:2].any() & ~shift_i[3]):
  71                     with m.If(op_sdir):
  72                         sync += cov[3].eq(1)
  73                     with m.Else():
  74                         sync += cov[4].eq(1)
  75                 # cover big shift
  76                 with m.If(shift_i[3] != 0):
  77                     sync += cov[5].eq(1)
  78             # cover non-zero shift giving non-zero result
  79             with m.If(data_i.any() & shift_i.any() & dut.n.data_o.data.any()):
  80                 sync += cov[6].eq(1)
  81             # dummy condition, to avoid optimizing-out the counters
  82             with m.If((write_cnt != 0) | (read_cnt != 0)):
  83                 sync += cov[7].eq(1)
  84         # check that each condition above occurred at least once
  85         comb += Cover(cov.all())
  86         return m
  87
  88
  89 class ALUFSMTestCase(FHDLTestCase):
  90     def test_formal(self):
  91         traces = [
  92             'clk',
  93             'p_data_i[7:0]', 'p_shift_i[7:0]', 'op__sdir',
  94             'p_valid_i', 'p_ready_o',
  95             'n_data_o[7:0]',
  96             'n_valid_o', 'n_ready_i',
  97             ('formal', {'module': 'top'}, [
  98                 'write_cnt[3:0]', 'read_cnt[3:0]', 'cov[7:0]'
  99             ])
 100         ]
 101         write_gtkw(
 102             'test_formal_alu_fsm.gtkw',
 103             os.path.dirname(__file__) +
 104             '/proof_alu_fsm_formal/engine_0/trace0.vcd',
 105             traces,
 106             module='top.dut',
 107             zoom=-6.3
 108         )
 109         module = Driver()
 110         self.assertFormal(module, mode="cover", depth=32)
 111
 112     @staticmethod
 113     def test_rtlil():
 114         dut = Driver()
 115         vl = rtlil.convert(dut, ports=[])
 116         with open("alu_fsm.il", "w") as f:
 117             f.write(vl)
 118
 119
 120 if __name__ == '__main__':
 121     unittest.main()