Commit b8e73be7 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

update index-kvx.html

parent 2d086fdf
......@@ -65,9 +65,9 @@ inequations by fixpoint iteration.
<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.
<LI> <A HREF="html/compcert.kvx.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.kvx.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq.
<LI> <A HREF="html/compcert.scheduling.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
<LI> <A HREF="html/compcert.scheduling.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
<LI> <A HREF="html/compcert.scheduling.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.scheduling.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq.
</UL>
<font color=gray>
......@@ -130,7 +130,7 @@ view of the activation record.
<UL>
<LI> <A HREF="html/compcert.scheduling.RTLpath.html">RTLpath</A>: extends RTL with annotations for delimitating superblocks (with possible liveness information).
This IR is generic over the processor, and used for prepass scheduling.
<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).
<LI> <A HREF="html/compcert.scheduling.postpass_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 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.
......@@ -358,16 +358,16 @@ This IR is generic over the processor, even if currently, only used for KVX.
<TR valign="top" style="color:#000000">
<TD>Reconstruction of basic-blocks at Mach level</TD>
<TD>Mach to Machblock</TD>
<TD><A HREF="html/compcert.kvx.lib.Machblockgen.html">Machblockgen</A></TD>
<TD><A HREF="html/compcert.kvx.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
<A HREF="html/compcert.kvx.lib.Machblockgenproof.html">Machblockgenproof</A></TD>
<TD><A HREF="html/compcert.scheduling.postpass_lib.Machblockgen.html">Machblockgen</A></TD>
<TD><A HREF="html/compcert.scheduling.postpass_lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR>
<A HREF="html/compcert.scheduling.postpass_lib.Machblockgenproof.html">Machblockgenproof</A></TD>
</TR>
<TR valign="top" style="color:#000000">
<TD>Emission of purely sequential assembly code</TD>
<TD>Machblock to Asmblock</TD>
<TD><A HREF="html/compcert.kvx.Asmblockgen.html"><I>Asmblockgen</I></A></TD>
<TD><A HREF="html/compcert.kvx.lib.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
<TD><A HREF="html/compcert.kvx.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR>
<A HREF="html/compcert.kvx.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR>
<A HREF="html/compcert.kvx.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD>
</TR>
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment