cfa936e1cfb0241201a3fce0b4f5d36aa57d1b5d
1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
3 # Copyright (C) 2020 Tobias Platen <tplaten@posteo.de>
5 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
7 from nmigen
.asserts
import Assert
, AnyConst
, AnySeq
, Assume
, Cover
8 from nmigen
.test
.utils
import FHDLTestCase
9 from nmigen
.cli
import rtlil
11 from soc
.experiment
.l0_cache
import DataMerger
16 # This defines a module to drive the device under test and assert
17 # properties about its outputs
18 class Driver(Elaboratable
):
23 def elaborate(self
, platform
):
28 m
.submodules
.dut
= dut
= DataMerger(array_size
)
30 # assign anyseq to inputs
31 for j
in range(dut
.array_size
):
32 comb
+= dut
.addr_array_i
[j
].eq(AnySeq(dut
.array_size
))
33 comb
+= dut
.data_i
[j
].eq(AnySeq(16+128))
36 for j
in range(dut
.array_size
):
37 allzero
= (dut
.addr_array_i
[j
] == 0) & allzero
39 # assert that the output is zero when the datamerger is idle
41 comb
+= Assert(dut
.data_o
== 0)
43 comb
+= Assume(dut
.data_o
!= 0) # at least one output bit is set
44 for j
in range(dut
.array_size
):
46 with m
.If(dut
.data_o
.en
[b
]):
47 comb
+= Assume(dut
.data_i
[j
].en
[b
])
48 for b
in range(0,128):
49 with m
.If(dut
.data_o
.data
[b
]):
50 comb
+= Assume(dut
.data_i
[j
].data
[b
])
55 class DataMergerTestCase(FHDLTestCase
):
56 def test_formal(self
):
58 # bounded model check first
59 self
.assertFormal(module
, mode
="bmc", depth
=2)
60 # self.assertFormal(module, mode="cover", depth=2) # case can happen
61 # XXX self.assertFormal(module, mode="prove") # uses induction
65 vl
= rtlil
.convert(dut
, ports
=[])
66 with
open("main_stage.il", "w") as f
:
70 if __name__
== '__main__':