diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
| commit | 2e39ecb491bbd001ecdfba73115bc76e3f53f517 (patch) | |
| tree | 7925ef9241e8b6d2a42dafe979010230ad36a84f /doc | |
| parent | 1bb219c2df5f7b06227a2bddfc24721a372847ab (diff) | |
| download | compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.tar.gz compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.zip | |
Improving the coqdoc
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index-kvx.html | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index 95fdb6de..ff3fbc17 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -60,7 +60,7 @@ inequations by fixpoint iteration. <LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph. </UL></font> -<H4>The <tt>abstractbb</tt> library, introduced for MPPA-KVX</H4> +<H4>The <tt>abstractbb</tt> library, introduced for KVX core</H4> <UL> <LI> <A HREF="html/compcert.kvx.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks. <LI> <A HREF="html/compcert.kvx.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. @@ -121,11 +121,11 @@ replaced by a linear list of instructions with explicit branches and labels. view of the activation record. </UL> </font> -<H4>Languages introduced for MPPA-KVX</H4> +<H4>Languages introduced for KVX core</H4> <UL> <LI> <A HREF="html/compcert.kvx.lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). -This IR is generic over the processor, even if currently, only used for MPPA_KVX. -<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for Mppa_KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. +This IR is generic over the processor, even if currently, only used for KVX. +<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. <LI> <A HREF="html/compcert.kvx.Asmblock.html"><I>Asmblock</I></A>: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks. This IR is an intermediate step between Machblock and Asmvliw. <LI> <A HREF="html/compcert.kvx.Asm.html"><I>Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax). @@ -294,7 +294,7 @@ This IR is generic over the processor, even if currently, only used for MPPA_KVX </TR> </TABLE> -<H4>Compilation passes introduced for MPPA-KVX</H4> +<H4>Compilation passes introduced for KVX VLIW</H4> <TABLE cellpadding="5%"> <TR valign="top"> <TD>Reconstruction of basic-blocks at Mach level</TD> |