sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-01-28	mips.sail: fix infamous lwr and ldr (now pass tests).	Robert Norton

2016-01-28	mips.sail: fix back-to-front operands of DSLLV.	Robert Norton

2016-01-28	mips.sail: fix incorrect decode of DSLLV	Robert Norton

2016-01-28	mips.sail: split store cases by word width as sail needs to know which bit ↵	Robert Norton
	of word to store (probably a bug that it does not complain at runtime).
2016-01-28	Support exit and assert better in sequential interpreter and general ↵	Kathy Gray
	interpreter interface
2016-01-27	Add --max_instruction to sequential interpreter to permit an upper bound on ↵	Kathy Gray
	instructions run
2016-01-27	Add ability to run to a particular instruction execution number	Kathy Gray
	Could later add the ability to run to a particular instruction form (like we had in ppcmem2) or address
2016-01-27	mips.sail: branches are relative to delay slot PC, not branch! Support ↵	Robert Norton
	config registers in mfc0.
2016-01-27	mips.sail: produce undefined result for division by zero instead of crashing.	Robert Norton

2016-01-27	actually commit the new mips file	Kathy Gray

2016-01-27	Make mips build again	Kathy Gray
	Make quiet mode for sequential interpreter not print
2016-01-27	Fix issue where constraint solver wasn't rewriting enough equality ↵	Kathy Gray
	constraints and thus causing inequality checks to be missed
2016-01-27	start adding breakpoint	Kathy Gray

2016-01-27	mips.sail: further support for CP0 registers needed to run tests.	Robert Norton

2016-01-26	Stop turning all decreasing vectors into indexed ones : i.e. let's print ↵	Kathy Gray
	them sensibly at last
2016-01-26	mips.sail: beginning of mfc0 implementation.	Robert Norton

2016-01-26	mips.sail: fix bugs in DSRL32 and DSRLV	Robert Norton

2016-01-26	fix starting indices for mips initial register values.	Robert Norton

2016-01-26	mips.sail: work around sail bug in equality comparing bit vector to integer	Robert Norton

2016-01-26	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

2016-01-26	mips.sail: 32-bit load linked should sign extend result.	Robert Norton

2016-01-26	mips: fix encoding of DSRAV.	Robert Norton

2016-01-26	tweak to dependencies to hopefully reduce need to rebuild mips.sail.	Robert Norton

2016-01-26	Add example of test which dies whilst trying to throw exception.	Robert Norton

2016-01-26	print reg dump in correct format for cheri test suite. Reinstate timing of ↵	Robert Norton
	execution.
2016-01-26	Fix problem in run_with_model where we forgot that ppcmem2 treats everything ↵	Kathy Gray
	as increasing, and updated ranges accordingly, and mistakenly were using the wrong range values for register slicing.
2016-01-26	move closer to power.sail -> power.ml output	Kathy Gray

2016-01-26	add example of mips test which fails with first instruction (jal)	Robert Norton

2016-01-26	dump registers in format expected by cheri test suite when halting. Remove ↵	Robert Norton
	distinction between prog_mem and data_mem at least for now as data_mem was not being populated correctly (wrong elf flags?).
2016-01-25	mips.sail: modify overflow check to do exactly what is described in the ↵	Robert Norton
	spec. as the overflow flag provided by +_s builtin doesn't seem to do what we want.
2016-01-22	mips: revert accidental removal of overflow check from daddi. It is broken ↵	Robert Norton
	but this is not the fix...
2016-01-22	mips: fix PC update logic so branches might work.	Robert Norton

2016-01-22	add some test elf files for mips (pinched from cheri test suite).	Robert Norton

2016-01-21	mips.sail: fix alignment check for memory accesses.	Robert Norton

2016-01-21	add another encoding for HCF instruction and add execute clause -> first ↵	Robert Norton
	complete execution of test mips program!
2016-01-21	Start splitting values/etc into int/big_int for ocaml generation	Kathy Gray

2016-01-21	build mips interpreter with -g	Robert Norton

2016-01-21	mips interpreter successfully executes more than one instruction after some ↵	Robert Norton
	wrangling of integer types
2016-01-21	mips: rename GPRs so that they sort lexicographically for display.	Robert Norton

2016-01-20	see writes to registers in the register file for sequential interpreter	Kathy Gray

2016-01-20	keep specified order of vectors...	Kathy Gray

2016-01-20	Assorted bug fixes that gets one mips instruction running (then fails for ↵	Kathy Gray
	expected reasons) :)
2016-01-20	trim some obsolete/bitrotted make stuff.	Robert Norton

2016-01-20	build all mips stuff in _build. Still hacky and might be preferable to use ↵	Robert Norton
	ocamlbuild but works OK and shouldn't have to call sanitize.
2016-01-20	Decoding a mips instruction :)	Kathy Gray
	Not executing yet as some previous commit has broken the interpreter's local assignment
2016-01-20	Show opcode in sequential interpreter when decode fails	Kathy Gray

2016-01-19	Put None and Some into interpreter environments	Kathy Gray
	Also making progress towards separating int sized things from integer sized things
2016-01-19	hacky initial makery for mips interpreter. Builds stuff in wrong places and ↵	Robert Norton
	needs fixing but nearly works.
2016-01-15	mips.sail: Add commented out alternative DSLLV implementation using ↵	Robert Norton
	bitslicing which is closer to what appears in spec. Might want to swap all the SLLs at some point.
2016-01-14	small edit to previous commit	Kathy Gray