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/PipelineOp.v | |
| parent | 27714f85233e52978caebd67b550bde51e693d48 (diff) | |
| download | vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.tar.gz vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.zip | |
Rewrite a lot fixing scheduling of Gible
Diffstat (limited to 'src/hls/PipelineOp.v')
| -rw-r--r-- | src/hls/PipelineOp.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v index bb01ff9..63d7d5a 100644 --- a/src/hls/PipelineOp.v +++ b/src/hls/PipelineOp.v @@ -28,8 +28,8 @@ Require Import compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePar. Require Import vericert.hls.FunctionalUnits. Import Option.Notation. @@ -56,8 +56,8 @@ Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb := let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l). -Definition find_divs (bb: bblock) := - snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)). +Definition find_divs (bb: ParBB.t) := + snd (List.fold_left div_pos_in_block bb (0%nat, nil)). Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B := match l with |