sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-07-04	Update power.sail	Gabriel Kerneis

2014-07-02	Update Power example	Gabriel Kerneis

2014-06-11	power.sail: store mode64bit in a bool register	Gabriel Kerneis
	This is now possible because we handle coercions better.
2014-06-11	Update power.sail: remove some hacks	Gabriel Kerneis

2014-06-07	Don't use cycle for fetch-decode-execute	Gabriel Kerneis

2014-06-07	exts returns bit[64] instead of nat	Gabriel Kerneis
	Update power.sail to new, pretty-printer-based version
2014-06-04	Fixup type coercions and overloading	Kathy Gray
	Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet
2014-06-02	Fix dependent-type for MEM in power.sail	Gabriel Kerneis
	Now, constraint resolution works for test/power.sail
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-04-03	Power example now EXECUTES (almost) CORRECTLY! \o/	Gabriel Kerneis
	Warning: we set the link register to the address of the first instruction, which means the program is effectively an infinite loop returning 42 forever. (Except it slows down and leaks memory, probably because the interpreter doesn't optimise the tail call in fde_loop.) 42, 42, 42, 42, 42, 42, 42, 42, ...
2014-04-03	Remove workarounds and update Power model	Gabriel Kerneis

2014-04-03	Exhibit two bugs about bitwise operators and vector casts	Gabriel Kerneis

2014-04-02	Fix EXTS and signedness of to_num	Gabriel Kerneis

2014-04-02	Update Power model	Gabriel Kerneis

2014-03-20	Add missing GPR registers for Power example	Gabriel Kerneis
	Second instruction now executes (but probably not correctly, check arithmetic since we ignore exts). Next step is to implement bitwise_or.
2014-03-20	Remove work-around from interpreter, move it to power.sail	Gabriel Kerneis
	Two bugs are worked-around here: - missing cast to nat when a vector is wrapped in exts (exts is a no-op currently anyway, so we are discarding it) - missing cast (due to limited type-inference) in one if branch: type given explicitly.
2014-03-19	Fetch-decode-execute & init for power	Gabriel Kerneis

2014-03-13	Make test_power compiling again	Gabriel Kerneis

2014-03-11	More work on interpreter and Power model	Gabriel Kerneis

2014-03-04	Minimal power model to run hello world	Gabriel Kerneis
	Crashes because register initialization is missing.
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-25	Sensible types for POWER registers	Gabriel Kerneis

2014-02-12	More library functions for interpreter	Gabriel Kerneis
	There is now enough stuff to decode and execute a very basic Branch instruction (encoding everything as little-endian rather than big- endian among many other work-arounds).
2014-02-12	Fix endianess issues	Gabriel Kerneis

2014-02-12	Remove spurious declaration	Gabriel Kerneis

2014-02-12	Fix type errors in power.sail	Gabriel Kerneis

2014-02-07	Implement is_one	Gabriel Kerneis

2014-02-07	Use bit->bool coercion for power.sail	Gabriel Kerneis

2014-02-05	Replace symbolic link by actual file	Gabriel Kerneis

2014-02-05	First bit of Power spec	Gabriel Kerneis
	Only chapter about branches (except system calls because of sail typechecking issue). Decoding seems to work. Execution typechecks currently, but is pretty surely broken otherwise.