sail - Formal specification language for ISAs

Age	Commit message (Expand)	Author
2018-11-19	A few more constraint lemmas for aarch64	Brian Campbell
2018-11-16	Canonicalise functions types in val specs	Alasdair Armstrong
2018-11-16	Various bugfixes and a simple profiling feature for rewrites	Alasdair Armstrong
2018-11-13	Make pretty printer stricter with brace placement	Alasdair Armstrong
2018-11-12	Infer tuple l-expressions types if all components are inferrable	Alasdair Armstrong
2018-11-12	Make type checker smarter at inferring l-expressions	Alasdair Armstrong
2018-11-12	opam release	Robert Norton
2018-11-09	RISC-V: add missed c.ebreak instruction	Prashanth Mundkur
2018-11-09	Add test case for passing register references	Thomas Bauereiss
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-11-06	Fix bug with loop indices not being mapped to int64 in C	Alasdair Armstrong
2018-11-05	Ensure function quantifier is in scope when generating C return type	Alasdair Armstrong
2018-11-05	Add a regression test for issue #22	Alasdair Armstrong
2018-11-05	Ensure type-synonyms are handled correctly in register dependencies	Alasdair Armstrong
2018-11-05	Make sure undefined_type functions are generated before registers	Alasdair Armstrong
2018-11-02	Add code to analyse function return types	Alasdair Armstrong
2018-11-02	Coq: add more autocasts for different but equal kids	Brian Campbell
2018-11-01	Changes to enable analysing type errors in ASL parser	Alasdair Armstrong
2018-10-31	Add rewriting pass for not-patterns	Alasdair Armstrong
2018-10-31	Remove Parse_ast.Int, add unique locations	Alasdair Armstrong
2018-10-31	Rename Reporting_basic to Reporting	Alasdair Armstrong
2018-10-31	Improve error messages for unsolved function quantifiers	Alasdair Armstrong
2018-10-29	Pretty printer tweaks for ASL parser	Alasdair Armstrong
2018-10-29	Merge pull request #21 from rems-project/riscv_c_platform	Alasdair Armstrong
2018-10-24	Add constraint synonyms	Alasdair Armstrong
2018-10-23	RISC-V: switch c tests to use the C platform simulator; update .gitignore.	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	RTS: Add elf symbol lookup support.	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