c1e71536d65546794734e336a5b77948285a9b5b
1 # Proof of correctness for ALU pipeline, main 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
, Repl
,
12 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
13 from nmutil
.formaltest
import FHDLTestCase
14 from nmigen
.cli
import rtlil
16 from soc
.fu
.alu
.main_stage
import ALUMainStage
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 InternalOp
23 # This defines a module to drive the device under test and assert
24 # properties about its outputs
25 class Driver(Elaboratable
):
30 def elaborate(self
, platform
):
34 rec
= CompALUOpSubset()
35 # Setup random inputs for dut.op
38 comb
+= p
.eq(AnyConst(width
))
40 pspec
= ALUPipeSpec(id_wid
=2)
41 m
.submodules
.dut
= dut
= ALUMainStage(pspec
)
43 # convenience variables
46 ca_in
= dut
.i
.xer_ca
[0] # CA carry in
47 ca32_in
= dut
.i
.xer_ca
[1] # CA32 carry in 32
48 so_in
= dut
.i
.xer_so
# SO sticky overflow
50 ca_o
= dut
.o
.xer_ca
.data
[0] # CA carry out
51 ca32_o
= dut
.o
.xer_ca
.data
[1] # CA32 carry out32
52 ov_o
= dut
.o
.xer_ov
.data
[0] # OV overflow
53 ov32_o
= dut
.o
.xer_ov
.data
[1] # OV32 overflow32
57 comb
+= [a
.eq(AnyConst(64)),
59 ca_in
.eq(AnyConst(0b11)),
60 so_in
.eq(AnyConst(1))]
62 comb
+= dut
.i
.ctx
.op
.eq(rec
)
64 # Assert that op gets copied from the input to output
65 for rec_sig
in rec
.ports():
67 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
68 comb
+= Assert(dut_sig
== rec_sig
)
70 # signed and signed/32 versions of input a
71 a_signed
= Signal(signed(64))
72 a_signed_32
= Signal(signed(32))
73 comb
+= a_signed
.eq(a
)
74 comb
+= a_signed_32
.eq(a
[0:32])
76 # do not check MSBs of a/b in 32-bit mode
77 with m
.If(rec
.is_32bit
):
78 comb
+= Assume(a
[32:64] == 0)
79 comb
+= Assume(b
[32:64] == 0)
81 # Data.ok checking. these only to be valid when there is a change
82 # in the output that needs to go into a regfile
91 # main assertion of arithmetic operations
92 with m
.Switch(rec
.insn_type
):
93 with m
.Case(InternalOp
.OP_ADD
):
95 # check result of 65-bit add-with-carry
96 comb
+= Assert(Cat(o
, ca_o
) == (a
+ b
+ ca_in
))
98 # CA32 - XXX note this fails! replace with ca_in and it works
99 comb
+= Assert((a
[0:32] + b
[0:32] + ca_in
)[32] == ca32_o
)
101 # From microwatt execute1.vhdl line 130, calc_ov() function
102 comb
+= Assert(ov_o
== ((ca_o ^ o
[-1]) & ~
(a
[-1] ^ b
[-1])))
103 comb
+= Assert(ov32_o
== ((ca32_o ^ o
[31]) & ~
(a
[31] ^ b
[31])))
108 with m
.Case(InternalOp
.OP_EXTS
):
110 with m
.If(rec
.data_len
== i
):
111 # main part, then sign-bit replicated up
112 comb
+= Assert(o
[0:i
*8] == a
[0:i
*8])
113 comb
+= Assert(o
[i
*8:64] == Repl(a
[i
*8-1], 64-(i
*8)))
116 with m
.Case(InternalOp
.OP_CMP
):
117 # CMP is defined as not taking in carry
118 comb
+= Assume(ca_in
== 0)
119 comb
+= Assert(o
== (a
+b
)[0:64])
121 with m
.Case(InternalOp
.OP_CMPEQB
):
125 comb
+= eqs
[i
].eq(src1
== b
[i
*8:(i
+1)*8])
126 comb
+= Assert(dut
.o
.cr0
.data
[2] == eqs
.any())
129 # check that data ok was only enabled when op actioned
130 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
131 comb
+= Assert(dut
.o
.cr0
.ok
== cr0_ok
)
132 comb
+= Assert(dut
.o
.xer_ov
.ok
== ov_ok
)
133 comb
+= Assert(dut
.o
.xer_ca
.ok
== ca_ok
)
138 class ALUTestCase(FHDLTestCase
):
139 def test_formal(self
):
141 self
.assertFormal(module
, mode
="bmc", depth
=2)
142 self
.assertFormal(module
, mode
="cover", depth
=2)
143 def test_ilang(self
):
145 vl
= rtlil
.convert(dut
, ports
=[])
146 with
open("alu_main_stage.il", "w") as f
:
150 if __name__
== '__main__':