sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-05-17	Experiment with making vector and bitvector distinct types	Alasdair Armstrong
	Only change that should be needed for 99.9% of uses is to change vector('n, 'ord, bit) to bitvector('n, 'ord), and adding $ifndef FEATURE_BITVECTOR_TYPE type bitvector('n, dec) = vector('n, dec, bit) $endif for to support any Sail before this Currently I have all C, Typechecking, and SMT tests passing, as well as the RISC-V spec building OCaml and C completely unmodified.
2019-04-17	SMT: Support generic vectors and handle lets between specs and functions	Alasdair Armstrong
	If we have e.g. $property val prop : ... let X = 0 function prop(...) = X == ... then we need to ensure that let X is included when we generate the property.