From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 2 Sep 2022 12:19:25 +0000 (+0100)
Subject: fix RCOE.RC_ONLY in formal test_decoder2.py
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87db26eba5a0791719a36826acb2c4bfd34a3f64;p=openpower-isa.git

fix RCOE.RC_ONLY in formal test_decoder2.py
---

diff --git a/src/openpower/decoder/formal/test_decoder2.py b/src/openpower/decoder/formal/test_decoder2.py
index d6686698..15e3538f 100644
--- a/src/openpower/decoder/formal/test_decoder2.py
+++ b/src/openpower/decoder/formal/test_decoder2.py
@@ -171,15 +171,21 @@ class Driver(Elaboratable):
         sel = pdecode2.dec.op.rc_sel
         dec = pdecode2.dec
         comb += Assert(pdecode2.e.rc.ok == 1)
+        # no RC: rc.data must be zero
         with m.If(sel == RCOE.NONE):
             comb += Assert(pdecode2.e.rc.data == 0)
+        # RC permanently set: rc.data must be hard-coded to 1
         with m.If(sel == RCOE.ONE):
             comb += Assert(pdecode2.e.rc.data == 1)
+        # RCOE.RC covers both RC and OE
         with m.If(sel == RCOE.RC):
             comb += Assert(pdecode2.e.rc.data == dec.Rc)
             comb += Assert(pdecode2.e.oe.ok == 1)
             comb += Assert(pdecode2.e.oe.data == dec.OE)
-        # FIXME(lkcl): handle other RCOE cases
+        # RCOE.RC_ONLY covers just RC: OE remains zero.
+        with m.If(sel == RCOE.RC_ONLY):
+            comb += Assert(pdecode2.e.rc.data == dec.Rc)
+            comb += Assert(pdecode2.e.oe.ok == 0)
 
     def test_single_bits(self):
         m = self.m