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