1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
5 * https://bugs.libre-soc.org/show_bug.cgi?id=331
6 * https://libre-soc.org/openpower/isa/fixedlogical/
9 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
11 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
12 from nmutil
.formaltest
import FHDLTestCase
13 from nmigen
.lib
.coding
import PriorityEncoder
14 from nmigen
.cli
import rtlil
16 from soc
.fu
.logical
.main_stage
import LogicalMainStage
17 from soc
.fu
.alu
.pipe_data
import ALUPipeSpec
18 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
19 from soc
.decoder
.power_enums
import MicrOp
23 def simple_popcount(sig
, width
):
24 """simple, naive (and obvious) popcount.
25 formal verification does not to be fast: it does have to be correct
28 for i
in range(width
):
29 result
= result
+ sig
[i
]
33 # This defines a module to drive the device under test and assert
34 # properties about its outputs
35 class Driver(Elaboratable
):
40 def elaborate(self
, platform
):
44 rec
= CompALUOpSubset()
45 # Setup random inputs for dut.op
48 comb
+= p
.eq(AnyConst(width
))
50 pspec
= ALUPipeSpec(id_wid
=2)
51 m
.submodules
.dut
= dut
= LogicalMainStage(pspec
)
53 # convenience variables
56 #carry_in = dut.i.xer_ca[0]
57 #carry_in32 = dut.i.xer_ca[1]
61 comb
+= [a
.eq(AnyConst(64)),
63 #carry_in.eq(AnyConst(0b11)),
66 comb
+= dut
.i
.ctx
.op
.eq(rec
)
68 # Assert that op gets copied from the input to output
69 for rec_sig
in rec
.ports():
71 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
72 comb
+= Assert(dut_sig
== rec_sig
)
74 # signed and signed/32 versions of input a
75 a_signed
= Signal(signed(64))
76 a_signed_32
= Signal(signed(32))
77 comb
+= a_signed
.eq(a
)
78 comb
+= a_signed_32
.eq(a
[0:32])
81 comb
+= o_ok
.eq(1) # will be set to zero if no op takes place
83 # main assertion of arithmetic operations
84 with m
.Switch(rec
.insn_type
):
85 with m
.Case(MicrOp
.OP_AND
):
86 comb
+= Assert(o
== a
& b
)
87 with m
.Case(MicrOp
.OP_OR
):
88 comb
+= Assert(o
== a | b
)
89 with m
.Case(MicrOp
.OP_XOR
):
90 comb
+= Assert(o
== a ^ b
)
92 with m
.Case(MicrOp
.OP_POPCNT
):
93 with m
.If(rec
.data_len
== 8):
94 comb
+= Assert(o
== simple_popcount(a
, 64))
95 with m
.If(rec
.data_len
== 4):
97 slc
= slice(i
*32, (i
+1)*32)
98 comb
+= Assert(o
[slc
] == simple_popcount(a
[slc
], 32))
99 with m
.If(rec
.data_len
== 1):
101 slc
= slice(i
*8, (i
+1)*8)
102 comb
+= Assert(o
[slc
] == simple_popcount(a
[slc
], 8))
104 with m
.Case(MicrOp
.OP_PRTY
):
105 with m
.If(rec
.data_len
== 8):
108 result
= result ^ a
[i
*8]
109 comb
+= Assert(o
== result
)
110 with m
.If(rec
.data_len
== 4):
114 result_low
= result_low ^ a
[i
*8]
115 result_high
= result_high ^ a
[i
*8 + 32]
116 comb
+= Assert(o
[0:32] == result_low
)
117 comb
+= Assert(o
[32:64] == result_high
)
119 with m
.Case(MicrOp
.OP_CNTZ
):
120 XO
= dut
.fields
.FormX
.XO
[0:-1]
121 with m
.If(rec
.is_32bit
):
122 m
.submodules
.pe32
= pe32
= PriorityEncoder(32)
123 peo
= Signal(range(0, 32+1))
127 comb
+= peo
.eq(pe32
.o
)
128 with m
.If(XO
[-1]): # cnttzw
129 comb
+= pe32
.i
.eq(a
[0:32])
130 comb
+= Assert(o
== peo
)
131 with m
.Else(): # cntlzw
132 comb
+= pe32
.i
.eq(a
[0:32][::-1])
133 comb
+= Assert(o
== peo
)
135 m
.submodules
.pe64
= pe64
= PriorityEncoder(64)
140 comb
+= peo64
.eq(pe64
.o
)
141 with m
.If(XO
[-1]): # cnttzd
142 comb
+= pe64
.i
.eq(a
[0:64])
143 comb
+= Assert(o
== peo64
)
144 with m
.Else(): # cntlzd
145 comb
+= pe64
.i
.eq(a
[0:64][::-1])
146 comb
+= Assert(o
== peo64
)
148 with m
.Case(MicrOp
.OP_CMPB
):
150 slc
= slice(i
*8, (i
+1)*8)
151 with m
.If(a
[slc
] == b
[slc
]):
152 comb
+= Assert(o
[slc
] == 0xff)
154 comb
+= Assert(o
[slc
] == 0)
156 with m
.Case(MicrOp
.OP_BPERM
):
157 # note that this is a copy of the beautifully-documented
159 comb
+= Assert(o
[8:] == 0)
162 with m
.If(index
>= 64):
163 comb
+= Assert(o
[i
] == 0)
166 with m
.If(index
== j
):
167 comb
+= Assert(o
[i
] == b
[63-j
])
172 # check that data ok was only enabled when op actioned
173 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
178 class LogicalTestCase(FHDLTestCase
):
179 def test_formal(self
):
181 self
.assertFormal(module
, mode
="bmc", depth
=2)
182 self
.assertFormal(module
, mode
="cover", depth
=2)
183 def test_ilang(self
):
185 vl
= rtlil
.convert(dut
, ports
=[])
186 with
open("main_stage.il", "w") as f
:
190 if __name__
== '__main__':