chore: add new test for match_bv

test/lean/match_bv.expected.lean

@@ -0,0 +1,23 @@
+import Out.Sail.Sail
+
+import Out.Sail.BitVec
+
+open Sail
+
+abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
+
+def decode (merge_var : (BitVec 32)) : Bool :=
+  match_bv merge_var with
+  | [11,111,0,00,opc:2,1,Rm:5,option_v:3,S,10,Rn:5,Rt:5] => if (Eq Rm Rn)
+  then true
+  else false
+  | [sf,10,01010,shift:2,N,Rm:5,imm6:6,Rn:5,Rd:5] => if (Eq Rn Rd)
+  then true
+  else false
+  | [1101010100,0,00,011,0011,CRm:4,1,01,11111] => true
+  | [1,011010,0,imm19:19,Rt:5] => false
+  | _ => true
+
+def initialize_registers (lit : Unit) : Unit :=
+  ()
+

test/lean/match_bv.sail

@@ -0,0 +1,29 @@
+default Order dec
+
+$include <prelude.sail>
+
+val decode : bits(32) -> bool
+
+function clause decode (0b11@0b111@0b0@0b00@(opc:bits(2))@0b1@(Rm:bits(5))@(option_v:bits(3))@[S]@0b10@(Rn:bits(5))@(Rt:bits(5))) = {
+  if Rm==Rn then
+    true
+  else
+    false 
+}
+
+function clause decode ([sf]@0b10@0b01010@(shift:bits(2))@[N]@(Rm:bits(5))@(imm6:bits(6))@(Rn:bits(5))@(Rd:bits(5))) = {
+  if Rn==Rd then
+    true
+  else
+    false  
+}
+
+function clause decode (0b1101010100@0b0@0b00@0b011@0b0011@(CRm : bits(4))@0b1@0b01@0b11111) = {
+  true
+}
+
+function clause decode (0b1@0b011010@0b0@(imm19:bits(19))@(Rt:bits(5))) = {
+  false
+}
+
+function clause decode(_) = { true }