1 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
3 from nmigen
.asserts
import (Assert
, AnyConst
, Assume
, Cover
, Initial
,
4 Rose
, Fell
, Stable
, Past
)
5 from nmigen
.test
.utils
import FHDLTestCase
6 from nmigen
.cli
import rtlil
9 from soc
.fu
.compunits
.compunits
import FunctionUnitBaseSingle
10 from soc
.experiment
.alu_hier
import DummyALU
11 from soc
.experiment
.compalu_multi
import MultiCompUnit
12 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
14 class Driver(Elaboratable
):
18 def elaborate(self
, platform
):
23 m
.submodules
.dut
= dut
= MultiCompUnit(16, alu
,
36 has_issued
= Signal(reset
=0)
41 comb
+= Assume(has_issued
== 0)
42 comb
+= Assume(issue
== 0)
43 comb
+= Assume(go_rd
== 0)
44 comb
+= Assume(rst
== 1)
46 comb
+= Assume(rst
== 0)
48 # detect when issue has been raised and remember it
50 sync
+= has_issued
.eq(1)
51 comb
+= Cover(has_issued
)
53 # Property One: Rd_rel should never be asserted before issue
55 # If issue has never been raised, then rd_rel should never
57 with m
.If(rd_rel
!= 0):
58 comb
+= Assert(has_issued
)
60 # Property Two: when rd_rel is asserted, it should stay
61 # that way until a go_rd
62 with m
.If((Past(go_rd
) == 0) & ~
Past(go_die
)):
63 comb
+= Assert(~
Fell(rd_rel
))
65 # Property Three: when a bit in rd_rel is asserted, and
66 # the corresponding bit in go_rd is asserted, then that
67 # bit of rd_rel should be deasserted
69 with m
.If(Past(go_rd
)[i
] & (Past(rd_rel
) != 0)):
70 comb
+= Assert(rd_rel
[i
] == ~
Past(go_rd
)[i
])
72 # Property Four: Similarly, if rd_rel is asserted,
73 # asserting go_die should make rd_rel be deasserted
75 with m
.If(Past(rd_rel
) != 0):
76 with m
.If(Past(go_die
)):
77 comb
+= Assert(rd_rel
== 0)
79 comb
+= Cover(Fell(rd_rel
))
81 # Assume no instruction is issued until rd_rel is
82 # released. Idk if this is valid
84 with m
.If((rd_rel
!= 0) |
(Past(rd_rel
) != 0)):
85 comb
+= Assume(issue
== 0)
89 class FUTestCase(FHDLTestCase
):
90 def test_formal(self
):
92 self
.assertFormal(module
, mode
="bmc", depth
=5)
93 self
.assertFormal(module
, mode
="cover", depth
=5)
95 dut
= MultiCompUnit(16, DummyALU(16), CompALUOpSubset
)
96 vl
= rtlil
.convert(dut
, ports
=dut
.ports())
97 with
open("multicompunit.il", "w") as f
:
101 if __name__
== '__main__':