Matita can be <a href="library/">browsed on line</a>.
</p>
+ <br/>
+
+ <h1>Large Developments</h1>
+
+ <h2>Freescale<a name="freescale"></a></h2>
+ <p>
+ The <a href="freescale/">scripts</a> present:
+ </p>
+
+ <ul>
+ <li>an executable formalization of the operational semantics of
+ any <a href="http://www.freescale.com">Freescale</a>
+ micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
+ <li>a compiler from assembly language (pseudocodes + operands) to
+ machine code
+ <li>several automatic checks for unhandled opcodes, memory accesses,
+ correctness of ALU logic, etc.
+ <li>three examples of assembly programs (string reverse, counting sort
+ and perfect numbers sieve) with sets of data to run them
+ </ul>
+ </a>
+
+ <p>The execution in the executable formalization has been compared
+ to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
+ in-circuit debugger.
+ </p>
+
+ <p>
+ The code (in <a href="http://caml.inria.fr">OCaml</a>)
+ of an executable <a href="freescale/freescale_ocaml">emulator</a>,
+ automatically generated from the scripts above. On the tests above,
+ it runs at about 29% of the speed of the
+ <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
+ emulation engine.
+ </p>
+
+ <p>The formalization has been the Undergraduate Thesis of
+ Mr. Cosimo Oliboni. The manuscript (italian only) can be found
+ <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
+ here</a>.
+ </p>
+
<!--#include virtual="bottombar.shtml" -->
</div>
</body>