sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-06-11	More efficient bitfield implementation	Alasdair Armstrong

2018-06-11	Merge branch 'mappings' into sail2	Jon French

2018-06-11	actually fix exist_pattern test	Jon French

2018-06-11	fix test exist_pattern.sail -- lem needed much more of the stdlib to be imported	Jon French

2018-06-11	Merge branch 'sail2' into mappings	Jon French

2018-06-11	Add string.sail file to lib	Alasdair Armstrong

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	ocaml test prelude: option is now in stdlib	Jon French

2018-06-11	drop now-unnecessary type annotation clutter from riscv decode mappings	Jon French

2018-06-11	better type inference of union-constructors and 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-09	Fix issue in C_backend, and run C tests with undefined behavior sanitizer	Alasdair

2018-06-09	Fix issue with catch block return values not being compiled correctly	Alasdair
	This should fix the issue raised in commit 45554f Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
2018-06-08	Fix mmio address matching for clint device.	Prashanth Mundkur

2018-06-08	Add counteren registers.	Prashanth Mundkur

2018-06-08	Slightly condense execution trace log.	Prashanth Mundkur

2018-06-08	Update initialization of misa.	Prashanth Mundkur

2018-06-08	Make the simulation loop use the platform interface to detect exits via htif.	Prashanth Mundkur

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

2018-06-08	Fix use of non-tail-recursive calls in elf_loader.	Prashanth Mundkur

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

2018-06-08	Coq: some handling of existential types as function return types	Brian Campbell

2018-06-08	Coq: add destructuring of atom existentials in patterns	Brian Campbell
	Plus test case, broken builtin name
2018-06-08	Coq: track add_typquant change	Brian Campbell

2018-06-08	Correct dependencies of bytecode sail	Brian Campbell

2018-06-08	Coq: existential and constraint solving work	Brian Campbell
	- add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving
2018-06-08	Coq: some very basic existential support	Brian Campbell
	Only single variable in places, only packed at literals and variables, no unpacking
2018-06-08	Coq: fix axiom generation	Brian Campbell

2018-06-08	Coq: ignore some currently unsupported tests	Brian Campbell

2018-06-08	Coq: update foreach handling, correct field accesses	Brian Campbell

2018-06-08	Fill in most Coq built-ins	Brian Campbell

2018-06-08	Coq: skip two tests with redundant pattern matches	Brian Campbell

2018-06-08	Coq: correct failure on unsupported undefined values	Brian Campbell

2018-06-08	Coq: use record update syntax (only single fields work for now)	Brian Campbell

2018-06-08	Coq: correct implicitness of type arguments in unions	Brian Campbell

2018-06-08	Add missing Coq builtin info to vector_inc	Brian Campbell

2018-06-08	add sail as dependency of mips targets.	Robert Norton

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

2018-06-07	Fix width guards on htif accesses.	Prashanth Mundkur

2018-06-07	Update physical memory and address translation for MMIO.	Prashanth Mundkur
	- Assume for now that atomic accesses are only to memory regions, to leave their effects unchanged. - The top-level mem_read and mem_write functions for physical memory now have rreg and wreg effects due to MMIO (due to reads/writes to device registers). It would be nice to have a separate construct for non-CPU-register state to avoid polluting the footprint. - Assume for now that page-table walks access physical memory regions only, and not MMIO regions. Leave a fixme note there to address this later, perhaps when PMP/PMA is added.
2018-06-07	More definitions for the physical memory map.	Prashanth Mundkur

2018-06-07	Remove unused file.	Prashanth Mundkur

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

2018-06-07	Fix bug in add_bits optimization	Alasdair Armstrong

2018-06-07	Refactor mips main a little to work around apparent bug in c generation. ↵	Robert Norton
	Generated c Works with no gcc optimisation but fails when optimisation is on, implying undefined behaviour. Probably due to control reaching end of non-void function in exception case.
2018-06-07	Use the vector_dec standard library for mips. This means we get all the c ↵	Robert Norton
	functions ready to go.
2018-06-07	add mips_c target.	Robert Norton

2018-06-07	Rename some functions in vector_dec library file to avoid clashes with ↵	Robert Norton
	functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired.