https://www.xcore.com/projects/formal-i ... tion-xcore
that XMOS has agreed to make fully public including code.
From chapter 1210 Results
10.1 Specification Improvements
Formal construction of the ISA specification revealed several issues in the published
specification, generally falling into three classes. Direct errors occurred where a
compiled executable would not execute under the specified behaviour: examples of
these were certain incorrectly specified operand field locations within an instruction.
Ambiguities can exist which can be open to misinterpretation and potentially lead to
differences in behaviour: for example addition calculations being in fact modulo
operation rather than a conventional addition with supporting exception condition on
overflow. Finally, omissions of certain functional conditions were discovered,
typically esoteric exception scenarios. For example, the requirement for dissimilar
destination registers during dual-destination instructions enabled discovery of an
undocumented exception implemented by the XCore for these instructions: the actual
machine robustly detects this error condition and yields an exception. Another
instruction was specified with different behaviours depending on the value of one of
its included immediate fields. Separate refinements were constructed for the two
forms of the instruction from separate abstract events, effectively defining separate
instructions, with differing exception conditions
1) What does this mean for the toolchain ?Completion of the model has driven the enhancement of the employed methodology
and tools, and numerous corrections to the existing ISA specification have been
identified and reported via the XMOS reporting system. The technical aspect of the
project has been dominated by the complexity of functionality specific to the XCore
ISA, and the model provides a valuable test-article for further analysis. Enhancements
made to the Rodin tool’s automatic prover have been submitted to the open-source
community for inclusion into further releases
Will this type of work fix small differences between the simulator and the real ISA, and thus also change the asm->machinecode compiler.
2) What is the problem in general that there is opcodes that isn't specified?
I know that the commodore C64 had many opcodes that didn't correspond to a documented operation, but some of the could be used anyway. On the other hand that made emulation of the C64 into a large amount of work, since the emulator had to emulate all possible opcodes that a programmer could use and the outcome of that.
