sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-09-30	Executing an actual elf file	Kathy Gray

2014-09-29	Connect up to elf model; which doesn't seem to be representing the elf file ↵	Kathy Gray
	properly yet but run_power.native is connected to it
2014-09-29	add run_power to last commit	Kathy Gray

2014-08-20	Add ability to track register dependencies in interactive stepper; thus ↵	Kathy Gray
	testing register tracking/tainting
2014-08-19	make test_power_interactive working again; now using interp_interface ↵	Kathy Gray
	instead of internal actions
2014-08-18	Handling many register reads, writes, and memory reads.	Kathy Gray
	There are problems that warrant discussion about handling special registers that hold records or data structures previously.
2014-08-18	Switch run_power to use interp_interface. Compilers and begins running, and ↵	Kathy Gray
	then hits an error. So still in progress Note: moved barrier kind changes to interp_interface, along with other memory kinds
2014-08-01	Support separated memory read/write functions.	Kathy Gray
	Also allows register writing functions to be on the left hand side of an assignment in the same way. The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.
2014-06-24	Get vector length for to_inc_vec and to_dec_vec from the type system after ↵	Kathy Gray
	constraint solving (instead of hardcoding 64 as the default).
2014-06-11	power.sail: store mode64bit in a bool register	Gabriel Kerneis
	This is now possible because we handle coercions better.
2014-06-09	Improve interaction after chat with Peter	Gabriel Kerneis
	- remember mode (run, step or next) between instructions - display continuation by default in step mode - start in step mode by default - incompatible change: the shorthand for stack is now bt (=backtrace), since s becomes the shorthand for step - incompatible change: pressing enter now repeats the current mode, instead of "step"
2014-06-07	Don't use cycle for fetch-decode-execute	Gabriel Kerneis

2014-06-07	Pattern-matching exhaustiveness	Gabriel Kerneis

2014-06-06	Add wrapper script and --interactive for demo	Gabriel Kerneis

2014-06-05	Shorten debug output for power	Gabriel Kerneis

2014-06-05	Enable single-stepping for test/power.sail	Gabriel Kerneis

2014-04-04	Cosmetic improvements (statistics, --quiet)	Gabriel Kerneis

2014-04-04	Improve Power execution	Gabriel Kerneis
	- Move FDE loop to the OCaml side of the Power model (avoid leaking memory due to lack of TCO in interpreter) - Display cycle count - Check the value of CIA at the end of each cycle and stop if it is equal to the initial value of LR, returning the value in GPR3.
2014-02-28	Fix endianness	Gabriel Kerneis
	In fact, increasing order is big-endian, not little-endian. This is good news for us, because it means we do not need any switch for the POWER spec.
2014-02-28	Fetch-decode POWER interpreter	Gabriel Kerneis
	Many limitations and bugs currently, but loads binary and decodes opcodes correctly (using endianness hacks). Disabled in the default test suite (but still compiled), run "make test_power" to try it.
2014-02-28	Load ELF sections to virtual memory addresses	Gabriel Kerneis
	Roughly 110KB/s (~5 seconds to load "hello" test).
2014-02-27	Load POWER binary into interpreter's memory	Gabriel Kerneis