diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:56:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:56:59 +0000 |
| commit | 8d71333042d9ed87a80cffd4005daa0a0acc1810 (patch) | |
| tree | 1453227ec7a8231d6c8e5c3050bc4af382138fa9 /src/hls | |
| parent | c1c5fc8e12342a9fe435c8066c8e9316036ff991 (diff) | |
| download | vericert-8d71333042d9ed87a80cffd4005daa0a0acc1810.tar.gz vericert-8d71333042d9ed87a80cffd4005daa0a0acc1810.zip | |
Start converting comments
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/IfConversion.v | 8 | ||||
| -rw-r--r-- | src/hls/RTLPargen.v | 20 |
2 files changed, 7 insertions, 21 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 4585770..9b8f4d4 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -30,14 +30,10 @@ Require Import vericert.bourdoncle.Bourdoncle. Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). -(*| -============= -If conversion -============= +(** * If conversion This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion -on basic blocks to make basic blocks larger. -|*) +on basic blocks to make basic blocks larger. *) Definition combine_pred (p: pred_op) (optp: option pred_op) := match optp with diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 58b048c..82f3f5e 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -34,24 +34,17 @@ Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. Import NE.NonEmptyNotation. -(*| -================= -RTLPar Generation -================= -|*) +(** * RTLPar Generation *) #[local] Open Scope positive. #[local] Open Scope forest. #[local] Open Scope pred_op. -(*| -Abstract Computations -===================== +(** ** Abstract Computations Define the abstract computation using the ``update`` function, which will set each register to its symbolic value. First we need to define a few helper functions to correctly translate the -predicates. -|*) +predicates. *) Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr := match l with @@ -146,9 +139,7 @@ Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) := Definition pred_ret {A: Type} (a: A) : predicated A := NE.singleton (T, a). -(*| -Update Function ---------------- +(** *** Update Function The ``update`` function will generate a new forest given an existing forest and a new instruction, so that it can evaluate a symbolic expression by folding over a list of instructions. The main @@ -158,8 +149,7 @@ problem is that predicates need to be merged as well, so that: 2. The expression assigned to the register should still be correct. This is done by multiplying the predicates together, and assigning the negation of the expression to -the other predicates. -|*) +the other predicates. *) Definition update (f : forest) (i : instr) : forest := match i with |