sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-12-20	RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ↵	Robert Norton
	and tests.
2018-11-29	RISC-V: implement WFI in the platform model.	Prashanth Mundkur
	The initial implementation tries to optimize for simulator execution, especially for OS boots.
2018-11-29	RISC-V: factor the execution trace.	Prashanth Mundkur
	This is now split into instructions, regs, memory and platform, each controlled individually. Currently all are enabled and not connected to any command-line options, so a recompile is needed for trace tuning.
2018-11-07	Move inline forall in function definitions	Alasdair Armstrong
	* Previously we allowed the following bizarre syntax for a forall quantifier on a function: val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit this commit changes this to the more sane: val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit Having talked about it today, we could consider adding the syntax val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit which would avoid the forall (by implicitly quantifying variables in the constraint), and be slightly more friendly especially for documentation purposes. Only RISC-V used this syntax, so all uses of it there have been switched to the new style. * Second, there is a new (somewhat experimental) syntax for existentials, that is hopefully more readable and closer to minisail: val foo(x: int, y: int) -> int('m) with 'm >= 2 "type('n) with constraint" is equivalent to minisail: {'n: type \| constraint} the type variables in typ are implicitly quantified, so this is equivalent to {'n, constraint. typ('n)} In order to make this syntax non-ambiguous we have to use == in constraints rather than =, but this is a good thing anyway because the previous situation where = was type level equality and == term level equality was confusing. Now all the type type-level and term-level operators can be consistent. However, to avoid breaking anything = is still allowed in non-with constraints, and produces a deprecated warning when parsed.
2018-10-23	RISC-V: Add a platform knob to control mtval contents on illegal instruction ↵	Prashanth Mundkur
	faults.
2018-10-23	RISC-V: Add some debug logs for within_phys_mem.	Prashanth Mundkur

2018-08-31	Some C stubs for platform bits for RISC-V.	Prashanth Mundkur

2018-08-15	Temporary fix for RISC-V Lem generation	Brian Campbell

2018-08-13	More RISC-V built-in type constraints	Brian Campbell

2018-07-20	Add assorted comments, consistency fixes and cleanup.	Prashanth Mundkur

2018-07-11	RISC-V model fixes for RMEM	Jon French

2018-07-07	Cancel riscv reservation before i/o scheduling, tweak reservation tracing.	Prashanth Mundkur

2018-07-03	Allow the riscv htif_tohost mmio port to be readable, and ack writes to that ↵	Prashanth Mundkur
	port.
2018-06-25	Add a riscv platform parameter to control trapping to M-mode on misaligned ↵	Prashanth Mundkur
	access, and a cli option to control it.
2018-06-25	Fix riscv interrupt pending check to handle implicit enabling at lower ↵	Prashanth Mundkur
	privileges. Also fix timer threshold comparison to be <= instead of <.
2018-06-23	Fix a missing check for interrupt dispatch when riscv clint registers are ↵	Prashanth Mundkur
	written.
2018-06-22	Make riscv pte dirty-bit update handling configurable via a platform cli option.	Prashanth Mundkur
	Fix a redundant clock tick.
2018-06-19	Add more detail to riscv execution trace log.	Prashanth Mundkur

2018-06-11	Use riscv platform insns_per_tick to tick the clock.	Prashanth Mundkur

2018-06-08	Fix mmio address matching for clint device.	Prashanth Mundkur

2018-06-08	Add mem and mmio access tracing.	Prashanth Mundkur

2018-06-07	Slight refactor to keep platform handling localized to the _platform file.	Prashanth Mundkur

2018-06-07	More definitions for the physical memory map.	Prashanth Mundkur

2018-06-07	Add terminal output to riscv platform, with incomplete handling of input.	Prashanth Mundkur

2018-06-07	Fix Lem build of RISC-V	Thomas Bauereiss

2018-06-04	Add the htif exit command, a top-level function to initialize the riscv ↵	Prashanth Mundkur
	platform, and document the artificial wreg effect due to using registers for device state.
2018-06-04	Uncomment the clint implementation in riscv_platform.	Prashanth Mundkur

2018-05-22	Fix for E_cons not being compiled correctly into OCaml	Alasdair Armstrong

2018-05-22	Fix Lem build for RISC-V	Thomas Bauereiss

2018-05-21	Add the missed _tags file, and fix a typo.	Prashanth Mundkur

2018-05-21	Add in the platform files and update the ocaml build. Disable the isabelle ↵	Prashanth Mundkur
	build until we add suitable platform definitions/stubs. The platform bits are not yet hooked into the model, but only into the build, so are untested.