From 6b9d6a743b69bb9370ef1ed06cd89d10114edcf4 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Thu, 28 May 2020 11:36:41 -0400 Subject: [PATCH] Add proof for OP_SETB --- libreriscv | 2 +- src/soc/fu/cr/formal/proof_main_stage.py | 23 +++++++++++++++++++---- 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/libreriscv b/libreriscv index 3eb2a0c1..8e2e9f9c 160000 --- a/libreriscv +++ b/libreriscv @@ -1 +1 @@ -Subproject commit 3eb2a0c15c9de78afe0252192b886ca4482c5243 +Subproject commit 8e2e9f9cff9001032b54ea26a49ece7e683f6cc6 diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py index ddf0089e..0bf37299 100644 --- a/src/soc/fu/cr/formal/proof_main_stage.py +++ b/src/soc/fu/cr/formal/proof_main_stage.py @@ -69,6 +69,11 @@ class Driver(Elaboratable): cr_input_arr = Array([full_cr_in[(7-i)*4:(7-i)*4+4] for i in range(8)]) cr_output_arr = Array([cr_o[(7-i)*4:(7-i)*4+4] for i in range(8)]) + bf = Signal(xl_fields.BF[0:-1].shape()) + bfa = Signal(xl_fields.BFA[0:-1].shape()) + comb += bf.eq(xl_fields.BF[0:-1]) + comb += bfa.eq(xl_fields.BFA[0:-1]) + with m.Switch(rec.insn_type): # CR_ISEL takes cr_a with m.Case(InternalOp.OP_ISEL): @@ -80,6 +85,7 @@ class Driver(Elaboratable): # into cr_a comb += dut.i.cr_a.eq(cr_input_arr[bc]) + # For OP_CROP, we need to input the corresponding CR # registers for BA, BB, and BT with m.Case(InternalOp.OP_CROP): @@ -109,10 +115,6 @@ class Driver(Elaboratable): # This does a similar thing to OP_CROP above, with # less inputs. The CR selection fields are already 3 # bits so there's no need to grab only the MSBs - bf = Signal(xl_fields.BF[0:-1].shape()) - bfa = Signal(xl_fields.BFA[0:-1].shape()) - comb += bf.eq(xl_fields.BF[0:-1]) - comb += bfa.eq(xl_fields.BFA[0:-1]) # set cr_a to the CR selected by BFA comb += dut.i.cr_a.eq(cr_input_arr[bfa]) @@ -125,6 +127,10 @@ class Driver(Elaboratable): with m.Else(): comb += cr_output_arr[i].eq(dut.o.cr.data) + # Set the input similar to OP_MCRF + with m.Case(InternalOp.OP_SETB): + comb += dut.i.cr_a.eq(cr_input_arr[bfa]) + # For the other two, they take the full CR as input, and # output a full CR. This handles that with m.Default(): @@ -229,6 +235,15 @@ class Driver(Elaboratable): comb += Assert(o == Mux(cr_bit, a, b)) comb += o_ok.eq(1) + with m.Case(InternalOp.OP_SETB): + with m.If(cr_arr[4*bfa]): + comb += Assert(o == ((1<<64)-1)) + with m.Elif(cr_arr[4*bfa+1]): + comb += Assert(o == 1) + with m.Else(): + comb += Assert(o == 0) + comb += o_ok.eq(1) + # check that data ok was only enabled when op actioned comb += Assert(dut.o.o.ok == o_ok) comb += Assert(dut.o.cr.ok == cr_o_ok) -- 2.30.2