From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 9 Mar 2020 15:14:38 +0000 (-0400)
Subject: Add proof for power_decoder2.DecodeA
X-Git-Tag: div_pipeline~1733
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17823579d39a7ea9082e69b646facfd08b1b9717;p=soc.git

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 e9e15cdd..651dcbf7 100644
--- 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):