SMT: Add property and counterexample directive

Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.

$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
  let c = capBitsToCapability(true, capbits);
  let (base, top) = getCapBounds(c);
  let e = unsigned(c.E);
  e >= 51 | base <= top
}

The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like

function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp

by rewriting to (conceptually)

function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
  if length(bv) > 100 then true else exp

The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.

1 files changed, 4 insertions, 3 deletions

diff --git a/test/smt/rv_add_1.unsat.sail b/test/smt/rv_add_1.unsat.sail
index d3b784e8..9621240d 100644
--- a/test/smt/rv_add_1.unsat.sail
+++ b/test/smt/rv_add_1.unsat.sail
@@ -143,13 +143,14 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
   let v = X(rs1);
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
     Some(instr) => {
       execute(instr);
-      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0)
+      X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0
     },
-    _ => true
+    _ => false
   }
 }