+++
title = "General overview"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3a", "2e1c6a"]
forwardlinks = ["1b8", "3c3c", "3c3b1"]
zettelid = "3c3b"
+++

The following two intermediate languages were created for scheduling:

-   **RTLPar**: A basic block version of RTL with parallel blocks inside
    a basic block.
-   **RTLBlock**: A standard basic block.

It should be possible to extend these with conditional execution to
support hyperblocks ([\#1b8]), however the translation validation might
have to change for that.

-   **RTL** is translated to **RTLBlock** using translation validation
    to prove the correctness of the generation of basic blocks.
-   **RTLBlock** is translated to **RTLPar** by scheduling, which is
    also proven using translation validation.
-   **RTLPar** is finally translated to **HTL** in a verified manner, as
    no optimisations need to be performed.

This should replace the verified **RTL** to **HTL** translation.

  [\#1b8]: /zettel/1b8