From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sun, 24 May 2020 19:23:54 +0000 (+0100)
Subject: add OP_CMPB formal proof
X-Git-Tag: div_pipeline~866
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f8a96863b7614421c22e1c4b4a336b37bcc79e4c;p=soc.git

add OP_CMPB formal proof
---

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 43dab03f..9e6d17a2 100644
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -143,8 +143,12 @@ class Driver(Elaboratable):
                         comb += Assert(o == peo64)
 
             with m.Case(InternalOp.OP_CMPB):
-                # TODO
-                pass
+                for i in range(8):
+                    slc = slice(i*8, (i+1)*8)
+                    with m.If(a[slc] == b[slc]):
+                        comb += Assert(o[slc] == 0xff)
+                    with m.Else():
+                        comb += Assert(o[slc] == 0)
 
             with m.Case(InternalOp.OP_BPERM):
                 # note that this is a copy of the beautifully-documented