SMT: Add count_leading_zeros and more builtins

5 files changed, 71 insertions, 3 deletions

diff --git a/test/smt/arith_FFL_2.unsat.sail b/test/smt/arith_FFL_2.unsat.sail
index 1b095e99..3535f1d1 100644
--- a/test/smt/arith_FFL_2.unsat.sail
+++ b/test/smt/arith_FFL_2.unsat.sail
@@ -3,7 +3,7 @@ default Order dec
 $include <prelude.sail>
 
 $option -smt_ignore_overflow
-$option -smt_int_size 256
+$option -smt_int_size 128
 
 $property
 function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> bool = {
@@ -14,8 +14,7 @@ function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int(
   };
 
   let mul_comm = x * y == y * x;
-  let mul_assoc = (x * y) * z == x * (y * z);
   let mul_zero = x * 0 == 0;
 
-  mul_comm & mul_assoc /* & mul_zero */
+  mul_comm & mul_zero
 }
diff --git a/test/smt/arith_FFL_5.unsat.sail b/test/smt/arith_FFL_5.unsat.sail
new file mode 100644
index 00000000..17dcfe86
--- /dev/null
+++ b/test/smt/arith_FFL_5.unsat.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+// CVC4 Really doesn't like it when this isn't 64
+$option -smt_int_size 64
+
+$property
+function prop forall 'n 'm, 0 <= 'n <= 128 & 0 <= 'm <= 64. (x: int('m), y: int('n), z: int) -> bool = {
+  let lo = -1000;
+  let hi = 1000;
+  if lo >= z | z >= hi then {
+    return(true)
+  };
+
+  let mul_assoc = (x * y) * z == x * (y * z);
+
+  mul_assoc
+}
diff --git a/test/smt/lzcnt.unsat.sail b/test/smt/lzcnt.unsat.sail
new file mode 100644
index 00000000..b627c9e5
--- /dev/null
+++ b/test/smt/lzcnt.unsat.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val lzcnt = "count_leading_zeros" : forall 'w. bits('w) -> range(0, 'w)
+
+$property
+function prop() -> bool = {
+  let p1 = lzcnt(0x0) == 4;
+  let p2 = lzcnt(0x00) == 8;
+  let p3 = lzcnt(0x02) == 6;
+  let p4 = lzcnt(0b01111111) == 1;
+  let p5 = lzcnt(0b1) == 0;
+  let p6 = lzcnt(0xF) == 0;
+  p1 & p2 & p3 & p4 & p5 & p6
+}
\ No newline at end of file
diff --git a/test/smt/lzcnt_2.unsat.sail b/test/smt/lzcnt_2.unsat.sail
new file mode 100644
index 00000000..b9f8249e
--- /dev/null
+++ b/test/smt/lzcnt_2.unsat.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val lzcnt = "count_leading_zeros" : forall 'w, 'w >= 1. bits('w) -> range(0, 'w)
+
+$property
+function prop() -> bool = {
+  let p1 = lzcnt(0b000) == 3;
+  let p2 = lzcnt(0x000) == 12;
+  let p3 = lzcnt(0x020) == 6;
+  let p4 = lzcnt(0b011111111) == 1;
+  let p5 = lzcnt(0b111) == 0;
+  let p6 = lzcnt(0b0 @ 0xF) == 1;
+  p1 & p2 & p3 & p4 & p5 & p6
+}
\ No newline at end of file
diff --git a/test/smt/lzcnt_3.unsat.sail b/test/smt/lzcnt_3.unsat.sail
new file mode 100644
index 00000000..b949a545
--- /dev/null
+++ b/test/smt/lzcnt_3.unsat.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <prelude.sail>
+
+val lzcnt = "count_leading_zeros" : forall 'w, 'w >= 1. bits('w) -> range(0, 'w)
+
+$property
+function prop(bv: bits(5)) -> bool = {
+  let x = unsigned(bv);
+  if x > 0 then {
+    let z = sail_zeros(x);
+    let p1 = lzcnt(z) == x;
+    let p2 = lzcnt(z @ 0xF) == x;
+    let p3 = lzcnt(0x0 @ z) == 4 + x;
+    p1 & p2
+  } else true
+}