From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 14:07:16 +0000 (-0400)
Subject: Add proof for OP_CMP and OP_CMPEQB
X-Git-Tag: div_pipeline~1039
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca79ab18a7fa9bdabeca860448d79b5d11dc222f;p=soc.git

Add proof for OP_CMP and OP_CMPEQB
---

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 24e42e84..c139cccb 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -81,6 +81,17 @@ class Driver(Elaboratable):
                     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)))
+            with m.Case(InternalOp.OP_CMP):
+                # CMP is defined as not taking in carry
+                comb += Assume(carry_in == 0)
+                comb += Assert(o == (a+b)[0:64])
+
+            with m.Case(InternalOp.OP_CMPEQB):
+                src1 = a[0:8]
+                eqs = Signal(8)
+                for i in range(8):
+                    comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
+                comb += Assert(dut.o.cr0[2] == eqs.any())
 
         return m