diff options
Diffstat (limited to 'test')
47 files changed, 153 insertions, 106 deletions
diff --git a/test/smt/basic_1.sat.sail b/test/smt/basic_1.sat.sail index d40c5a59..a4c79660 100644 --- a/test/smt/basic_1.sat.sail +++ b/test/smt/basic_1.sat.sail @@ -15,7 +15,8 @@ struct S = { register R1 : bits(16) register R2 : bits(8) -function check_sat(x: bool) -> bool = { +$property +function prop(x: bool) -> bool = { if x then { R1 = 0x007F } else { diff --git a/test/smt/basic_1.unsat.sail b/test/smt/basic_1.unsat.sail index cf469d75..9ce19539 100644 --- a/test/smt/basic_1.unsat.sail +++ b/test/smt/basic_1.unsat.sail @@ -15,11 +15,12 @@ struct S = { register R1 : bits(16) register R2 : bits(8) -function check_sat(x: bool) -> bool = { +$property +function prop(x: bool) -> bool = { if false then { R1 = 0x007F } else { R1 = 0xFFFF }; - R1 == sail_zero_extend(R2, 16) + not_bool(R1 == sail_zero_extend(R2, 16)) } diff --git a/test/smt/basic_2.sat.sail b/test/smt/basic_2.sat.sail index 73b18446..132c92ba 100644 --- a/test/smt/basic_2.sat.sail +++ b/test/smt/basic_2.sat.sail @@ -15,7 +15,8 @@ struct S = { register R1 : bits(16) register R2 : bits(8) -function check_sat(x: bool) -> bool = { +$property +function prop(x: bool) -> bool = { if x then { R1 = 0x00FF } else { diff --git a/test/smt/basic_2.unsat.sail b/test/smt/basic_2.unsat.sail index 1f3d8488..e87beec2 100644 --- a/test/smt/basic_2.unsat.sail +++ b/test/smt/basic_2.unsat.sail @@ -15,11 +15,12 @@ struct S = { register R1 : bits(16) register R2 : bits(8) -function check_sat(x: bool) -> bool = { +$property +function prop(x: bool) -> bool = { if x then { R1 = 0x01FF } else { R1 = 0xFFFF }; - R1 == sail_zero_extend(R2, 16) + R1 != sail_zero_extend(R2, 16) } diff --git a/test/smt/ccheri_regression1.unsat.sail b/test/smt/ccheri_regression1.unsat.sail index 808759cd..7b846a02 100644 --- a/test/smt/ccheri_regression1.unsat.sail +++ b/test/smt/ccheri_regression1.unsat.sail @@ -13,10 +13,11 @@ function operator <_u forall 'n, 'n >= 0. (x: bits('n), y: bits('n)) -> bool = overload ~ = {not_bool} -function check_sat() -> bool = { +$property +function prop() -> bool = { let i1 = 0b110 == truncate(shiftr(0x531E02A72708B000, 11), 3); let i2 = 0b000 == truncateLSB(0b00001010000011, 3); let i3 = 0b101 == sub_vec(0b110, 0b001); let i4 = false == operator <_u(0b110, 0b101); - ~(i1 & i2 & i3 & i4) + i1 & i2 & i3 & i4 }
\ No newline at end of file diff --git a/test/smt/concat_prop.unsat.sail b/test/smt/concat_prop.unsat.sail index 417152d5..857f7f33 100644 --- a/test/smt/concat_prop.unsat.sail +++ b/test/smt/concat_prop.unsat.sail @@ -5,7 +5,8 @@ $include <prelude.sail> register R1 : bits(32) register R2 : bits(32) -function check_sat('sz: range(0, 32)) -> bool = { +$property +function prop('sz: range(0, 32)) -> bool = { let z: bits('sz) = sail_zeros(sz); let x: bits('sz + 32) = R1 @ z; let y: bits(32 + 'sz) = R2 @ z; @@ -14,5 +15,5 @@ function check_sat('sz: range(0, 32)) -> bool = { // A and B must be equal let A = x @ y; let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y); - not_bool(A == B) + A == B } diff --git a/test/smt/concat_prop128.unsat.sail b/test/smt/concat_prop128.unsat.sail index 3d8ea45f..4205db10 100644 --- a/test/smt/concat_prop128.unsat.sail +++ b/test/smt/concat_prop128.unsat.sail @@ -5,7 +5,8 @@ $include <prelude.sail> register R1 : bits(64) register R2 : bits(64) -function check_sat('sz: range(0, 64)) -> bool = { +$property +function prop('sz: range(0, 64)) -> bool = { let z: bits('sz) = sail_zeros(sz); let x: bits('sz + 64) = R1 @ z; let y: bits(64 + 'sz) = R2 @ z; @@ -14,5 +15,5 @@ function check_sat('sz: range(0, 64)) -> bool = { // A and B must be equal let A = x @ y; let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y); - not_bool(A == B) + A == B } diff --git a/test/smt/exception.unsat.sail b/test/smt/exception.unsat.sail index e2455425..cd9f64d8 100644 --- a/test/smt/exception.unsat.sail +++ b/test/smt/exception.unsat.sail @@ -7,11 +7,12 @@ union exception = { E_unit : unit } -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { try { - throw(E_bool(false)) + throw(E_bool(true)) } catch { E_bool(b) => b, - E_unit() => true + E_unit() => false } } diff --git a/test/smt/exception_2.unsat.sail b/test/smt/exception_2.unsat.sail index 0a540341..795aa867 100644 --- a/test/smt/exception_2.unsat.sail +++ b/test/smt/exception_2.unsat.sail @@ -9,15 +9,16 @@ union exception = { register R : bool -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { try { if R then { - throw(E_bool(false)) + throw(E_bool(true)) } else { - false + true } } catch { E_bool(b) => b, - E_unit() => true + E_unit() => false } } diff --git a/test/smt/exception_3.unsat.sail b/test/smt/exception_3.unsat.sail index f0f71945..b0dd37db 100644 --- a/test/smt/exception_3.unsat.sail +++ b/test/smt/exception_3.unsat.sail @@ -9,16 +9,17 @@ union exception = { register R : bool -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { try { if R then { - throw(E_bool(false)) + throw(E_bool(true)) } else { - return(false); - true + return(true); + false } } catch { E_bool(b) => b, - E_unit() => true + E_unit() => false } } diff --git a/test/smt/lt_int_irrefl.unsat.sail b/test/smt/lt_int_irrefl.unsat.sail index 984793be..371208b4 100644 --- a/test/smt/lt_int_irrefl.unsat.sail +++ b/test/smt/lt_int_irrefl.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int) -> bool = { - x < x +$property +function prop(x: int) -> bool = { + not_bool(x < x) }
\ No newline at end of file diff --git a/test/smt/lt_int_trans.unsat.sail b/test/smt/lt_int_trans.unsat.sail index efd930b3..289839a7 100644 --- a/test/smt/lt_int_trans.unsat.sail +++ b/test/smt/lt_int_trans.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int, y: int, z: int) -> bool = { - if (x < y & y < z) then not_bool(x < z) else false +$property +function prop(x: int, y: int, z: int) -> bool = { + if (x < y & y < z) then x < z else true }
\ No newline at end of file diff --git a/test/smt/lteq_int_antisym.unsat.sail b/test/smt/lteq_int_antisym.unsat.sail index 1730f417..3c6dc028 100644 --- a/test/smt/lteq_int_antisym.unsat.sail +++ b/test/smt/lteq_int_antisym.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int, y: int) -> bool = { - if x <= y & y <= x then not_bool(x == y) else false +$property +function prop(x: int, y: int) -> bool = { + if x <= y & y <= x then x == y else true }
\ No newline at end of file diff --git a/test/smt/lteq_int_def.unsat.sail b/test/smt/lteq_int_def.unsat.sail index db3bf1f0..11859019 100644 --- a/test/smt/lteq_int_def.unsat.sail +++ b/test/smt/lteq_int_def.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int, y: int) -> bool = { - if x <= y then not_bool(x < y | x == y) else not_bool(y < x) +$property +function prop(x: int, y: int) -> bool = { + if x <= y then x < y | x == y else y < x }
\ No newline at end of file diff --git a/test/smt/lteq_int_refl.unsat.sail b/test/smt/lteq_int_refl.unsat.sail index eeb7e0d9..0417ae6e 100644 --- a/test/smt/lteq_int_refl.unsat.sail +++ b/test/smt/lteq_int_refl.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int) -> bool = { - not_bool(x <= x) +$property +function prop(x: int) -> bool = { + x <= x }
\ No newline at end of file diff --git a/test/smt/lteq_int_trans.unsat.sail b/test/smt/lteq_int_trans.unsat.sail index e7a8a3d7..d95ccb8e 100644 --- a/test/smt/lteq_int_trans.unsat.sail +++ b/test/smt/lteq_int_trans.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <prelude.sail> -function check_sat(x: int, y: int, z: int) -> bool = { - if (x <= y & y <= z) then not_bool(x <= z) else false +$property +function prop(x: int, y: int, z: int) -> bool = { + if (x <= y & y <= z) then x <= z else true }
\ No newline at end of file diff --git a/test/smt/order.unsat.sail b/test/smt/order.unsat.sail index c25762c9..0d96967f 100644 --- a/test/smt/order.unsat.sail +++ b/test/smt/order.unsat.sail @@ -4,7 +4,8 @@ $include <prelude.sail> overload ~ = {not_bool} -function check_sat(x: int, y: int, z: int) -> bool = { +$property +function prop(x: int, y: int, z: int) -> bool = { let lteq_refl = x <= x; let lteq_trans = (if x <= y & y <= z then x <= z else true); let lteq_antisym = (if x <= y & y <= x then x == y else true); @@ -26,7 +27,7 @@ function check_sat(x: int, y: int, z: int) -> bool = { let lt_negate = (if x > 0 then negate(x) < x else true); let gt_negate = (if x < 0 then negate(x) > x else true); - ~(lteq_refl & lteq_trans & lteq_antisym & lt_irrefl & lt_trans & lt_implies_lteq + lteq_refl & lteq_trans & lteq_antisym & lt_irrefl & lt_trans & lt_implies_lteq & gteq_refl & gteq_trans & gteq_antisym & gt_irrefl & gt_trans & gt_implies_gteq - & lt_negate & gt_negate) + & lt_negate & gt_negate } diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py index 097c0672..fb5a0ebd 100755 --- a/test/smt/run_tests.py +++ b/test/smt/run_tests.py @@ -19,10 +19,11 @@ def test_smt(name, solver, sail_opts): tests = {} for filename in filenames: basename = os.path.splitext(os.path.basename(filename))[0] + basename = basename.replace('.', '_') tests[filename] = os.fork() if tests[filename] == 0: step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename)) - step('{} {}.smt2 1> {}.out'.format(solver, basename, basename)) + step('{} {}_prop.smt2 1> {}.out'.format(solver, basename, basename)) if re.match('.+\.sat\.sail$', filename): step('grep -q ^sat$ {}.out'.format(basename)) else: diff --git a/test/smt/rv_add_0.sat.sail b/test/smt/rv_add_0.sat.sail index f1c86c4d..d0e8a5f5 100644 --- a/test/smt/rv_add_0.sat.sail +++ b/test/smt/rv_add_0.sat.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, v: xlenbits) -> bool = { +$property +function prop(imm: bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = { X(rs1) = v; 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 } } diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail index daa2996d..cddc5c7a 100644 --- a/test/smt/rv_add_0.unsat.sail +++ b/test/smt/rv_add_0.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, v: xlenbits) -> bool = { +$property +function prop(imm: bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = { X(rs1) = v; match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) { Some(instr) => { execute(instr); - not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0 | rs1 == 0) + X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0 | rs1 == 0 }, - _ => true + _ => false } } diff --git a/test/smt/rv_add_1.sat.sail b/test/smt/rv_add_1.sat.sail index b2a562c4..d9c1c127 100644 --- a/test/smt/rv_add_1.sat.sail +++ b/test/smt/rv_add_1.sat.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))) + X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) }, - _ => true + _ => false } } 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 } } diff --git a/test/smt/rv_add_decode.unsat.sail b/test/smt/rv_add_decode.unsat.sail index d5952e09..01653c6f 100644 --- a/test/smt/rv_add_decode.unsat.sail +++ b/test/smt/rv_add_decode.unsat.sail @@ -17,9 +17,10 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0 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 = { match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) { - Some(ITYPE(_)) => false, - _ => true + Some(ITYPE(_)) => true, + _ => false } }
\ No newline at end of file diff --git a/test/smt/rv_reg_rw.unsat.sail b/test/smt/rv_reg_rw.unsat.sail index 5bf419a9..485f45c7 100644 --- a/test/smt/rv_reg_rw.unsat.sail +++ b/test/smt/rv_reg_rw.unsat.sail @@ -128,7 +128,8 @@ scattered union ast union clause ast = ITYPE : (bits(12), regbits, regbits, iop) -function check_sat(r: regbits, v: xlenbits) -> bool = { +$property +function prop(r: regbits, v: xlenbits) -> bool = { X(r) = v; - not_bool(X(r) == v | r == 0) + X(r) == v | r == 0 } diff --git a/test/smt/shift_or_concat.unsat.sail b/test/smt/shift_or_concat.unsat.sail index 4e562889..1cb8f11a 100644 --- a/test/smt/shift_or_concat.unsat.sail +++ b/test/smt/shift_or_concat.unsat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(32) register R2 : bits(32) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 64); let x = sail_shiftleft(x, 32); let y = or_vec(x, sail_zero_extend(R2, 64)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shift_or_concat128.unsat.sail b/test/smt/shift_or_concat128.unsat.sail index 9cb0a0b8..36eab646 100644 --- a/test/smt/shift_or_concat128.unsat.sail +++ b/test/smt/shift_or_concat128.unsat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(128) register R2 : bits(128) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 256); let x = sail_shiftleft(x, 128); let y = or_vec(x, sail_zero_extend(R2, 256)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shift_or_concat4.unsat.sail b/test/smt/shift_or_concat4.unsat.sail index b8510151..7bc983f5 100644 --- a/test/smt/shift_or_concat4.unsat.sail +++ b/test/smt/shift_or_concat4.unsat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(4) register R2 : bits(4) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 8); let x = sail_shiftleft(x, 4); let y = or_vec(x, sail_zero_extend(R2, 8)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shift_or_concat4_2.unsat.sail b/test/smt/shift_or_concat4_2.unsat.sail index 2c730cbd..43a1b198 100644 --- a/test/smt/shift_or_concat4_2.unsat.sail +++ b/test/smt/shift_or_concat4_2.unsat.sail @@ -5,11 +5,12 @@ $include <prelude.sail> register R1 : bits(4) register R2 : bits(4) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let w = 4; let x = sail_zero_extend(R1, 8); let x = sail_shiftleft(x, w); let y = or_vec(x, sail_zero_extend(R2, 8)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shift_or_concat_1.sat.sail b/test/smt/shift_or_concat_1.sat.sail index 88107c50..505753b2 100644 --- a/test/smt/shift_or_concat_1.sat.sail +++ b/test/smt/shift_or_concat_1.sat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(32) register R2 : bits(32) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 64); let x = sail_shiftleft(x, 31); let y = or_vec(x, sail_zero_extend(R2, 64)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shift_or_concat_2.sat.sail b/test/smt/shift_or_concat_2.sat.sail index f7fd1f4c..8929834b 100644 --- a/test/smt/shift_or_concat_2.sat.sail +++ b/test/smt/shift_or_concat_2.sat.sail @@ -5,10 +5,11 @@ $include <prelude.sail> register R1 : bits(32) register R2 : bits(32) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_zero_extend(R1, 64); let x = sail_shiftleft(x, 33); let y = or_vec(x, sail_zero_extend(R2, 64)); let z = R1 @ R2; - not_bool(y == z) + y == z }
\ No newline at end of file diff --git a/test/smt/shiftr_zero_1.sat.sail b/test/smt/shiftr_zero_1.sat.sail index 9eb75c69..04dd74c4 100644 --- a/test/smt/shiftr_zero_1.sat.sail +++ b/test/smt/shiftr_zero_1.sat.sail @@ -4,7 +4,8 @@ $include <prelude.sail> register R : bits(64) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_shiftright(R, 63); - not_bool(x == 0x0000_0000_0000_0000) + x == 0x0000_0000_0000_0000 }
\ No newline at end of file diff --git a/test/smt/shiftr_zero_1.unsat.sail b/test/smt/shiftr_zero_1.unsat.sail index bcf60bb8..e43787d9 100644 --- a/test/smt/shiftr_zero_1.unsat.sail +++ b/test/smt/shiftr_zero_1.unsat.sail @@ -4,7 +4,8 @@ $include <prelude.sail> register R : bits(64) -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { let x = sail_shiftright(R, 64); - not_bool(x == 0x0000_0000_0000_0000) + x == 0x0000_0000_0000_0000 }
\ No newline at end of file diff --git a/test/smt/sign_extend.unsat.sail b/test/smt/sign_extend.unsat.sail index 835c2ce9..91f9d192 100644 --- a/test/smt/sign_extend.unsat.sail +++ b/test/smt/sign_extend.unsat.sail @@ -2,12 +2,13 @@ default Order dec $include <prelude.sail> -function check_sat(xs: bits(16)) -> bool = { +$property +function prop(xs: bits(16)) -> bool = { var p: bool = false; if xs[15] == bitzero then { p = 0x0000 @ xs == sail_sign_extend(xs, 32); } else { p = 0xFFFF @ xs == sail_sign_extend(xs, 32); }; - not_bool(p) + p }
\ No newline at end of file diff --git a/test/smt/sign_extend_2.unsat.sail b/test/smt/sign_extend_2.unsat.sail index 9c5b4437..75ec3836 100644 --- a/test/smt/sign_extend_2.unsat.sail +++ b/test/smt/sign_extend_2.unsat.sail @@ -2,12 +2,13 @@ default Order dec $include <prelude.sail> -function check_sat(xs: bits(16)) -> bool = { +$property +function prop(xs: bits(16)) -> bool = { var p: bool = true; if xs[15] == bitzero then { p = 0x0000 @ xs == sail_sign_extend(xs, 32); } else { p = 0xFFFF @ xs == sail_sign_extend(xs, 32); }; - not_bool(p) + p }
\ No newline at end of file diff --git a/test/smt/trivial.sat.sail b/test/smt/trivial.sat.sail index 8b8d67ce..0f802d54 100644 --- a/test/smt/trivial.sat.sail +++ b/test/smt/trivial.sat.sail @@ -2,6 +2,7 @@ default Order dec $include <flow.sail> -function check_sat((): unit) -> bool = { - true +$property +function prop((): unit) -> bool = { + false }
\ No newline at end of file diff --git a/test/smt/trivial.unsat.sail b/test/smt/trivial.unsat.sail index 2237a21f..a6c32ed1 100644 --- a/test/smt/trivial.unsat.sail +++ b/test/smt/trivial.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <flow.sail> -function check_sat((): unit) -> bool = { - false +$property +function prop((): unit) -> bool = { + true }
\ No newline at end of file diff --git a/test/smt/trivial_funcall.sat.sail b/test/smt/trivial_funcall.sat.sail index 48166c12..09fa5381 100644 --- a/test/smt/trivial_funcall.sat.sail +++ b/test/smt/trivial_funcall.sat.sail @@ -2,8 +2,9 @@ default Order dec $include <flow.sail> -function f((): unit) -> bool = true +function f((): unit) -> bool = false -function check_sat((): unit) -> bool = { +$property +function prop((): unit) -> bool = { f() }
\ No newline at end of file diff --git a/test/smt/trivial_return.sat.sail b/test/smt/trivial_return.sat.sail index 4cfd709a..180606cd 100644 --- a/test/smt/trivial_return.sat.sail +++ b/test/smt/trivial_return.sat.sail @@ -2,7 +2,8 @@ default Order dec $include <flow.sail> -function check_sat((): unit) -> bool = { - return true; - false +$property +function prop((): unit) -> bool = { + return false; + true }
\ No newline at end of file diff --git a/test/smt/trivial_return.unsat.sail b/test/smt/trivial_return.unsat.sail index 261955a4..507e3116 100644 --- a/test/smt/trivial_return.unsat.sail +++ b/test/smt/trivial_return.unsat.sail @@ -2,7 +2,8 @@ default Order dec $include <flow.sail> -function check_sat((): unit) -> bool = { - return false; - return true +$property +function prop((): unit) -> bool = { + return true; + return false }
\ No newline at end of file diff --git a/test/smt/update_access.unsat.sail b/test/smt/update_access.unsat.sail index 26411ff0..38a25d99 100644 --- a/test/smt/update_access.unsat.sail +++ b/test/smt/update_access.unsat.sail @@ -2,11 +2,12 @@ default Order dec $include <vector_dec.sail> -function check_sat(xs: bits(65), x: bit) -> bool = { +$property +function prop(xs: bits(65), x: bit) -> bool = { ys = xs; ys[63] = x; ys[64] = x; ys[42] = x; ys[0] = x; - not_bool(ys[64] == x & ys[63] == x & ys[42] == x & ys[0] == x) + ys[64] == x & ys[63] == x & ys[42] == x & ys[0] == x }
\ No newline at end of file diff --git a/test/smt/zeros_1.sat.sail b/test/smt/zeros_1.sat.sail index 4a813dcc..476b5ba4 100644 --- a/test/smt/zeros_1.sat.sail +++ b/test/smt/zeros_1.sat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x00 == sail_zeros(8) +$property +function prop((): unit) -> bool = { + 0x00 != sail_zeros(8) }
\ No newline at end of file diff --git a/test/smt/zeros_1.unsat.sail b/test/smt/zeros_1.unsat.sail index ade7cd23..02499efe 100644 --- a/test/smt/zeros_1.unsat.sail +++ b/test/smt/zeros_1.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x1 == sail_zeros(4) -}
\ No newline at end of file +$property +function prop((): unit) -> bool = { + 0x1 != sail_zeros(4) +} diff --git a/test/smt/zeros_2.sat.sail b/test/smt/zeros_2.sat.sail index 5cea2e99..1d61c9a2 100644 --- a/test/smt/zeros_2.sat.sail +++ b/test/smt/zeros_2.sat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x0000_0000_0000_0000 == sail_zeros(64) +$property +function prop((): unit) -> bool = { + 0x0000_0000_0000_0000 != sail_zeros(64) }
\ No newline at end of file diff --git a/test/smt/zeros_2.unsat.sail b/test/smt/zeros_2.unsat.sail index 855c46b4..0d5aad20 100644 --- a/test/smt/zeros_2.unsat.sail +++ b/test/smt/zeros_2.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0b1 == sail_zeros(1) +$property +function prop((): unit) -> bool = { + 0b1 != sail_zeros(1) }
\ No newline at end of file diff --git a/test/smt/zeros_3.sat.sail b/test/smt/zeros_3.sat.sail index 3da36e1f..243ceac2 100644 --- a/test/smt/zeros_3.sat.sail +++ b/test/smt/zeros_3.sat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x0000_0000_0000_0000_0 == sail_zeros(68) +$property +function prop((): unit) -> bool = { + not_bool(0x0000_0000_0000_0000_0 == sail_zeros(68)) }
\ No newline at end of file diff --git a/test/smt/zeros_3.unsat.sail b/test/smt/zeros_3.unsat.sail index 145ab386..0c271660 100644 --- a/test/smt/zeros_3.unsat.sail +++ b/test/smt/zeros_3.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x0000_0000_0000_0000_1 == sail_zeros(68) +$property +function prop((): unit) -> bool = { + 0x0000_0000_0000_0000_1 != sail_zeros(68) }
\ No newline at end of file diff --git a/test/smt/zeros_4.unsat.sail b/test/smt/zeros_4.unsat.sail index 416430fc..c02e034d 100644 --- a/test/smt/zeros_4.unsat.sail +++ b/test/smt/zeros_4.unsat.sail @@ -2,6 +2,7 @@ default Order dec $include <vector_dec.sail> -function check_sat((): unit) -> bool = { - 0x1000_0000_0000_0000_0 == sail_zeros(68) +$property +function prop((): unit) -> bool = { + 0x1000_0000_0000_0000_0 != sail_zeros(68) }
\ No newline at end of file |