1 # Proof of correctness for FSGNJ module
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen
import Module
, Signal
, Elaboratable
5 from nmigen
.asserts
import Assert
, Assume
6 from nmigen
.test
.utils
import FHDLTestCase
8 from ieee754
.fpcommon
.fpbase
import FPNumDecode
, FPNumBaseRecord
9 from ieee754
.fsgnj
.fsgnj
import FSGNJPipeMod
10 from ieee754
.pipeline
import PipelineSpec
13 # This defines a module to drive the device under test and assert
14 # properties about its outputs
15 class FSGNJDriver(Elaboratable
):
16 def __init__(self
, pspec
):
19 self
.a
= Signal(pspec
.width
)
20 self
.b
= Signal(pspec
.width
)
21 self
.z
= Signal(pspec
.width
)
22 self
.opc
= Signal(pspec
.op_wid
)
23 self
.muxid
= Signal(pspec
.id_wid
)
25 def elaborate(self
, platform
):
28 m
.submodules
.dut
= dut
= FSGNJPipeMod(self
.pspec
)
30 a1
= FPNumBaseRecord(self
.pspec
.width
, False)
31 b1
= FPNumBaseRecord(self
.pspec
.width
, False)
32 z1
= FPNumBaseRecord(self
.pspec
.width
, False)
33 m
.submodules
.sc_decode_a
= a1
= FPNumDecode(None, a1
)
34 m
.submodules
.sc_decode_b
= b1
= FPNumDecode(None, b1
)
35 m
.submodules
.sc_decode_z
= z1
= FPNumDecode(None, z1
)
37 m
.d
.comb
+= [a1
.v
.eq(self
.a
),
41 # connect up the inputs and outputs. I think these could
42 # theoretically be $anyconst/$anysync but I'm not sure nmigen
43 # has support for that
44 m
.d
.comb
+= dut
.i
.a
.eq(self
.a
)
45 m
.d
.comb
+= dut
.i
.b
.eq(self
.b
)
46 m
.d
.comb
+= dut
.i
.ctx
.op
.eq(self
.opc
)
47 m
.d
.comb
+= dut
.i
.muxid
.eq(self
.muxid
)
48 m
.d
.comb
+= self
.z
.eq(dut
.o
.z
)
50 # Since the RISCV spec doesn't define what FSGNJ with a funct3
51 # field of 0b011 throug 0b111 does, they should be ignored.
52 m
.d
.comb
+= Assume(self
.opc
!= 0b11)
54 # The RISCV spec (page 70) says FSGNJ "produces a result that
55 # takes all buts except the sign bit from [operand 1]". This
56 # asserts that that holds true
57 m
.d
.comb
+= Assert(z1
.e
== a1
.e
)
58 m
.d
.comb
+= Assert(z1
.m
== a1
.m
)
60 with m
.Switch(self
.opc
):
62 # The RISCV Spec (page 70) states that for FSGNJ (opcode
63 # 0b00 in this case) "the result's sign bit is [operand
66 m
.d
.comb
+= Assert(z1
.s
== b1
.s
)
68 # The RISCV Spec (page 70) states that for FSGNJN (opcode
69 # 0b01 in this case) "the result's sign bit is the opposite
70 # of [operand 2's] sign bit"
72 m
.d
.comb
+= Assert(z1
.s
== ~b1
.s
)
73 # The RISCV Spec (page 70) states that for FSGNJX (opcode
74 # 0b10 in this case) "the result's sign bit is the XOR of
75 # the sign bits of [operand 1] and [operand 2]"
77 m
.d
.comb
+= Assert(z1
.s
== (a1
.s ^ b1
.s
))
82 return [self
.a
, self
.b
, self
.z
, self
.opc
, self
.muxid
]
85 class FPMAXTestCase(FHDLTestCase
):
87 for bits
in [16, 32, 64]:
88 module
= FSGNJDriver(PipelineSpec(bits
, 2, 2))
89 self
.assertFormal(module
, mode
="bmc", depth
=4)
92 if __name__
== '__main__':