From: Michael Nolan <mtnolan2640@gmail.com>
Date: Thu, 28 May 2020 15:36:41 +0000 (-0400)
Subject: Add proof for OP_SETB
X-Git-Tag: div_pipeline~763
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b9d6a743b69bb9370ef1ed06cd89d10114edcf4;p=soc.git

Add proof for OP_SETB
---

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)