add links to bugreports into ALu formal proof as well

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 5b871f5abc52269a9cd16aa1838fba0a0cdf9d31..a6ce38028072ccbd2a4991f4086f66074560b580 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -1,5 +1,11 @@
-# Proof of correctness for partitioned equal signal combiner
+# Proof of correctness for ALU pipeline, main 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, Repl,
                     signed)

diff --git a/src/soc/fu/alu/formal/proof_output_stage.py b/src/soc/fu/alu/formal/proof_output_stage.py
index 4d02df67a777829d17a6751c8b712d04f630587d..d76a5e2743334b95a0e07315a8a93a05d543dbba 100644 (file)
--- a/src/soc/fu/alu/formal/proof_output_stage.py
+++ b/src/soc/fu/alu/formal/proof_output_stage.py
@@ -1,4 +1,4 @@
-# Proof of correctness for partitioned equal signal combiner, output stage
+# Proof of correctness for ALU pipeline, output stage
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 """
 Links: