helm/www/matita/library.shtml

   1 <!--#include virtual="xhtml-header.shtml" -->
   2 <!-- $Id$ -->
   3 <html xmlns="http://www.w3.org/1999/xhtml">
   4   <head>
   5     <title>Matita - Library</title>
   6     <!--#include virtual="xhtml-meta.shtml" -->
   7   </head>
   8   <body>
   9     <!--#include virtual="menubar.shtml" -->
  10     <div class="main">
  11       <h1>Matita Library</h1>
  12
  13       <h2>Scripts<a name="scripts"></a></h2>
  14       <p>
  15       The <a href="library/">scripts</a> used to generate the knowledge base of
  16       Matita can be <a href="library/">browsed on line</a>.
  17       </p>
  18
  19       <br/>
  20
  21       <h1>Large Developments</h1>
  22
  23       <h2>Freescale<a name="freescale"></a></h2>
  24       <p>
  25       The <a href="freescale/">scripts</a> present:
  26       </p>
  27
  28       <ul>
  29        <li>an executable formalization of the operational semantics of
  30            any <a href="http://www.freescale.com">Freescale</a>
  31            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>
  32            </li>
  33        <li>a compiler from assembly language (pseudocodes + operands) to
  34        machine code</li>
  35        <li>several automatic checks for unhandled opcodes, memory accesses,
  36        correctness of ALU logic, etc.</li>
  37        <li>three examples of assembly programs (string reverse, counting sort
  38        and perfect numbers sieve) with sets of data to run them</li>
  39       </ul>
  40
  41       <p>The execution in the executable formalization has been compared
  42          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>
  43         in-circuit debugger.
  44       </p>
  45
  46       <p>
  47        The code (in <a href="http://caml.inria.fr">OCaml</a>)
  48        of an executable <a href="freescale/freescale_ocaml">emulator</a>,
  49        automatically generated from the scripts above. On the tests above,
  50        it runs at about 29% of the speed of the
  51        <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
  52        emulation engine.
  53       </p>
  54
  55       <p>The formalization has been the Undergraduate Thesis of
  56          Mr. Cosimo Oliboni. The manuscript (italian only) can be found
  57          <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
  58          here</a>.
  59       </p>
  60
  61       <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
  62       <p>
  63       See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>.
  64       </p>
  65
  66       <!--#include virtual="bottombar.shtml" -->
  67     </div>
  68   </body>
  69 </html>