sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-05-10	Merge branch 'sail2' into mappings	Jon French

2018-05-10	riscv/Makefile: add SAIL variable for easier debugging	Jon French

2018-05-09	remove redundant cloc targets.	Robert Norton

2018-05-09	Add targets for counting lines in mips, cheri and riscv. Can use either ↵	Robert Norton
	sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount.
2018-05-09	add SAIL_FLAGS env var to riscv makefile	Jon French

2018-05-03	Implement fetch to properly handle RVC and address translation, and add a ↵	Prashanth Mundkur
	step function for execution.
2018-04-23	Make riscv build depend on Makefile updates.	Prashanth Mundkur

2018-04-13	Move riscv memory definitions into a separate file.	Prashanth Mundkur

2018-03-21	Patch AST datatypes in generated Isabelle theories	Thomas Bauereiss
	Deactivate plugins of the datatype package except for the size plugin in order to keep processing time reasonable. This is currently only needed for the big AST datatypes, so we just patch this using a sed command.
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-02-01	Clean up riscv_duopod sail and add make targets for ocaml and Isabelle.	Robert Norton

2018-01-29	riscv: fix warnings about incomplete patterns. Add a check target in ↵	Robert Norton
	Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
2018-01-29	Added ecall/mret and exception support.	Prashanth Mundkur

2018-01-27	Add Makefile for RISC-V	Thomas Bauereiss