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 90854c1d8eace4c310dbadab13ed9451cf09879c..5b871f5abc52269a9cd16aa1838fba0a0cdf9d31 100644 (file)
--- 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 f03196e4cdde251b6d9e0cd781204acff52f2c54..4d02df67a777829d17a6751c8b712d04f630587d 100644 (file)
--- 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