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-29	RISC-V: no ldu for rv64i	Brian Campbell

2018-11-29	RISC-V: add some missing constraints on compressed instruction encodings	Brian Campbell

2018-11-29	RISC-V: add checks for misaligned targets to jumps and branches	Brian Campbell

2018-11-09	RISC-V: add missed c.ebreak instruction	Prashanth Mundkur

2018-11-07	RISC-V: fix assembly mappings for lr/sc.	Prashanth Mundkur

2018-10-23	RISC-V: separate jalr execute clause for seq model and rmem.	Prashanth Mundkur

2018-10-23	RISC-V: Initial splitting of instructions across multiple files.	Prashanth Mundkur

2018-10-23	RISC-V: various fixes	Prashanth Mundkur
	- add mstatus to cross-check - fix typo in assembly mapping for lr/sc
2018-10-05	RISC-V: encode/decode and assembly mappings for compressed instructions	Jon French

2018-08-28	fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bits	Jon French

2018-07-27	Add some missing rv64i instructions, discovered when annotating the riscv ↵	Prashanth Mundkur
	isa spec.
2018-07-20	Add assorted comments, consistency fixes and cleanup.	Prashanth Mundkur

2018-07-12	Fixed a nested comment issue	Shaked Flur

2018-07-11	Add fixme note about riscv jalr.	Prashanth Mundkur

2018-07-11	Update the exception code for riscv LR after clarification on isa-dev.	Prashanth Mundkur

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

2018-07-10	correct pretty-printing using mappings	Jon French

2018-07-09	Support writes to misa.C in riscv.	Prashanth Mundkur

2018-07-08	Move the riscv analysis function into its own file for coverage purposes.	Prashanth Mundkur

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

2018-07-07	An initial fix to riscv lr/sc, needs a review.	Prashanth Mundkur
	This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options.
2018-07-05	Fix printing of aq/rl flags in risc-v lr/sc.	Prashanth Mundkur

2018-07-05	support acquire/release loads/stores in RISCV initial_analysis	Jon French

2018-07-05	restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵	Jon French
	cleanly
2018-06-28	further changes to support rmem	Jon French

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	Hook in the missed misa legalizer.	Prashanth Mundkur

2018-06-25	Fix a missed fixme for the sstatus view of mstatus.	Prashanth Mundkur

2018-06-22	More trace log tweaks.	Prashanth Mundkur

2018-06-21	add PMP registers to CSR, fix build	Jon French

2018-06-21	changes to riscv model to support rmem	Jon French

2018-06-11	Update retire semantics for riscv WFI.	Prashanth Mundkur

2018-06-11	Merge branch 'sail2' into mappings	Jon French
	(involved some manual tinkering with gitignore, type_check, riscv)
2018-06-11	change double-caret for string-append-pattern to single caret, since that ↵	Jon French
	wouldn't be legal in a pattern anyway
2018-06-11	drop now-unnecessary type annotation clutter from riscv decode mappings	Jon French

2018-06-09	Increment minstret on instruction retires, and handle the case when the ↵	Prashanth Mundkur
	minstret CSR is explicitly written to.
2018-06-09	Some fixes to counteren handling.	Prashanth Mundkur

2018-06-08	Add counteren registers.	Prashanth Mundkur

2018-06-08	type checking mappings: allow inferring based on the other side's id inferences	Jon French

2018-05-23	riscv decode now uses mapping-decode and passes tests	Jon French

2018-05-21	further RISCV mapping: all extant non-compressed instructions done	Jon French

2018-05-18	more riscv mapping	Jon French

2018-05-18	more riscv mappings; riscv now builds successfully to lem which builds to ↵	Jon French
	isabelle (but isabelle almost certainly broken)
2018-05-15	Merge branch 'sail2' into mappings	Jon French

2018-05-15	Fix the ebreak instruction to trap, and remove the now obsolete internal ↵	Prashanth Mundkur
	exception. This should fix the sbreak test.
2018-05-11	...and actually working	Jon French

2018-05-11	further riscv mapping	Jon French