1 from nmigen
import Module
, Signal
, Elaboratable
, Cat
2 from nmigen
.asserts
import Assert
, AnyConst
, Assume
3 from nmutil
.formaltest
import FHDLTestCase
5 from openpower
.decoder
.power_decoder
import create_pdecode
, PowerOp
6 from openpower
.decoder
.power_enums
import (In1Sel
, In2Sel
, In3Sel
,
7 OutSel
, RCOE
, Form
, Function
,
10 from openpower
.decoder
.power_decoder2
import (PowerDecode2
,
11 Decode2ToExecute1Type
)
16 class Driver(Elaboratable
):
18 self
.instruction
= Signal(32, reset_less
=True)
22 def elaborate(self
, platform
):
24 self
.comb
= self
.m
.d
.comb
25 self
.instruction
= Signal(32)
27 self
.comb
+= self
.instruction
.eq(AnyConst(32))
29 pdecode
= create_pdecode()
31 self
.m
.submodules
.pdecode2
= pdecode2
= PowerDecode2(pdecode
)
33 self
.comb
+= pdecode2
.dec
.bigendian
.eq(1) # TODO: bigendian=0
34 self
.comb
+= pdecode2
.dec
.raw_opcode_in
.eq(self
.instruction
)
36 # ignore special decoding of nop
37 self
.comb
+= Assume(self
.instruction
!= 0x60000000)
39 #self.assert_dec1_decode(dec1, dec1.dec)
41 self
.assert_form(dec1
, pdecode2
)
44 def assert_dec1_decode(self
, dec1
, decoders
):
45 if not isinstance(decoders
, list):
49 opcode_switch
= Signal(d
.bitsel
[1] - d
.bitsel
[0])
50 self
.comb
+= opcode_switch
.eq(
51 self
.instruction
[d
.bitsel
[0]:d
.bitsel
[1]])
52 with self
.m
.Switch(opcode_switch
):
53 self
.handle_subdecoders(dec1
, d
)
55 opcode
= row
['opcode']
56 if d
.opint
and '-' not in opcode
:
57 opcode
= int(opcode
, 0)
60 with self
.m
.Case(opcode
):
61 self
.comb
+= self
.assert_dec1_signals(dec1
, row
)
62 with self
.m
.Default():
63 self
.comb
+= Assert(dec
.op
.internal_op
==
66 def handle_subdecoders(self
, dec1
, decoders
):
67 for dec
in decoders
.subdecoders
:
68 if isinstance(dec
, list):
69 pattern
= dec
[0].pattern
72 with self
.m
.Case(pattern
):
73 self
.assert_dec1_decode(dec1
, dec
)
75 def assert_dec1_signals(self
, dec
, row
):
77 return [Assert(op
.function_unit
== Function
[row
['unit']]),
78 Assert(op
.internal_op
== MicrOp
[row
['internal op']]),
79 Assert(op
.in1_sel
== In1Sel
[row
['in1']]),
80 Assert(op
.in2_sel
== In2Sel
[row
['in2']]),
81 Assert(op
.in3_sel
== In3Sel
[row
['in3']]),
82 Assert(op
.out_sel
== OutSel
[row
['out']]),
83 Assert(op
.ldst_len
== LdstLen
[row
['ldst len']]),
84 Assert(op
.rc_sel
== RCOE
[row
['rc']]),
85 Assert(op
.cry_in
== CryIn
[row
['cry in']]),
86 Assert(op
.form
== Form
[row
['form']]),
89 # This is to assert that the decoder conforms to the table listed
90 # in PowerISA public spec v3.0B, Section 1.6, page 12
91 def assert_form(self
, dec
, dec2
):
92 with self
.m
.Switch(dec
.op
.form
):
93 with self
.m
.Case(Form
.A
):
94 self
.comb
+= Assert(dec
.op
.in1_sel
.matches(
95 In1Sel
.NONE
, In1Sel
.RA
, In1Sel
.RA_OR_ZERO
))
96 self
.comb
+= Assert(dec
.op
.in2_sel
.matches(
97 In2Sel
.RB
, In2Sel
.NONE
))
98 self
.comb
+= Assert(dec
.op
.in3_sel
.matches(
99 In3Sel
.RS
, In3Sel
.NONE
))
100 self
.comb
+= Assert(dec
.op
.out_sel
.matches(
101 OutSel
.NONE
, OutSel
.RT
))
102 # The table has fields for XO and Rc, but idk what they correspond to
103 with self
.m
.Case(Form
.B
):
105 with self
.m
.Case(Form
.D
):
106 self
.comb
+= Assert(dec
.op
.in1_sel
.matches(
107 In1Sel
.NONE
, In1Sel
.RA
, In1Sel
.RA_OR_ZERO
))
108 self
.comb
+= Assert(dec
.op
.in2_sel
.matches(
109 In2Sel
.CONST_UI
, In2Sel
.CONST_SI
, In2Sel
.CONST_UI_HI
,
111 self
.comb
+= Assert(dec
.op
.out_sel
.matches(
112 OutSel
.NONE
, OutSel
.RT
, OutSel
.RA
))
113 with self
.m
.Case(Form
.I
):
114 self
.comb
+= Assert(dec
.op
.in2_sel
.matches(
117 def instr_bits(self
, start
, end
=None):
120 return self
.instruction
[::-1][start
:end
+1]
123 class DecoderTestCase(FHDLTestCase
):
124 @unittest.expectedFailure
# FIXME: proof failed:
125 # self.comb += Assert(dec.op.out_sel.matches(
126 # OutSel.NONE, OutSel.RT, OutSel.RA))
127 def test_decoder(self
):
129 self
.assertFormal(module
, mode
="bmc", depth
=4)
132 if __name__
== '__main__':