rename proof_decoder*.py -> test_decoder*.py so it gets run by pytest
authorJacob Lifshay <programmerjake@gmail.com>
Fri, 2 Sep 2022 06:06:56 +0000 (23:06 -0700)
committerJacob Lifshay <programmerjake@gmail.com>
Fri, 2 Sep 2022 06:06:56 +0000 (23:06 -0700)
src/openpower/decoder/formal/proof_decoder.py [deleted file]
src/openpower/decoder/formal/proof_decoder2.py [deleted file]
src/openpower/decoder/formal/test_decoder.py [new file with mode: 0644]
src/openpower/decoder/formal/test_decoder2.py [new file with mode: 0644]

diff --git a/src/openpower/decoder/formal/proof_decoder.py b/src/openpower/decoder/formal/proof_decoder.py
deleted file mode 100644 (file)
index ae53efb..0000000
+++ /dev/null
@@ -1,128 +0,0 @@
-from nmigen import Module, Signal, Elaboratable, Cat
-from nmigen.asserts import Assert, AnyConst, Assume
-from nmutil.formaltest import FHDLTestCase
-
-from openpower.decoder.power_decoder import create_pdecode, PowerOp
-from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
-                                     OutSel, RC, Form, Function,
-                                     LdstLen, CryIn,
-                                     MicrOp, get_csv)
-from openpower.decoder.power_decoder2 import (PowerDecode2,
-                                        Decode2ToExecute1Type)
-import unittest
-import pdb
-
-class Driver(Elaboratable):
-    def __init__(self):
-        self.instruction = Signal(32, reset_less=True)
-        self.m = None
-        self.comb = None
-
-    def elaborate(self, platform):
-        self.m = Module()
-        self.comb = self.m.d.comb
-        self.instruction = Signal(32)
-
-        self.comb += self.instruction.eq(AnyConst(32))
-
-        pdecode = create_pdecode()
-
-        self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
-        dec1 = pdecode2.dec
-        self.comb += pdecode2.dec.bigendian.eq(1) # TODO: bigendian=0
-        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
-
-        # ignore special decoding of nop
-        self.comb += Assume(self.instruction != 0x60000000)
-
-        #self.assert_dec1_decode(dec1, dec1.dec)
-
-        self.assert_form(dec1, pdecode2)
-        return self.m
-
-    def assert_dec1_decode(self, dec1, decoders):
-        if not isinstance(decoders, list):
-            decoders = [decoders]
-        for d in decoders:
-            print(d.pattern)
-            opcode_switch = Signal(d.bitsel[1] - d.bitsel[0])
-            self.comb += opcode_switch.eq(
-                self.instruction[d.bitsel[0]:d.bitsel[1]])
-            with self.m.Switch(opcode_switch):
-                self.handle_subdecoders(dec1, d)
-                for row in d.opcodes:
-                    opcode = row['opcode']
-                    if d.opint and '-' not in opcode:
-                        opcode = int(opcode, 0)
-                    if not row['unit']:
-                        continue
-                    with self.m.Case(opcode):
-                        self.comb += self.assert_dec1_signals(dec1, row)
-                with self.m.Default():
-                    self.comb += Assert(dec.op.internal_op ==
-                                        MicrOp.OP_ILLEGAL)
-                                        
-
-    def handle_subdecoders(self, dec1, decoders):
-        for dec in decoders.subdecoders:
-            if isinstance(dec, list):
-                pattern = dec[0].pattern
-            else:
-                pattern = dec.pattern
-            with self.m.Case(pattern):
-                self.assert_dec1_decode(dec1, dec)
-
-    def assert_dec1_signals(self, dec, row):
-        op = dec.op
-        return [Assert(op.function_unit == Function[row['unit']]),
-                Assert(op.internal_op == MicrOp[row['internal op']]),
-                Assert(op.in1_sel == In1Sel[row['in1']]),
-                Assert(op.in2_sel == In2Sel[row['in2']]),
-                Assert(op.in3_sel == In3Sel[row['in3']]),
-                Assert(op.out_sel == OutSel[row['out']]),
-                Assert(op.ldst_len == LdstLen[row['ldst len']]),
-                Assert(op.rc_sel == RC[row['rc']]),
-                Assert(op.cry_in == CryIn[row['cry in']]),
-                Assert(op.form == Form[row['form']]),
-                ]
-
-    # This is to assert that the decoder conforms to the table listed
-    # in PowerISA public spec v3.0B, Section 1.6, page 12
-    def assert_form(self, dec, dec2):
-        with self.m.Switch(dec.op.form):
-            with self.m.Case(Form.A):
-                self.comb += Assert(dec.op.in1_sel.matches(
-                    In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
-                self.comb += Assert(dec.op.in2_sel.matches(
-                    In2Sel.RB, In2Sel.NONE))
-                self.comb += Assert(dec.op.in3_sel.matches(
-                    In3Sel.RS, In3Sel.NONE))
-                self.comb += Assert(dec.op.out_sel.matches(
-                    OutSel.NONE, OutSel.RT))
-                # The table has fields for XO and Rc, but idk what they correspond to
-            with self.m.Case(Form.B):
-                pass
-            with self.m.Case(Form.D):
-                self.comb += Assert(dec.op.in1_sel.matches(
-                    In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
-                self.comb += Assert(dec.op.in2_sel.matches(
-                    In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
-                    In2Sel.CONST_SI_HI))
-                self.comb += Assert(dec.op.out_sel.matches(
-                    OutSel.NONE, OutSel.RT, OutSel.RA))
-            with self.m.Case(Form.I):
-                self.comb += Assert(dec.op.in2_sel.matches(
-                    In2Sel.CONST_LI))
-
-    def instr_bits(self, start, end=None):
-        if not end:
-            end = start
-        return self.instruction[::-1][start:end+1]
-
-class DecoderTestCase(FHDLTestCase):
-    def test_decoder(self):
-        module = Driver()
-        self.assertFormal(module, mode="bmc", depth=4)
-
-if __name__ == '__main__':
-    unittest.main()
diff --git a/src/openpower/decoder/formal/proof_decoder2.py b/src/openpower/decoder/formal/proof_decoder2.py
deleted file mode 100644 (file)
index 87f6919..0000000
+++ /dev/null
@@ -1,216 +0,0 @@
-from nmigen import Module, Signal, Elaboratable, Cat, Repl
-from nmigen.asserts import Assert, AnyConst
-from nmutil.formaltest import FHDLTestCase
-
-from openpower.decoder.power_decoder import create_pdecode, PowerOp
-from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
-                                           OutSel, RC, Form,
-                                           MicrOp, SPRfull as SPR)
-from openpower.decoder.power_decoder2 import (PowerDecode2,
-                                              Decode2ToExecute1Type)
-import unittest
-
-
-class Driver(Elaboratable):
-    def __init__(self):
-        self.m = None
-        self.comb = None
-        self.instruction = None
-
-    def elaborate(self, platform):
-        self.m = Module()
-        self.comb = self.m.d.comb
-        self.instruction = Signal(32)
-
-        self.comb += self.instruction.eq(AnyConst(32))
-
-        pdecode = create_pdecode()
-
-        self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
-        self.comb += pdecode2.dec.bigendian.eq(1)  # XXX TODO: bigendian=0
-        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
-
-        self.test_in1(pdecode2, pdecode)
-        self.test_in2()
-        self.test_in2_fields()
-        self.test_in3()
-        self.test_out()
-        self.test_rc()
-        self.test_single_bits()
-
-        return self.m
-
-    def test_in1(self, pdecode2, pdecode):
-        m = self.m
-        comb = self.comb
-        ra = self.instr_bits(11, 15)
-        with m.If(pdecode.op.in1_sel == In1Sel.RA):
-            comb += Assert(pdecode2.e.read_reg1.data == ra)
-            comb += Assert(pdecode2.e.read_reg1.ok == 1)
-        with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
-            with m.If(ra == 0):
-                comb += Assert(pdecode2.e.read_reg1.ok == 0)
-            with m.Else():
-                comb += Assert(pdecode2.e.read_reg1.data == ra)
-                comb += Assert(pdecode2.e.read_reg1.ok == 1)
-                op = pdecode.op.internal_op
-        with m.If((op == MicrOp.OP_BC) |
-                  (op == MicrOp.OP_BCREG)):
-            with m.If(~self.instr_bits(8)):
-                comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
-                comb += Assert(pdecode2.e.read_spr1.ok == 1)
-        with m.If((op == MicrOp.OP_MFSPR) |
-                  (op == MicrOp.OP_MTSPR)):
-            comb += Assert(pdecode2.e.read_spr1.data ==
-                           self.instr_bits(11, 20))
-            comb += Assert(pdecode2.e.read_spr1.ok == 1)
-
-    def test_in2(self):
-        m = self.m
-        comb = self.comb
-        pdecode2 = m.submodules.pdecode2
-        dec = pdecode2.dec
-        with m.If(dec.op.in2_sel == In2Sel.RB):
-            comb += Assert(pdecode2.e.read_reg2.ok == 1)
-            comb += Assert(pdecode2.e.read_reg2.data == dec.RB)
-        with m.Elif(dec.op.in2_sel == In2Sel.NONE):
-            comb += Assert(pdecode2.e.imm_data.ok == 0)
-            comb += Assert(pdecode2.e.read_reg2.ok == 0)
-        with m.Elif(dec.op.in2_sel == In2Sel.SPR):
-            comb += Assert(pdecode2.e.imm_data.ok == 0)
-            comb += Assert(pdecode2.e.read_reg2.ok == 0)
-            comb += Assert(pdecode2.e.read_spr2.ok == 1)
-            with m.If(dec.fields.FormXL.XO[9]):
-                comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR)
-            with m.Else():
-                comb += Assert(pdecode2.e.read_spr2.data == SPR.LR)
-        with m.Else():
-            comb += Assert(pdecode2.e.imm_data.ok == 1)
-            with m.Switch(dec.op.in2_sel):
-                with m.Case(In2Sel.CONST_UI):
-                    comb += Assert(pdecode2.e.imm_data.data == dec.UI)
-                with m.Case(In2Sel.CONST_SI):
-                    comb += Assert(pdecode2.e.imm_data.data ==
-                                   self.exts(dec.SI, 16, 64))
-                with m.Case(In2Sel.CONST_UI_HI):
-                    comb += Assert(pdecode2.e.imm_data.data == (dec.UI << 16))
-                with m.Case(In2Sel.CONST_SI_HI):
-                    comb += Assert(pdecode2.e.imm_data.data ==
-                                   self.exts(dec.SI << 16, 32, 64))
-                with m.Case(In2Sel.CONST_LI):
-                    comb += Assert(pdecode2.e.imm_data.data == (dec.LI << 2))
-                with m.Case(In2Sel.CONST_BD):
-                    comb += Assert(pdecode2.e.imm_data.data == (dec.BD << 2))
-                with m.Case(In2Sel.CONST_DS):
-                    comb += Assert(pdecode2.e.imm_data.data == (dec.DS << 2))
-                with m.Case(In2Sel.CONST_M1):
-                    comb += Assert(pdecode2.e.imm_data.data == ~0)
-                with m.Case(In2Sel.CONST_SH):
-                    comb += Assert(pdecode2.e.imm_data.data == dec.sh)
-                with m.Case(In2Sel.CONST_SH32):
-                    comb += Assert(pdecode2.e.imm_data.data == dec.SH32)
-                with m.Case(In2Sel.CONST_XBI):
-                    comb += Assert(pdecode2.e.imm_data.data == dec.FormXB.XBI)
-                with m.Default():
-                    comb += Assert(0)
-
-    def exts(self, exts_data, width, fullwidth):
-        exts_data = exts_data[0:width]
-        topbit = exts_data[-1]
-        signbits = Repl(topbit, fullwidth-width)
-        return Cat(exts_data, signbits)
-
-    def test_in2_fields(self):
-        m = self.m
-        comb = self.comb
-        dec = m.submodules.pdecode2.dec
-
-        comb += Assert(dec.RB == self.instr_bits(16, 20))
-        comb += Assert(dec.UI == self.instr_bits(16, 31))
-        comb += Assert(dec.SI == self.instr_bits(16, 31))
-        comb += Assert(dec.LI == self.instr_bits(6, 29))
-        comb += Assert(dec.BD == self.instr_bits(16, 29))
-        comb += Assert(dec.DS == self.instr_bits(16, 29))
-        comb += Assert(dec.sh == Cat(self.instr_bits(16, 20),
-                                     self.instr_bits(30)))
-        comb += Assert(dec.SH32 == self.instr_bits(16, 20))
-
-    def test_in3(self):
-        m = self.m
-        comb = self.comb
-        pdecode2 = m.submodules.pdecode2
-        with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS):
-            comb += Assert(pdecode2.e.read_reg3.ok == 1)
-            comb += Assert(pdecode2.e.read_reg3.data == self.instr_bits(6, 10))
-
-    def test_out(self):
-        m = self.m
-        comb = self.comb
-        pdecode2 = m.submodules.pdecode2
-        sel = pdecode2.dec.op.out_sel
-        dec = pdecode2.dec
-        with m.If(sel == OutSel.SPR):
-            comb += Assert(pdecode2.e.write_spr.ok == 1)
-            comb += Assert(pdecode2.e.write_reg.ok == 0)
-        with m.Elif(sel == OutSel.NONE):
-            comb += Assert(pdecode2.e.write_spr.ok == 0)
-            comb += Assert(pdecode2.e.write_reg.ok == 0)
-        with m.Else():
-            comb += Assert(pdecode2.e.write_spr.ok == 0)
-            comb += Assert(pdecode2.e.write_reg.ok == 1)
-            data = pdecode2.e.write_reg.data
-            with m.If(sel == OutSel.RT):
-                comb += Assert(data == self.instr_bits(6, 10))
-            with m.If(sel == OutSel.RA):
-                comb += Assert(data == self.instr_bits(11, 15))
-
-    def test_rc(self):
-        m = self.m
-        comb = self.comb
-        pdecode2 = m.submodules.pdecode2
-        sel = pdecode2.dec.op.rc_sel
-        dec = pdecode2.dec
-        comb += Assert(pdecode2.e.rc.ok == 1)
-        with m.If(sel == RC.NONE):
-            comb += Assert(pdecode2.e.rc.data == 0)
-        with m.If(sel == RC.ONE):
-            comb += Assert(pdecode2.e.rc.data == 1)
-        with m.If(sel == RC.RC):
-            comb += Assert(pdecode2.e.rc.data == dec.Rc)
-            comb += Assert(pdecode2.e.oe.ok == 1)
-            comb += Assert(pdecode2.e.oe.data == dec.OE)
-
-    def test_single_bits(self):
-        m = self.m
-        comb = self.comb
-        pdecode2 = m.submodules.pdecode2
-        dec = pdecode2.dec
-        e = pdecode2.e
-        comb += Assert(e.invert_in == dec.op.inv_a)
-        comb += Assert(e.invert_out == dec.op.inv_out)
-        comb += Assert(e.input_carry == dec.op.cry_in)
-        comb += Assert(e.output_carry == dec.op.cry_out)
-        comb += Assert(e.is_32bit == dec.op.is_32b)
-        comb += Assert(e.is_signed == dec.op.sgn)
-        with m.If(dec.op.lk):
-            comb += Assert(e.lk == self.instr_bits(31))
-        comb += Assert(e.byte_reverse == dec.op.br)
-        comb += Assert(e.sign_extend == dec.op.sgn_ext)
-        comb += Assert(e.update == dec.op.upd)
-        comb += Assert(e.input_cr == dec.op.cr_in)
-        comb += Assert(e.output_cr == dec.op.cr_out)
-
-    def instr_bits(self, start, end=None):
-        if not end:
-            end = start
-        return self.instruction[::-1][start:end+1][::-1]
-
-
-class Decoder2TestCase(FHDLTestCase):
-    def test_decoder2(self):
-        module = Driver()
-        self.assertFormal(module, mode="bmc", depth=4)
-
-
-if __name__ == '__main__':
-    unittest.main()
diff --git a/src/openpower/decoder/formal/test_decoder.py b/src/openpower/decoder/formal/test_decoder.py
new file mode 100644 (file)
index 0000000..ae53efb
--- /dev/null
@@ -0,0 +1,128 @@
+from nmigen import Module, Signal, Elaboratable, Cat
+from nmigen.asserts import Assert, AnyConst, Assume
+from nmutil.formaltest import FHDLTestCase
+
+from openpower.decoder.power_decoder import create_pdecode, PowerOp
+from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
+                                     OutSel, RC, Form, Function,
+                                     LdstLen, CryIn,
+                                     MicrOp, get_csv)
+from openpower.decoder.power_decoder2 import (PowerDecode2,
+                                        Decode2ToExecute1Type)
+import unittest
+import pdb
+
+class Driver(Elaboratable):
+    def __init__(self):
+        self.instruction = Signal(32, reset_less=True)
+        self.m = None
+        self.comb = None
+
+    def elaborate(self, platform):
+        self.m = Module()
+        self.comb = self.m.d.comb
+        self.instruction = Signal(32)
+
+        self.comb += self.instruction.eq(AnyConst(32))
+
+        pdecode = create_pdecode()
+
+        self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
+        dec1 = pdecode2.dec
+        self.comb += pdecode2.dec.bigendian.eq(1) # TODO: bigendian=0
+        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
+
+        # ignore special decoding of nop
+        self.comb += Assume(self.instruction != 0x60000000)
+
+        #self.assert_dec1_decode(dec1, dec1.dec)
+
+        self.assert_form(dec1, pdecode2)
+        return self.m
+
+    def assert_dec1_decode(self, dec1, decoders):
+        if not isinstance(decoders, list):
+            decoders = [decoders]
+        for d in decoders:
+            print(d.pattern)
+            opcode_switch = Signal(d.bitsel[1] - d.bitsel[0])
+            self.comb += opcode_switch.eq(
+                self.instruction[d.bitsel[0]:d.bitsel[1]])
+            with self.m.Switch(opcode_switch):
+                self.handle_subdecoders(dec1, d)
+                for row in d.opcodes:
+                    opcode = row['opcode']
+                    if d.opint and '-' not in opcode:
+                        opcode = int(opcode, 0)
+                    if not row['unit']:
+                        continue
+                    with self.m.Case(opcode):
+                        self.comb += self.assert_dec1_signals(dec1, row)
+                with self.m.Default():
+                    self.comb += Assert(dec.op.internal_op ==
+                                        MicrOp.OP_ILLEGAL)
+                                        
+
+    def handle_subdecoders(self, dec1, decoders):
+        for dec in decoders.subdecoders:
+            if isinstance(dec, list):
+                pattern = dec[0].pattern
+            else:
+                pattern = dec.pattern
+            with self.m.Case(pattern):
+                self.assert_dec1_decode(dec1, dec)
+
+    def assert_dec1_signals(self, dec, row):
+        op = dec.op
+        return [Assert(op.function_unit == Function[row['unit']]),
+                Assert(op.internal_op == MicrOp[row['internal op']]),
+                Assert(op.in1_sel == In1Sel[row['in1']]),
+                Assert(op.in2_sel == In2Sel[row['in2']]),
+                Assert(op.in3_sel == In3Sel[row['in3']]),
+                Assert(op.out_sel == OutSel[row['out']]),
+                Assert(op.ldst_len == LdstLen[row['ldst len']]),
+                Assert(op.rc_sel == RC[row['rc']]),
+                Assert(op.cry_in == CryIn[row['cry in']]),
+                Assert(op.form == Form[row['form']]),
+                ]
+
+    # This is to assert that the decoder conforms to the table listed
+    # in PowerISA public spec v3.0B, Section 1.6, page 12
+    def assert_form(self, dec, dec2):
+        with self.m.Switch(dec.op.form):
+            with self.m.Case(Form.A):
+                self.comb += Assert(dec.op.in1_sel.matches(
+                    In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
+                self.comb += Assert(dec.op.in2_sel.matches(
+                    In2Sel.RB, In2Sel.NONE))
+                self.comb += Assert(dec.op.in3_sel.matches(
+                    In3Sel.RS, In3Sel.NONE))
+                self.comb += Assert(dec.op.out_sel.matches(
+                    OutSel.NONE, OutSel.RT))
+                # The table has fields for XO and Rc, but idk what they correspond to
+            with self.m.Case(Form.B):
+                pass
+            with self.m.Case(Form.D):
+                self.comb += Assert(dec.op.in1_sel.matches(
+                    In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
+                self.comb += Assert(dec.op.in2_sel.matches(
+                    In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
+                    In2Sel.CONST_SI_HI))
+                self.comb += Assert(dec.op.out_sel.matches(
+                    OutSel.NONE, OutSel.RT, OutSel.RA))
+            with self.m.Case(Form.I):
+                self.comb += Assert(dec.op.in2_sel.matches(
+                    In2Sel.CONST_LI))
+
+    def instr_bits(self, start, end=None):
+        if not end:
+            end = start
+        return self.instruction[::-1][start:end+1]
+
+class DecoderTestCase(FHDLTestCase):
+    def test_decoder(self):
+        module = Driver()
+        self.assertFormal(module, mode="bmc", depth=4)
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/src/openpower/decoder/formal/test_decoder2.py b/src/openpower/decoder/formal/test_decoder2.py
new file mode 100644 (file)
index 0000000..87f6919
--- /dev/null
@@ -0,0 +1,216 @@
+from nmigen import Module, Signal, Elaboratable, Cat, Repl
+from nmigen.asserts import Assert, AnyConst
+from nmutil.formaltest import FHDLTestCase
+
+from openpower.decoder.power_decoder import create_pdecode, PowerOp
+from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
+                                           OutSel, RC, Form,
+                                           MicrOp, SPRfull as SPR)
+from openpower.decoder.power_decoder2 import (PowerDecode2,
+                                              Decode2ToExecute1Type)
+import unittest
+
+
+class Driver(Elaboratable):
+    def __init__(self):
+        self.m = None
+        self.comb = None
+        self.instruction = None
+
+    def elaborate(self, platform):
+        self.m = Module()
+        self.comb = self.m.d.comb
+        self.instruction = Signal(32)
+
+        self.comb += self.instruction.eq(AnyConst(32))
+
+        pdecode = create_pdecode()
+
+        self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
+        self.comb += pdecode2.dec.bigendian.eq(1)  # XXX TODO: bigendian=0
+        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
+
+        self.test_in1(pdecode2, pdecode)
+        self.test_in2()
+        self.test_in2_fields()
+        self.test_in3()
+        self.test_out()
+        self.test_rc()
+        self.test_single_bits()
+
+        return self.m
+
+    def test_in1(self, pdecode2, pdecode):
+        m = self.m
+        comb = self.comb
+        ra = self.instr_bits(11, 15)
+        with m.If(pdecode.op.in1_sel == In1Sel.RA):
+            comb += Assert(pdecode2.e.read_reg1.data == ra)
+            comb += Assert(pdecode2.e.read_reg1.ok == 1)
+        with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
+            with m.If(ra == 0):
+                comb += Assert(pdecode2.e.read_reg1.ok == 0)
+            with m.Else():
+                comb += Assert(pdecode2.e.read_reg1.data == ra)
+                comb += Assert(pdecode2.e.read_reg1.ok == 1)
+                op = pdecode.op.internal_op
+        with m.If((op == MicrOp.OP_BC) |
+                  (op == MicrOp.OP_BCREG)):
+            with m.If(~self.instr_bits(8)):
+                comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
+                comb += Assert(pdecode2.e.read_spr1.ok == 1)
+        with m.If((op == MicrOp.OP_MFSPR) |
+                  (op == MicrOp.OP_MTSPR)):
+            comb += Assert(pdecode2.e.read_spr1.data ==
+                           self.instr_bits(11, 20))
+            comb += Assert(pdecode2.e.read_spr1.ok == 1)
+
+    def test_in2(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        dec = pdecode2.dec
+        with m.If(dec.op.in2_sel == In2Sel.RB):
+            comb += Assert(pdecode2.e.read_reg2.ok == 1)
+            comb += Assert(pdecode2.e.read_reg2.data == dec.RB)
+        with m.Elif(dec.op.in2_sel == In2Sel.NONE):
+            comb += Assert(pdecode2.e.imm_data.ok == 0)
+            comb += Assert(pdecode2.e.read_reg2.ok == 0)
+        with m.Elif(dec.op.in2_sel == In2Sel.SPR):
+            comb += Assert(pdecode2.e.imm_data.ok == 0)
+            comb += Assert(pdecode2.e.read_reg2.ok == 0)
+            comb += Assert(pdecode2.e.read_spr2.ok == 1)
+            with m.If(dec.fields.FormXL.XO[9]):
+                comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR)
+            with m.Else():
+                comb += Assert(pdecode2.e.read_spr2.data == SPR.LR)
+        with m.Else():
+            comb += Assert(pdecode2.e.imm_data.ok == 1)
+            with m.Switch(dec.op.in2_sel):
+                with m.Case(In2Sel.CONST_UI):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.UI)
+                with m.Case(In2Sel.CONST_SI):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   self.exts(dec.SI, 16, 64))
+                with m.Case(In2Sel.CONST_UI_HI):
+                    comb += Assert(pdecode2.e.imm_data.data == (dec.UI << 16))
+                with m.Case(In2Sel.CONST_SI_HI):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   self.exts(dec.SI << 16, 32, 64))
+                with m.Case(In2Sel.CONST_LI):
+                    comb += Assert(pdecode2.e.imm_data.data == (dec.LI << 2))
+                with m.Case(In2Sel.CONST_BD):
+                    comb += Assert(pdecode2.e.imm_data.data == (dec.BD << 2))
+                with m.Case(In2Sel.CONST_DS):
+                    comb += Assert(pdecode2.e.imm_data.data == (dec.DS << 2))
+                with m.Case(In2Sel.CONST_M1):
+                    comb += Assert(pdecode2.e.imm_data.data == ~0)
+                with m.Case(In2Sel.CONST_SH):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.sh)
+                with m.Case(In2Sel.CONST_SH32):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.SH32)
+                with m.Case(In2Sel.CONST_XBI):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.FormXB.XBI)
+                with m.Default():
+                    comb += Assert(0)
+
+    def exts(self, exts_data, width, fullwidth):
+        exts_data = exts_data[0:width]
+        topbit = exts_data[-1]
+        signbits = Repl(topbit, fullwidth-width)
+        return Cat(exts_data, signbits)
+
+    def test_in2_fields(self):
+        m = self.m
+        comb = self.comb
+        dec = m.submodules.pdecode2.dec
+
+        comb += Assert(dec.RB == self.instr_bits(16, 20))
+        comb += Assert(dec.UI == self.instr_bits(16, 31))
+        comb += Assert(dec.SI == self.instr_bits(16, 31))
+        comb += Assert(dec.LI == self.instr_bits(6, 29))
+        comb += Assert(dec.BD == self.instr_bits(16, 29))
+        comb += Assert(dec.DS == self.instr_bits(16, 29))
+        comb += Assert(dec.sh == Cat(self.instr_bits(16, 20),
+                                     self.instr_bits(30)))
+        comb += Assert(dec.SH32 == self.instr_bits(16, 20))
+
+    def test_in3(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS):
+            comb += Assert(pdecode2.e.read_reg3.ok == 1)
+            comb += Assert(pdecode2.e.read_reg3.data == self.instr_bits(6, 10))
+
+    def test_out(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        sel = pdecode2.dec.op.out_sel
+        dec = pdecode2.dec
+        with m.If(sel == OutSel.SPR):
+            comb += Assert(pdecode2.e.write_spr.ok == 1)
+            comb += Assert(pdecode2.e.write_reg.ok == 0)
+        with m.Elif(sel == OutSel.NONE):
+            comb += Assert(pdecode2.e.write_spr.ok == 0)
+            comb += Assert(pdecode2.e.write_reg.ok == 0)
+        with m.Else():
+            comb += Assert(pdecode2.e.write_spr.ok == 0)
+            comb += Assert(pdecode2.e.write_reg.ok == 1)
+            data = pdecode2.e.write_reg.data
+            with m.If(sel == OutSel.RT):
+                comb += Assert(data == self.instr_bits(6, 10))
+            with m.If(sel == OutSel.RA):
+                comb += Assert(data == self.instr_bits(11, 15))
+
+    def test_rc(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        sel = pdecode2.dec.op.rc_sel
+        dec = pdecode2.dec
+        comb += Assert(pdecode2.e.rc.ok == 1)
+        with m.If(sel == RC.NONE):
+            comb += Assert(pdecode2.e.rc.data == 0)
+        with m.If(sel == RC.ONE):
+            comb += Assert(pdecode2.e.rc.data == 1)
+        with m.If(sel == RC.RC):
+            comb += Assert(pdecode2.e.rc.data == dec.Rc)
+            comb += Assert(pdecode2.e.oe.ok == 1)
+            comb += Assert(pdecode2.e.oe.data == dec.OE)
+
+    def test_single_bits(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        dec = pdecode2.dec
+        e = pdecode2.e
+        comb += Assert(e.invert_in == dec.op.inv_a)
+        comb += Assert(e.invert_out == dec.op.inv_out)
+        comb += Assert(e.input_carry == dec.op.cry_in)
+        comb += Assert(e.output_carry == dec.op.cry_out)
+        comb += Assert(e.is_32bit == dec.op.is_32b)
+        comb += Assert(e.is_signed == dec.op.sgn)
+        with m.If(dec.op.lk):
+            comb += Assert(e.lk == self.instr_bits(31))
+        comb += Assert(e.byte_reverse == dec.op.br)
+        comb += Assert(e.sign_extend == dec.op.sgn_ext)
+        comb += Assert(e.update == dec.op.upd)
+        comb += Assert(e.input_cr == dec.op.cr_in)
+        comb += Assert(e.output_cr == dec.op.cr_out)
+
+    def instr_bits(self, start, end=None):
+        if not end:
+            end = start
+        return self.instruction[::-1][start:end+1][::-1]
+
+
+class Decoder2TestCase(FHDLTestCase):
+    def test_decoder2(self):
+        module = Driver()
+        self.assertFormal(module, mode="bmc", depth=4)
+
+
+if __name__ == '__main__':
+    unittest.main()