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 # This defines a module to drive the device under test and assert
24 # properties about its outputs
25 class Driver(Elaboratable
):
30 def popcount(self
, sig
, width
):
32 for i
in range(width
):
33 result
= result
+ sig
[i
]
36 def elaborate(self
, platform
):
40 rec
= CompALUOpSubset()
42 # Setup random inputs for dut.op
46 comb
+= p
.eq(AnyConst(width
))
48 pspec
= ALUPipeSpec(id_wid
=2, op_wid
=recwidth
)
49 m
.submodules
.dut
= dut
= LogicalMainStage(pspec
)
51 # convenience variables
54 carry_in
= dut
.i
.xer_ca
[0]
55 carry_in32
= dut
.i
.xer_ca
[1]
60 comb
+= [a
.eq(AnyConst(64)),
62 carry_in
.eq(AnyConst(0b11)),
63 so_in
.eq(AnyConst(1))]
65 comb
+= dut
.i
.ctx
.op
.eq(rec
)
67 # Assert that op gets copied from the input to output
68 for rec_sig
in rec
.ports():
70 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
71 comb
+= Assert(dut_sig
== rec_sig
)
73 # signed and signed/32 versions of input a
74 a_signed
= Signal(signed(64))
75 a_signed_32
= Signal(signed(32))
76 comb
+= a_signed
.eq(a
)
77 comb
+= a_signed_32
.eq(a
[0:32])
79 # main assertion of arithmetic operations
80 with m
.Switch(rec
.insn_type
):
81 with m
.Case(MicrOp
.OP_AND
):
82 comb
+= Assert(dut
.o
.o
== a
& b
)
83 with m
.Case(MicrOp
.OP_OR
):
84 comb
+= Assert(dut
.o
.o
== a | b
)
85 with m
.Case(MicrOp
.OP_XOR
):
86 comb
+= Assert(dut
.o
.o
== a ^ b
)
88 with m
.Case(MicrOp
.OP_POPCNT
):
89 with m
.If(rec
.data_len
== 8):
90 comb
+= Assert(dut
.o
.o
== self
.popcount(a
, 64))
91 with m
.If(rec
.data_len
== 4):
94 comb
+= Assert(dut
.o
.o
[i
*32:(i
+1)*32] ==
95 self
.popcount(a
[i
*32:(i
+1)*32], 32))
96 with m
.If(rec
.data_len
== 1):
98 comb
+= Assert(dut
.o
.o
[i
*8:(i
+1)*8] ==
99 self
.popcount(a
[i
*8:(i
+1)*8], 8))
101 with m
.Case(MicrOp
.OP_PRTY
):
102 with m
.If(rec
.data_len
== 8):
105 result
= result ^ a
[i
*8]
106 comb
+= Assert(dut
.o
.o
== result
)
107 with m
.If(rec
.data_len
== 4):
111 result_low
= result_low ^ a
[i
*8]
112 result_high
= result_high ^ a
[i
*8 + 32]
113 comb
+= Assert(dut
.o
.o
[0:32] == result_low
)
114 comb
+= Assert(dut
.o
.o
[32:64] == result_high
)
115 with m
.Case(MicrOp
.OP_CNTZ
):
116 XO
= dut
.fields
.FormX
.XO
[0:-1]
117 with m
.If(rec
.is_32bit
):
118 m
.submodules
.pe32
= pe32
= PriorityEncoder(32)
119 peo
= Signal(range(0, 32+1))
123 comb
+= peo
.eq(pe32
.o
)
124 with m
.If(XO
[-1]): # cnttzw
125 comb
+= pe32
.i
.eq(a
[0:32])
126 comb
+= Assert(dut
.o
.o
== peo
)
127 with m
.Else(): # cntlzw
128 comb
+= pe32
.i
.eq(a
[0:32][::-1])
129 comb
+= Assert(dut
.o
.o
== peo
)
131 m
.submodules
.pe64
= pe64
= PriorityEncoder(64)
136 comb
+= peo64
.eq(pe64
.o
)
137 with m
.If(XO
[-1]): # cnttzd
138 comb
+= pe64
.i
.eq(a
[0:64])
139 comb
+= Assert(dut
.o
.o
== peo64
)
140 with m
.Else(): # cntlzd
141 comb
+= pe64
.i
.eq(a
[0:64][::-1])
142 comb
+= Assert(dut
.o
.o
== peo64
)
148 class LogicalTestCase(FHDLTestCase
):
149 def test_formal(self
):
151 self
.assertFormal(module
, mode
="bmc", depth
=2)
152 self
.assertFormal(module
, mode
="cover", depth
=2)
153 def test_ilang(self
):
155 vl
= rtlil
.convert(dut
, ports
=[])
156 with
open("main_stage.il", "w") as f
:
160 if __name__
== '__main__':