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         # capture transferred input data
  48         with m.If(dut.p.ready_o & dut.p.valid_i):
  49             sync += [
  50                 data_i.eq(dut.p.data_i.data),
  51                 shift_i.eq(dut.p.data_i.shift),
  52                 op_sdir.eq(dut.op.sdir),
  53                 # increment write counter
  54                 write_cnt.eq(write_cnt + 1),
  55             ]
  56             # calculate the expected result
  57             dut_data_i = dut.p.data_i.data
  58             dut_shift_i = dut.p.data_i.shift[:4]
  59             dut_sdir = dut.op.sdir
  60             with m.If(dut_sdir):
  61                 sync += expected.eq(dut_data_i >> dut_shift_i)
  62             with m.Else():
  63                 sync += expected.eq(dut_data_i << dut_shift_i)
  64         # check coverage as output data is accepted
  65         with m.If(dut.n.ready_i & dut.n.valid_o):
  66             # increment read counter
  67             sync += read_cnt.eq(read_cnt + 1)
  68             # check result
  69             comb += Assert(dut.n.data_o.data == expected)
  70             # cover zero data, with zero and non-zero shift
  71             # (any direction)
  72             with m.If(data_i == 0):
  73                 with m.If(shift_i == 0):
  74                     sync += cov[0].eq(1)
  75                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  76                     sync += cov[1].eq(1)
  77             # cover non-zero data, with zero and non-zero shift
  78             # (both directions)
  79             with m.If(data_i != 0):
  80                 with m.If(shift_i == 0):
  81                     sync += cov[2].eq(1)
  82                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  83                     with m.If(op_sdir):
  84                         sync += cov[3].eq(1)
  85                     with m.Else():
  86                         sync += cov[4].eq(1)
  87                 # cover big shift
  88                 with m.If(shift_i[3] != 0):
  89                     sync += cov[5].eq(1)
  90             # cover non-zero shift giving non-zero result
  91             with m.If(data_i.any() & shift_i.any() & dut.n.data_o.data.any()):
  92                 sync += cov[6].eq(1)
  93             # dummy condition, to avoid optimizing-out the counters
  94             with m.If((write_cnt != 0) | (read_cnt != 0)):
  95                 sync += cov[7].eq(1)
  96         # check that each condition above occurred at least once
  97         comb += Cover(cov.all())
  98         return m
  99
 100
 101 class ALUFSMTestCase(FHDLTestCase):
 102     def test_formal(self):
 103         traces = [
 104             'clk',
 105             'p_data_i[7:0]', 'p_shift_i[7:0]', 'op__sdir',
 106             'p_valid_i', 'p_ready_o',
 107             'n_data_o[7:0]',
 108             'n_valid_o', 'n_ready_i',
 109             ('formal', {'module': 'top'}, [
 110                 'write_cnt[3:0]', 'read_cnt[3:0]', 'cov[7:0]'
 111             ])
 112         ]
 113         write_gtkw(
 114             'test_formal_cover_alu_fsm.gtkw',
 115             os.path.dirname(__file__) +
 116             '/proof_alu_fsm_formal/engine_0/trace0.vcd',
 117             traces,
 118             module='top.dut',
 119             zoom=-6.3
 120         )
 121         write_gtkw(
 122             'test_formal_bmc_alu_fsm.gtkw',
 123             os.path.dirname(__file__) +
 124             '/proof_alu_fsm_formal/engine_0/trace.vcd',
 125             traces,
 126             module='top.dut',
 127             zoom=-6.3
 128         )
 129         module = Driver()
 130         self.assertFormal(module, mode="bmc", depth=16)
 131         self.assertFormal(module, mode="cover", depth=32)
 132
 133     @staticmethod
 134     def test_rtlil():
 135         dut = Driver()
 136         vl = rtlil.convert(dut, ports=[])
 137         with open("alu_fsm.il", "w") as f:
 138             f.write(vl)
 139
 140
 141 if __name__ == '__main__':
 142     unittest.main()