Add proof for power_decoder2.DecodeA

diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py
index e9e15cdda80939d542416aadd65ae65b2cd0bfeb..651dcbf7673ba1d9330cc76d9cc5ef2a5520f703 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder2.py
+++ b/src/soc/decoder/formal/proof_decoder2.py
@@ -3,7 +3,8 @@ from nmigen.asserts import Assert, AnyConst
 from nmigen.test.utils import FHDLTestCase
 
 from soc.decoder.power_decoder import create_pdecode, PowerOp
-from soc.decoder.power_enums import In1Sel, In2Sel, In3Sel
+from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
+                                     InternalOp, SPR)
 from soc.decoder.power_decoder2 import (PowerDecode2,
                                         Decode2ToExecute1Type)
 import unittest
@@ -28,8 +29,26 @@ class Driver(Elaboratable):
         return m
 
     def test_in1(self, m, pdecode2, pdecode):
+        ra = pdecode.RA[0:-1]
         with m.If(pdecode.op.in1_sel == In1Sel.RA):
+            m.d.comb += Assert(pdecode2.e.read_reg1.data == ra)
             m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1)
+        with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO):
+            with m.If(ra == 0):
+                m.d.comb += Assert(pdecode2.e.read_reg1.ok == 0)
+            with m.Else():
+                m.d.comb += Assert(pdecode2.e.read_reg1.data == ra)
+                m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1)
+        op = pdecode.op.internal_op
+        with m.If((op == InternalOp.OP_BC) |
+                  (op == InternalOp.OP_BCREG)):
+            with m.If(~pdecode.BO[2]):
+                m.d.comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR)
+                m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1)
+        with m.If((op == InternalOp.OP_MFSPR) |
+                  (op == InternalOp.OP_MTSPR)):
+            m.d.comb += Assert(pdecode2.e.read_spr1.data == pdecode.SPR[0:-1])
+            m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1)
 
 
 class Decoder2TestCase(FHDLTestCase):