4 from nmigen
import Elaboratable
, Signal
, Module
5 from nmigen
.asserts
import Assert
, Assume
, Cover
, Past
, Stable
6 from nmigen
.cli
import rtlil
8 from nmutil
.formaltest
import FHDLTestCase
9 from nmutil
.gtkw
import write_gtkw
11 from soc
.experiment
.alu_fsm
import Shifter
14 # This defines a module to drive the device under test and assert
15 # properties about its outputs
16 class Driver(Elaboratable
):
27 m
.submodules
.dut
= dut
= Shifter(8)
28 # Coverage condition (one bit for each coverage case)
30 # input data to the shifter
36 # transaction count for each port
39 # keep data and valid stable, until accepted
40 with m
.If(Past(dut
.p
.valid_i
) & ~
Past(dut
.p
.ready_o
)):
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
)),
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
):
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),
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
65 sync
+= expected
.eq(dut_data_i
>> dut_shift_i
)
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)
78 comb
+= Assert(dut
.n
.data_o
.data
== expected
)
79 # cover zero data, with zero and non-zero shift
81 with m
.If(data_i
== 0):
82 with m
.If(shift_i
== 0):
84 with m
.If(shift_i
[:3].any() & ~shift_i
[3]):
86 # cover non-zero data, with zero and non-zero shift
88 with m
.If(data_i
!= 0):
89 with m
.If(shift_i
== 0):
91 with m
.If(shift_i
[:3].any() & ~shift_i
[3]):
97 with m
.If(shift_i
[3] != 0):
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()):
102 # dummy condition, to avoid optimizing-out the counters
103 with m
.If((write_cnt
!= 0) |
(read_cnt
!= 0)):
105 # check that each condition above occurred at least once
106 comb
+= Cover(cov
.all())
110 class ALUFSMTestCase(FHDLTestCase
):
111 def test_formal(self
):
114 'p_data_i[7:0]', 'p_shift_i[7:0]', 'op__sdir',
115 'p_valid_i', 'p_ready_o',
117 'n_valid_o', 'n_ready_i',
118 ('formal', {'module': 'top'}, [
119 'write_cnt[3:0]', 'read_cnt[3:0]', 'cov[7:0]'
123 'test_formal_cover_alu_fsm.gtkw',
124 os
.path
.dirname(__file__
) +
125 '/proof_alu_fsm_formal/engine_0/trace0.vcd',
131 'test_formal_bmc_alu_fsm.gtkw',
132 os
.path
.dirname(__file__
) +
133 '/proof_alu_fsm_formal/engine_0/trace.vcd',
139 'test_formal_induct_alu_fsm.gtkw',
140 os
.path
.dirname(__file__
) +
141 '/proof_alu_fsm_formal/engine_0/trace_induct.vcd',
147 self
.assertFormal(module
, mode
="prove", depth
=18)
148 self
.assertFormal(module
, mode
="cover", depth
=32)
153 vl
= rtlil
.convert(dut
, ports
=[])
154 with
open("alu_fsm.il", "w") as f
:
158 if __name__
== '__main__':