xieby1's notes

Sail是ISA描述语言。

剩下的再讲啥？ 他要prove些啥？

他们设计了一套语言（Sail）来描述ISA。 为了能够严谨地描述ISA。 为了能够便利地生成各类theorem prover需要的格式。

所以我想要做什么？ 我想要学习他严谨描述ISA的方法。 然后应该会有新的想法。 比如如何度量指令距离。 如何把口头描述（ISA手册）给严谨化，是我需要学习的。