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 Assert, 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         # expected result
  35         expected = Signal(8)
  36         # transaction count for each port
  37         write_cnt = Signal(4)
  38         read_cnt = Signal(4)
  39         # keep data and valid stable, until accepted
  40         with m.If(Past(dut.p.valid_i) & ~Past(dut.p.ready_o)):
  41             comb += [
  42                 Assume(Stable(dut.op.sdir)),
  43                 Assume(Stable(dut.p.data_i.data)),
  44                 Assume(Stable(dut.p.data_i.shift)),
  45                 Assume(Stable(dut.p.valid_i)),
  46             ]
  47         # force reading the output in a reasonable time,
  48         # necessary to pass induction
  49         with m.If(Past(dut.n.valid_o) & ~Past(dut.n.ready_i)):
  50             comb += Assume(dut.n.ready_i)
  51         # capture transferred input data
  52         with m.If(dut.p.ready_o & dut.p.valid_i):
  53             sync += [
  54                 data_i.eq(dut.p.data_i.data),
  55                 shift_i.eq(dut.p.data_i.shift),
  56                 op_sdir.eq(dut.op.sdir),
  57                 # increment write counter
  58                 write_cnt.eq(write_cnt + 1),
  59             ]
  60             # calculate the expected result
  61             dut_data_i = dut.p.data_i.data
  62             dut_shift_i = dut.p.data_i.shift[:4]
  63             dut_sdir = dut.op.sdir
  64             with m.If(dut_sdir):
  65                 sync += expected.eq(dut_data_i >> dut_shift_i)
  66             with m.Else():
  67                 sync += expected.eq(dut_data_i << dut_shift_i)
  68         # Check for dropped inputs, by ensuring that there are no more than
  69         # one work item ever in flight at any given time.
  70         # Whenever the unit is busy (not ready) the read and write counters
  71         # will differ by exactly one unit.
  72         m.d.comb += Assert((read_cnt + ~dut.p.ready_o) & 0xF == write_cnt)
  73         # check coverage as output data is accepted
  74         with m.If(dut.n.ready_i & dut.n.valid_o):
  75             # increment read counter
  76             sync += read_cnt.eq(read_cnt + 1)
  77             # check result
  78             comb += Assert(dut.n.data_o.data == expected)
  79             # cover zero data, with zero and non-zero shift
  80             # (any direction)
  81             with m.If(data_i == 0):
  82                 with m.If(shift_i == 0):
  83                     sync += cov[0].eq(1)
  84                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  85                     sync += cov[1].eq(1)
  86             # cover non-zero data, with zero and non-zero shift
  87             # (both directions)
  88             with m.If(data_i != 0):
  89                 with m.If(shift_i == 0):
  90                     sync += cov[2].eq(1)
  91                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  92                     with m.If(op_sdir):
  93                         sync += cov[3].eq(1)
  94                     with m.Else():
  95                         sync += cov[4].eq(1)
  96                 # cover big shift
  97                 with m.If(shift_i[3] != 0):
  98                     sync += cov[5].eq(1)
  99             # cover non-zero shift giving non-zero result
 100             with m.If(data_i.any() & shift_i.any() & dut.n.data_o.data.any()):
 101                 sync += cov[6].eq(1)
 102             # dummy condition, to avoid optimizing-out the counters
 103             with m.If((write_cnt != 0) | (read_cnt != 0)):
 104                 sync += cov[7].eq(1)
 105         # check that each condition above occurred at least once
 106         comb += Cover(cov.all())
 107         return m
 108
 109
 110 class ALUFSMTestCase(FHDLTestCase):
 111     def test_formal(self):
 112         traces = [
 113             'clk',
 114             'p_data_i[7:0]', 'p_shift_i[7:0]', 'op__sdir',
 115             'p_valid_i', 'p_ready_o',
 116             'n_data_o[7:0]',
 117             'n_valid_o', 'n_ready_i',
 118             ('formal', {'module': 'top'}, [
 119                 'write_cnt[3:0]', 'read_cnt[3:0]', 'cov[7:0]'
 120             ])
 121         ]
 122         write_gtkw(
 123             'test_formal_cover_alu_fsm.gtkw',
 124             os.path.dirname(__file__) +
 125             '/proof_alu_fsm_formal/engine_0/trace0.vcd',
 126             traces,
 127             module='top.dut',
 128             zoom=-6.3
 129         )
 130         write_gtkw(
 131             'test_formal_bmc_alu_fsm.gtkw',
 132             os.path.dirname(__file__) +
 133             '/proof_alu_fsm_formal/engine_0/trace.vcd',
 134             traces,
 135             module='top.dut',
 136             zoom=-6.3
 137         )
 138         write_gtkw(
 139             'test_formal_induct_alu_fsm.gtkw',
 140             os.path.dirname(__file__) +
 141             '/proof_alu_fsm_formal/engine_0/trace_induct.vcd',
 142             traces,
 143             module='top.dut',
 144             zoom=-6.3
 145         )
 146         module = Driver()
 147         self.assertFormal(module, mode="prove", depth=18)
 148         self.assertFormal(module, mode="cover", depth=32)
 149
 150     @staticmethod
 151     def test_rtlil():
 152         dut = Driver()
 153         vl = rtlil.convert(dut, ports=[])
 154         with open("alu_fsm.il", "w") as f:
 155             f.write(vl)
 156
 157
 158 if __name__ == '__main__':
 159     unittest.main()