From: Michael Nolan Date: Wed, 20 May 2020 14:01:29 +0000 (-0400) Subject: Add proof for OP_EXTS X-Git-Tag: div_pipeline~1040 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32d9da2bd849d3ae9b59bdec7a4add0c35908922;p=soc.git 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 33c97809..24e42e84 100644 --- 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