From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 27 May 2020 14:34:01 +0000 (+0100)
Subject: add links to bugreports into alu output stage proof
X-Git-Tag: div_pipeline~794
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf2c52cf3448d7c492a4510c4b45f5286e889f16;p=soc.git

add links to bugreports into alu output stage proof
---

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 90854c1d..5b871f5a 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -103,13 +103,14 @@ class Driver(Elaboratable):
                 eqs = Signal(8)
                 for i in range(8):
                     comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
-                comb += Assert(dut.o.cr0[2] == eqs.any())
+                comb += Assert(dut.o.cr0.data[2] == eqs.any())
 
             with m.Default():
                 comb += o_ok.eq(0)
 
         # check that data ok was only enabled when op actioned
         comb += Assert(dut.o.o.ok == o_ok)
+        #comb += Assert(dut.o.xer_ca.ok == o_ok)
 
         return m
 
diff --git a/src/soc/fu/alu/formal/proof_output_stage.py b/src/soc/fu/alu/formal/proof_output_stage.py
index f03196e4..4d02df67 100644
--- a/src/soc/fu/alu/formal/proof_output_stage.py
+++ b/src/soc/fu/alu/formal/proof_output_stage.py
@@ -1,5 +1,11 @@
-# Proof of correctness for partitioned equal signal combiner
+# Proof of correctness for partitioned equal signal combiner, output stage
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+"""
+Links:
+* https://bugs.libre-soc.org/show_bug.cgi?id=306
+* https://bugs.libre-soc.org/show_bug.cgi?id=305
+* https://bugs.libre-soc.org/show_bug.cgi?id=343
+"""
 
 from nmigen import Module, Signal, Elaboratable, Mux, Cat, signed
 from nmigen.asserts import Assert, AnyConst, Assume, Cover