From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 27 May 2020 14:15:14 +0000 (+0100)
Subject: test Data.ok for cr output and full cr output
X-Git-Tag: div_pipeline~797
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc106fcb4c8bbcccd7da8247cadc1ae71d594ae8;p=soc.git

test Data.ok for cr output and full cr output
---

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
index 26ebc79e..16295e90 100644
--- a/src/soc/fu/cr/formal/proof_main_stage.py
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -157,7 +157,7 @@ class Driver(Elaboratable):
                 for i in range(8):
                     with m.If(FXM[i]):
                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
-                comb += cr_o_ok.eq(1)
+                comb += full_cr_o_ok.eq(1)
 
             with m.Case(InternalOp.OP_MFCR):
                 with m.If(rec.insn[20]):  # mfocrf
@@ -214,6 +214,8 @@ class Driver(Elaboratable):
                 with m.If(lut == 0b0110):
                     comb += Assert(bit_o == bit_a ^ bit_b)
 
+                comb += cr_o_ok.eq(1)
+
             with m.Case(InternalOp.OP_ISEL):
                 # Extract the bit selector of the CR
                 bc = Signal(a_fields.BC[0:-1].shape(), reset_less=True)
@@ -229,6 +231,8 @@ class Driver(Elaboratable):
 
         # check that data ok was only enabled when op actioned
         comb += Assert(dut.o.o.ok == o_ok)
+        comb += Assert(dut.o.cr_o.ok == cr_o_ok)
+        comb += Assert(dut.o.full_cr.ok == full_cr_o_ok)
 
         return m