sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2020-02-24	Allow overloading of subrange builtins for non-bitvectors	Thomas Bauereiss

2019-05-17	Experiment with making vector and bitvector distinct types	Alasdair Armstrong
	Only change that should be needed for 99.9% of uses is to change vector('n, 'ord, bit) to bitvector('n, 'ord), and adding $ifndef FEATURE_BITVECTOR_TYPE type bitvector('n, dec) = vector('n, dec, bit) $endif for to support any Sail before this Currently I have all C, Typechecking, and SMT tests passing, as well as the RISC-V spec building OCaml and C completely unmodified.
2018-12-28	Merge branch 'sail2' into rmem_interpreter	Jon French

2018-11-20	Add full constraints for vector updates	Brian Campbell
	Also fix a test with an insufficient constraint
2018-11-19	Add missing constraints on bitvector_access, with regression test.Fixes #24.	Robert Norton

2018-10-24	Interpreter: don't silently use OCaml externs, only interpreter externs	Jon French
	(Adds 'interpreter' externs as appropriate.)
2018-06-25	Coq: automatic cast introduction	Brian Campbell

2018-06-22	Precise bitvector subrange functions for Coq.	Brian Campbell
	Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas.
2018-06-18	Separate bitvector access/update from generic vector access in std prelude	Brian Campbell
	(necessary for backends where they're different) Coq uint/sint and related fixes
2018-06-08	Fill in most Coq built-ins	Brian Campbell

2018-06-08	Add missing Coq builtin info to vector_inc	Brian Campbell

2018-05-25	Coq: fill in some built-ins	Brian Campbell
	vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general
2018-05-23	A couple of missing >= 0 constraints on vector handling functions	Brian Campbell

2018-04-05	Add generic prelude library that pulls in various basic sail	Alasdair Armstrong
	definitions from sail/lib.