From f0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 17 May 2019 16:34:00 +0100 Subject: SMT: Finish adding all memory builtins from lib/regfp.sail --- test/smt/mem_builtins.unsat.sail | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test/smt/mem_builtins.unsat.sail (limited to 'test') diff --git a/test/smt/mem_builtins.unsat.sail b/test/smt/mem_builtins.unsat.sail new file mode 100644 index 00000000..28e44658 --- /dev/null +++ b/test/smt/mem_builtins.unsat.sail @@ -0,0 +1,12 @@ +default Order dec + +$include +$include + +$property +function prop() -> bool = { + __barrier(Barrier_DSB); + let _ = __excl_res(); + __write_mem_ea(Write_exclusive_release, 32, 0xFFFF_FFFF, 8); + true +} -- cgit v1.2.3