diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
| commit | 0a44da6a7037d9eb270386eeef4f929177c4ec0d (patch) | |
| tree | ac08c768bbdedda7d791972ee0e2c4db1fb5ac14 /src/hls/GiblePar.v | |
| parent | 27714f85233e52978caebd67b550bde51e693d48 (diff) | |
| download | vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.tar.gz vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.zip | |
Rewrite a lot fixing scheduling of Gible
Diffstat (limited to 'src/hls/GiblePar.v')
| -rw-r--r-- | src/hls/GiblePar.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v index 8eb06ae..9600d16 100644 --- a/src/hls/GiblePar.v +++ b/src/hls/GiblePar.v @@ -35,10 +35,17 @@ RTLBlock ======== |*) -Module BB <: BlockType. +Module ParBB <: BlockType. Definition t := list (list (list instr)). + Definition foldl (A: Type) (f: A -> instr -> A) (bb : t) (m : A): A := + fold_left + (fun x l => fold_left (fun x' l' => fold_left f l' x') l x) + bb m. + + Definition length : t -> nat := @length (list (list instr)). + Section RELSEM. Context {A B: Type} (ge: Genv.t A B). @@ -63,13 +70,7 @@ function that can execute lists of things, given their execution rule. End RELSEM. - Definition max_reg (m : positive) (pc : node) (bb : t) := - fold_left - (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) - bb m. - - Definition length : t -> nat := @length (list (list instr)). - -End BB. +End ParBB. -Module GiblePar := Gible(BB). +Module GiblePar := Gible(ParBB). +Export GiblePar. |