sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-11-30	Rename Undefined outcome to Choose	Thomas Bauereiss
	It is used for nondeterministic choice, so Undefined might be misleading.
2018-06-21	Follow Sail2 renaming in Isabelle library	Thomas Bauereiss

2018-04-18	Add first draft of Isabelle library documentation	Thomas Bauereiss

2018-02-26	Rename some Isabelle theories	Thomas Bauereiss
	The suffix _lemmas is more descriptive than _extras.
2018-02-26	Add/generate Isabelle lemmas about the monad lifting	Thomas Bauereiss
	Architecture-specific lemmas about concrete registers and types are generated and written to a file <prefix>_lemmas.thy, generic lemmas are in the theories *_extras.thy in lib/isabelle. In particular, State_extras contains simplification lemmas about the lifting from prompt to state monad.
2018-02-15	Rebase state monad onto prompt monad	Thomas Bauereiss
	Generate only one Lem model based on the prompt monad (instead of two models with different monads), and add a lifting from prompt to state monad. Add some Isabelle lemmas about the monad lifting. Also drop the "_embed" and "_sequential" suffixes from names of generated files.
2018-01-31	Add wrappers around Lem operators using bitvector type class	Thomas Bauereiss
	Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output.
2018-01-22	Update Lem shallow embedding to Sail2	Thomas Bauereiss
	- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
2017-09-29	Move Isabelle library	Thomas Bauereiss