From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 22 May 2020 20:37:46 +0000 (+0100)
Subject: add TODO and link to SHIFT_ROT formal bugreport
X-Git-Tag: div_pipeline~926
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8867856c988478e2417f04f65954be0a9eec1e6;p=soc.git

add TODO and link to SHIFT_ROT formal bugreport
---

diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py
index 8ae7b629..6f03f1a6 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -1,5 +1,9 @@
 # Proof of correctness for partitioned equal signal combiner
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+"""
+Links:
+* https://bugs.libre-soc.org/show_bug.cgi?id=340
+"""
 
 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
                     signed)
@@ -86,6 +90,10 @@ class Driver(Elaboratable):
                         comb += Assert(o[32:64] == Repl(a[31], 32))
                     with m.Else():
                         comb += Assert(o == (a_signed >> b[0:7]))
+            #TODO 
+            #with m.Case(InternalOp.OP_RLC):
+            #with m.Case(InternalOp.OP_RLCR):
+            #with m.Case(InternalOp.OP_RLCL):
 
         return m