From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Mon, 13 Jul 2020 13:21:44 +0000 (+0100)
Subject: add EXTSWSLI "pass" to formal shift_rot proof
X-Git-Tag: div_pipeline~62
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22363faf2502c1e87736cb3ecc9332f388b71d4a;p=soc.git

add EXTSWSLI "pass" to formal shift_rot proof
---

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 685b221f..6346950d 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -103,6 +103,8 @@ class Driver(Elaboratable):
                 pass
             with m.Case(MicrOp.OP_RLCL):
                 pass
+            with m.Case(MicrOp.OP_EXTSWSLI):
+                pass
             with m.Default():
                 comb += o_ok.eq(0)