sail-riscv.git - Unnamed repository; edit this file 'description' to name the repository.

Age	Commit message (Collapse)	Author	Files	Lines
2023-10-11	Implement menvcfg	Tim Hutt	1	-0/+1
	This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work. It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.
2023-05-31	Fix build for Coq 8.17	Michael Sammler	1	-1/+1

2023-05-31	Coq updates for Sail 0.15	Brian Campbell	1	-14/+0

2023-05-29	apply_headers: regenerate copyright headersupdate-copyright-headers	Philipp Tomsich	1	-1/+3

2022-08-09	Minimal updates for Coq proof assistant output	Brian Campbell	1	-2/+4

2021-07-29	Use headache to apply copyright header at request of Peter Sewell.	Robert Norton	1	-0/+68

2021-02-11	Make N extension configurable.	Prashanth Mundkur	1	-0/+1

2020-06-15	Remove obsolete Coq axiom	Brian Campbell	1	-2/+0

2020-06-15	Update handwritten Coq support files to match current Sail.	Brian Campbell	1	-5/+2

2020-01-22	Fix coq build.	Prashanth Mundkur	1	-0/+1

2020-01-17	Update handwritten Coq to use boolean predicates	Brian Campbell	1	-10/+12
	Matches recent changes to Sail
2019-08-13	Update barriers in Coq.	Brian Campbell	1	-11/+11

2019-04-25	Fix coq build.	Prashanth Mundkur	1	-19/+19

2019-04-10	Update Coq memory interfaces	Brian Campbell	1	-20/+27
	(requires recent changes to the Coq library)
2019-04-04	Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras file	Brian Campbell	1	-0/+3

2019-01-16	More reorg.	Prashanth Mundkur	1	-0/+145
	. move prover files into a single support directory . generated_models -> generated_definitions . reset vector -> c_emulator