Unreleased Features
The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation.
Scheduling #
Scheduling is an optimisation which is used to run various instructions in parallel that are independent to each other.
Operation Chaining #
Operation chaining is an optimisation that can be added on to scheduling and allows for the sequential execution of instructions in a clock cycle, while executing other instructions in parallel in the same clock cycle.
If-conversion #
If-conversion is an optimisation which can turn code with simple control flow into a single block (called a hyper-block), using predicated instructions.
Functions #
Functions are currently only inlined in Vericert, however, we are working on a proper interface to integrate function calls into the hardware.