From f8a96863b7614421c22e1c4b4a336b37bcc79e4c Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sun, 24 May 2020 20:23:54 +0100 Subject: [PATCH] add OP_CMPB formal proof --- src/soc/fu/logical/formal/proof_main_stage.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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 -- 2.30.2