sail - Formal specification language for ISAs

Age	Commit message (Expand)	Author
2018-10-23	RISC-V: flush logs at each step.	Prashanth Mundkur
2018-10-23	RISC-V: Flesh out more of the tandem checks in the C platform simulator.	Prashanth Mundkur
2018-10-23	RISC-V: An initial C Sail model linked against Spike for testing.	Prashanth Mundkur
2018-10-23	RISC-V: Refactor c platform bits.	Prashanth Mundkur
2018-10-22	Coq: use function type more carefully in untupling	Brian Campbell
2018-10-22	Update Coq patch for RISC-V, add string_take to Coq library	Brian Campbell
2018-10-16	Merge branch 'sail2' into rmem_interpreter	Jon French
2018-10-16	Re-implement space-related mapping functions in Sail rather than backends	Jon French
2018-10-15	Add interpreted RISC-V model to test suite	Jon French
2018-10-13	Adapt checked_mem_read to have acquire/release/reserve arguments so	Christopher Pulte
2018-10-05	RISC-V: encode/decode and assembly mappings for compressed instructions	Jon French
2018-10-01	Update Coq RISC-V patch now that the assembler is in good shape	Brian Campbell
2018-09-19	Coq: track changes elsewhere	Brian Campbell
2018-09-19	separate decimal_string_of_bits from string_of_bits	Jon French
2018-09-14	More monomorphisations for hex_bits_N...	Jon French
2018-09-14	RISCV prelude: fix typo in ocaml extern for negate_*	Jon French
2018-09-14	Sail_lib and RISCV prelude: functions for bitwise operations on ints	Jon French
2018-09-12	Coq: update RISC-V patch	Brian Campbell
2018-09-10	RISC-V: move the PC and minstret updates into the step function, to better lo...	Prashanth Mundkur
2018-09-07	RISCV: Run RISC-V tests using version compiled to C	Alasdair Armstrong
2018-09-06	Coq: fill in a few more RISC-V axioms	Brian Campbell
2018-09-06	Coq: fix up some barrier/memory definitions for RISC-V	Brian Campbell
2018-09-06	RISCV: Get enough of the RISCV platform into C to run some tests	Alasdair Armstrong
2018-09-05	Coq: fill in trivial ranges in constraint solver	Brian Campbell
2018-09-04	C: Tweaks to RISC-V to get compiling to C	Alasdair Armstrong
2018-09-04	Add a rewrite to minimise the number of functions marked as recursive	Brian Campbell
2018-09-03	Coq: solver should split earlier	Brian Campbell
2018-09-03	Coq: update RISC-V patch again	Brian Campbell
2018-09-03	Coq: rework generation of dependent pairs so that they are only	Brian Campbell
2018-08-31	Some C stubs for platform bits for RISC-V.	Prashanth Mundkur
2018-08-31	riscv prelude: yet more manual monomorphisations for hex_bits	Jon French
2018-08-30	Annotate the RISC-V prelude for C builtins.	Prashanth Mundkur
2018-08-30	Add a C header containing declarations needed by RISC-V.	Prashanth Mundkur
2018-08-29	C: Fix some issues with tuples as arguments to polymorphic constructors	Alasdair Armstrong
2018-08-29	Updated snapshots for Isabelle 2018	Thomas Bauereiss
2018-08-28	Adapt theory imports for Isabelle 2018	Thomas Bauereiss
2018-08-28	fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bits	Jon French
2018-08-16	Add the type an expression was checked against to tannots, and use for Coq	Brian Campbell
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
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
2018-07-27	Add some missing rv64i instructions, discovered when annotating the riscv isa...	Prashanth Mundkur
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