Add cases for DecodeB and DecodeC

diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py
index ccdeda8f9bfcfdf957aa26796d9a6967082a71ab..53848be775bae71c8629df6223c4972cda1513e5 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder2.py
+++ b/src/soc/decoder/formal/proof_decoder2.py
@@ -27,6 +27,8 @@ class Driver(Elaboratable):
         self.comb += pdecode2.dec.opcode_in.eq(instruction)
 
         self.test_in1(pdecode2, pdecode)
+        self.test_in2()
+        self.test_in3()
 
         return self.m
 
@@ -55,6 +57,67 @@ class Driver(Elaboratable):
                            pdecode.SPR[0:-1])
             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[0:-1])
+        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.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[0:-1])
+                with m.Case(In2Sel.CONST_SI):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.SI[0:-1])
+                with m.Case(In2Sel.CONST_UI_HI):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   (dec.UI[0:-1] << 4))
+                with m.Case(In2Sel.CONST_SI_HI):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   (dec.SI[0:-1] << 4))
+                with m.Case(In2Sel.CONST_LI):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   (dec.LI[0:-1] << 2))
+                with m.Case(In2Sel.CONST_BD):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   (dec.BD[0:-1] << 2))
+                with m.Case(In2Sel.CONST_DS):
+                    comb += Assert(pdecode2.e.imm_data.data ==
+                                   (dec.DS[0:-1] << 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[0:-1])
+                with m.Case(In2Sel.CONST_SH32):
+                    comb += Assert(pdecode2.e.imm_data.data == dec.SH32[0:-1])
+                with m.Default():
+                    comb += Assert(0)
+
+    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 ==
+                           pdecode2.dec.RS[0:-1])
+
+
 class Decoder2TestCase(FHDLTestCase):
     def test_decoder2(self):
         module = Driver()