sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-08-16	Add the type an expression was checked against to tannots, and use for Coq	Brian Campbell
	Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast.
2018-08-15	Temporary fix for RISC-V Lem generation	Brian Campbell

2018-08-15	Get RISC-V on Coq into reasonable state to show	Brian Campbell
	- Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values
2018-08-13	More RISC-V built-in type constraints	Brian Campbell

2018-08-13	Coq: more strings for RISC-V	Brian Campbell

2018-08-13	Add constraints to RISC-V duopod, makefile rules	Brian Campbell

2018-08-13	RISC-V: mult_range is ill-typed, use mult_atom instead	Brian Campbell

2018-08-13	Basic Coq support for RISC-V	Brian Campbell
	Note that constraints have been added to ensure that all bitvector types are inhabited.
2018-07-27	Add some missing rv64i instructions, discovered when annotating the riscv ↵	Prashanth Mundkur
	isa spec.
2018-07-27	Add a riscv latex target.	Prashanth Mundkur

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-11	Fix riscv_duopod build.	Robert Norton

2018-07-10	Add an option to specify the dtc to use for the riscv platform.	Prashanth Mundkur

2018-07-10	Turn off some riscv debug tracing.	Prashanth Mundkur

2018-07-10	Start adding c-backend bits for riscv.	Prashanth Mundkur

2018-07-10	Support riscv atomic accesses to mmio regions, used by linux to access ↵	Prashanth Mundkur
	device registers.
2018-07-10	Make HOL build properly again for all of the models	Brian Campbell

2018-07-10	RISCV load-acquire in Lem (-> rmem)	Jon French

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

2018-07-10	disable printing when compiling to Lem to keep rmem happy	Jon French

2018-07-09	Log some timing info at the end of riscv execution.	Prashanth Mundkur

2018-07-09	add riscv_analysis.sail to SAIL_SRCS	Jon French

2018-07-09	add LOADRES, STORECON, AMO to analysis	Jon French

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

2018-07-08	Make the riscv fetch-execute loop return instead of exiting when done.	Prashanth Mundkur

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

2018-07-08	Add a riscv coverage target using bisect-ppx.	Prashanth Mundkur

2018-07-07	Add reservation traces to riscv tracecmp tool.	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-07	Add some tracing to riscv address translation.	Prashanth Mundkur

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	print to stdout not stderr to stop upsetting rmem regression tests	Jon French

2018-07-05	restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵	Jon French
	cleanly
2018-07-03	Add htif tohost to the riscv tracecmp tool.	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-28	further changes to support rmem	Jon French

2018-06-26	Fix duplicate riscv mem-ea, spotted by Jon French.	Prashanth Mundkur

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	Increment the riscv trace step counter only when instructions are executed.	Prashanth Mundkur

2018-06-25	Hook in the missed misa legalizer.	Prashanth Mundkur

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-25	Make sstatus.UXL legalization match spike for now. Leave a fixme to make ↵	Prashanth Mundkur
	this a platform setting.
2018-06-25	Fix a missed fixme for the sstatus view of mstatus.	Prashanth Mundkur

2018-06-25	Fix tracecmp for spike's recursive calls for sie/sip/sstatus csr writes.	Prashanth Mundkur