sail - Formal specification language for ISAs

Age	Commit message (Expand)	Author
2018-11-09	RISC-V: add missed c.ebreak instruction	Prashanth Mundkur
2018-11-08	RISC-V: fix a typo-induced bug in updating the PTE.	Prashanth Mundkur
2018-11-07	RISC-V: fix assembly mappings for lr/sc.	Prashanth Mundkur
2018-11-07	Move inline forall in function definitions	Alasdair Armstrong
2018-11-07	RISC-V: add some consistency checks when run with spike.	Prashanth Mundkur
2018-10-23	RISC-V: use stderr for terminal output in OCaml backend.	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: Allow the C platform to get the DTB from a file, so that OS boot is p...	Prashanth Mundkur
2018-10-23	RISC-V: add cli option to dump the platform device-tree.	Prashanth Mundkur
2018-10-23	RISC-V: Add a platform knob to control mtval contents on illegal instruction ...	Prashanth Mundkur
2018-10-23	RISC-V: various fixes	Prashanth Mundkur
2018-10-23	RISC-V: fix: sstatus.SD depends on .XS and .FS.	Prashanth Mundkur
2018-10-23	RISC-V: adjust main loop for the non-spike case.	Prashanth Mundkur
2018-10-23	RISC-V: implement terminal output for C platform.	Prashanth Mundkur
2018-10-23	RISC-V: tick the clock in the C platform.	Prashanth Mundkur
2018-10-23	RISC-V: Add device tree blob into rom, currently only when linked against spike.	Prashanth Mundkur
2018-10-23	RISC-V: add default reset vector.	Prashanth Mundkur
2018-10-23	RISC-V: fix up platform bits for lr/sc.	Prashanth Mundkur
2018-10-23	RISC-V: set htif tohost port address using ELF symbol.	Prashanth Mundkur
2018-10-23	Fix typo in plat_ram_size	Alasdair Armstrong
2018-10-23	RISC-V: Add some debug logs for within_phys_mem.	Prashanth Mundkur
2018-10-23	RISC-V: Allow Spike linkage to be conditionally enabled.	Prashanth Mundkur
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	Re-implement space-related mapping functions in Sail rather than backends	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