From 32d9da2bd849d3ae9b59bdec7a4add0c35908922 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 10:01:29 -0400 Subject: [PATCH] Add proof for OP_EXTS --- src/soc/fu/alu/formal/proof_main_stage.py | 5 +++++ 1 file changed, 5 insertions(+) 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 -- 2.30.2