index
:
sail
sail2
Formal specification language for ISAs
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test
/
smt
Age
Commit message (
Expand
)
Author
2019-05-29
SMT: Make bitvector equality work between vectors of different lengths
Alasdair Armstrong
2019-05-29
SMT: Fix sail_truncate and sail_mask for unusual argument types
Alasdair Armstrong
2019-05-28
SMT: Add min and max functions
Alasdair Armstrong
2019-05-21
SMT: Use a separate constructor for memory read variables
Alasdair Armstrong
2019-05-17
SMT: Finish adding all memory builtins from lib/regfp.sail
Alasdair Armstrong
2019-05-16
SMT: Improve simplification for generated SMT
Alasdair Armstrong
2019-05-10
SMT: Implement memory events for read_mem and write_mem
Alasdair
2019-05-10
SMT: Experiment with symbolic memory reads and writes
Alasdair Armstrong
2019-05-10
SMT: Fix error in get_pathcond
Alasdair Armstrong
2019-05-09
SMT: Make path conditionals more precise
Alasdair Armstrong
2019-05-08
SMT: Add test for various real number properties
Alasdair Armstrong
2019-05-08
SMT: Add reals and strings to SMT backend
Alasdair Armstrong
2019-04-30
SMT: Allow custom queries
Alasdair Armstrong
2019-04-30
SMT: Simplify and generalise checking events
Alasdair Armstrong
2019-04-29
SMT: Refactor overflow checks into generic event checking system
Alasdair Armstrong
2019-04-24
SMT: Make sure we clear overflow checks between generating properties
Alasdair Armstrong
2019-04-23
SMT: Add parser for generated models
Alasdair Armstrong
2019-04-20
SMT: Support writing to register references
Alasdair Armstrong
2019-04-17
SMT: Support register references
Alasdair Armstrong
2019-04-17
SMT: Support generic vectors and handle lets between specs and functions
Alasdair Armstrong
2019-04-17
SMT: Unroll simple foreach loops
Alasdair Armstrong
2019-04-16
SMT: Support toplevel letbindings
Alasdair Armstrong
2019-04-16
SMT: Fix inlining issues
Alasdair Armstrong
2019-04-13
SMT: Add count_leading_zeros and more builtins
Alasdair
2019-04-13
SMT: More builtins
Alasdair
2019-04-11
SMT: Add property and counterexample directive
Alasdair Armstrong
2019-04-11
SMT: Fixes for more cheri compressed cap properties
Alasdair
2019-04-10
SMT: More builtins and tests
Alasdair Armstrong
2019-04-09
SMT: Experimental Jib->SMT translation
Alasdair Armstrong