From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 2 Sep 2022 12:32:45 +0000 (+0100)
Subject: add fix of out_sel in power_decoder.py formal proof
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c39e98213055bfcbebb0c55da65f2ba3edaa806d;p=openpower-isa.git

add fix of out_sel in power_decoder.py formal proof
but there are others.  basically the list of enums needs to be
automatically listed and put into the matches
---

diff --git a/src/openpower/decoder/formal/test_decoder.py b/src/openpower/decoder/formal/test_decoder.py
index f0053134..0236d93a 100644
--- a/src/openpower/decoder/formal/test_decoder.py
+++ b/src/openpower/decoder/formal/test_decoder.py
@@ -99,7 +99,7 @@ class Driver(Elaboratable):
                     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
+                # The table has fields for XO and Rc, what do they match to?
             with self.m.Case(Form.B):
                 pass
             with self.m.Case(Form.D):
@@ -109,7 +109,8 @@ class Driver(Elaboratable):
                     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))
+                    OutSel.NONE, OutSel.RT, OutSel.RA, OutSel.SPR,
+                    OutSel.RT_OR_ZERO, OutSel.FRT, OutSel.FRS))
             with self.m.Case(Form.I):
                 self.comb += Assert(dec.op.in2_sel.matches(
                     In2Sel.CONST_LI))
@@ -122,8 +123,11 @@ class Driver(Elaboratable):
 
 class DecoderTestCase(FHDLTestCase):
     @unittest.expectedFailure  # FIXME: proof failed:
-    # self.comb += Assert(dec.op.out_sel.matches(
-    #     OutSel.NONE, OutSel.RT, OutSel.RA))
+    # needs to have all the enum entries added, TODO there
+    # has to be an automated way to do that
+    # self.comb += Assert(dec.op.in2_sel.matches(
+    #    In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI,
+    #    In2Sel.CONST_SI_HI))
     def test_decoder(self):
         module = Driver()
         self.assertFormal(module, mode="bmc", depth=4)