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 43dab03f0eb6bcc996450b0db641e29b6dd1a927..9e6d17a2fa4ad7ec001c034ba3e6ef4e6420b5a2 100644 (file)
--- 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