1 # Proof of correctness for ALU pipeline, output stage
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
5 * https://bugs.libre-soc.org/show_bug.cgi?id=306
6 * https://bugs.libre-soc.org/show_bug.cgi?id=305
7 * https://bugs.libre-soc.org/show_bug.cgi?id=343
10 from nmigen
import Module
, Signal
, Elaboratable
, Mux
, Cat
, signed
11 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
12 from nmutil
.formaltest
import FHDLTestCase
13 from nmigen
.cli
import rtlil
15 from soc
.fu
.alu
.output_stage
import ALUOutputStage
16 from soc
.fu
.alu
.pipe_data
import ALUPipeSpec
17 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
18 from soc
.decoder
.power_enums
import MicrOp
22 # This defines a module to drive the device under test and assert
23 # properties about its outputs
24 class Driver(Elaboratable
):
29 def elaborate(self
, platform
):
33 rec
= CompALUOpSubset()
35 # Setup random inputs for dut.op
39 comb
+= p
.eq(AnyConst(width
))
41 pspec
= ALUPipeSpec(id_wid
=2)
42 m
.submodules
.dut
= dut
= ALUOutputStage(pspec
)
46 carry_out32
= Signal()
51 comb
+= [dut
.i
.o
.eq(o
),
52 dut
.i
.xer_ca
[0].eq(carry_out
),
54 dut
.i
.xer_ca
[1].eq(carry_out32
),
56 dut
.i
.xer_ov
[0].eq(ov
),
57 dut
.i
.xer_ov
[1].eq(ov32
),
59 carry_out
.eq(AnyConst(1)),
60 carry_out32
.eq(AnyConst(1)),
66 comb
+= dut
.i
.ctx
.op
.eq(rec
)
68 with m
.If(dut
.i
.ctx
.op
.invert_out
):
69 comb
+= Assert(dut
.o
.o
== ~o
)
71 comb
+= Assert(dut
.o
.o
== o
)
73 cr_out
= Signal
.like(cr0
)
74 comb
+= cr_out
.eq(dut
.o
.cr0
)
76 o_signed
= Signal(signed(64))
77 comb
+= o_signed
.eq(dut
.o
.o
)
78 # Assert only one of the comparison bits is set
79 comb
+= Assert(cr_out
[3] + cr_out
[2] + cr_out
[1] == 1)
80 with m
.If(o_signed
== 0):
81 comb
+= Assert(cr_out
[1] == 1)
82 with m
.Elif(o_signed
> 0):
83 # sigh. see https://bugs.libre-soc.org/show_bug.cgi?id=305#c61
84 # for OP_CMP we do b-a rather than a-b (just like ADD) and
85 # then invert the *test condition*.
86 with m
.If(rec
.insn_type
== MicrOp
.OP_CMP
):
87 comb
+= Assert(cr_out
[3] == 1)
89 comb
+= Assert(cr_out
[2] == 1)
90 with m
.Elif(o_signed
< 0):
92 with m
.If(rec
.insn_type
== MicrOp
.OP_CMP
):
93 comb
+= Assert(cr_out
[2] == 1)
95 comb
+= Assert(cr_out
[3] == 1)
97 # Assert that op gets copied from the input to output
101 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
102 comb
+= Assert(dut_sig
== rec_sig
)
106 class GTCombinerTestCase(FHDLTestCase
):
107 def test_formal(self
):
109 self
.assertFormal(module
, mode
="bmc", depth
=4)
110 self
.assertFormal(module
, mode
="cover", depth
=4)
111 def test_ilang(self
):
113 vl
= rtlil
.convert(dut
, ports
=[])
114 with
open("output_stage.il", "w") as f
:
118 if __name__
== '__main__':