Add proof for OP_EXTS

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 33c97809ff074c9bd674043da05807b97137b302..24e42e846b2105892825706adbccfec45bf75802 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -76,6 +76,11 @@ class Driver(Elaboratable):
                 # CA32
                 comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
                                == carry_out32)
+            with m.Case(InternalOp.OP_EXTS):
+                for i in [1, 2, 4]:
+                    with m.If(rec.data_len == i):
+                        comb += Assert(o[0:i*8] == a[0:i*8])
+                        comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
 
         return m