From 78e6e9f800a3dbfad854bf5a4afaf48307275960 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 16:33:02 -0400 Subject: [PATCH] Add proof for OP_MCRF --- src/soc/fu/cr/formal/proof_main_stage.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py index d109f81f..16223a45 100644 --- a/src/soc/fu/cr/formal/proof_main_stage.py +++ b/src/soc/fu/cr/formal/proof_main_stage.py @@ -78,6 +78,15 @@ class Driver(Elaboratable): comb += Assert(o[4*i:4*i+4] == 0) with m.Else(): # mfcrf comb += Assert(o == cr) + with m.Case(InternalOp.OP_MCRF): + BF = xl_fields.BF[0:-1] + BFA = xl_fields.BFA[0:-1] + for i in range(4): + comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i]) + for i in range(8): + with m.If(BF != 7-i): + comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4]) + with m.Case(InternalOp.OP_CROP): bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True) ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True) -- 2.30.2