diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-29 15:42:09 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-29 15:42:09 +0000 |
| commit | dbbc756ea4dbea5102da914f888b369dfe39b892 (patch) | |
| tree | 7169007ded63a9a9ea9b021625933b59c6e66ae4 /src/hls/HTLPargen.v | |
| parent | 3539ac357ae86f8923e98887e7ff9cc5a7a09a94 (diff) | |
| download | vericert-dbbc756ea4dbea5102da914f888b369dfe39b892.tar.gz vericert-dbbc756ea4dbea5102da914f888b369dfe39b892.zip | |
Fix HTLPargen and RTLPargen
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 7e6f97c..2014c0e 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -519,7 +519,7 @@ Definition max_pc_map (m : Maps.PTree.t stmnt) := Lemma max_pc_map_sound: forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). Proof. - intros until i. unfold max_pc_function. + intros until i. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). (* extensionality *) intros. apply H0. rewrite H; auto. @@ -690,9 +690,9 @@ Definition transf_module (f: function) : mon HTL.module := do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); do _ <- collectlist (transf_bblock fin rtrn stack) - (Maps.PTree.elements f.(RTLPar.fn_code)); + (Maps.PTree.elements f.(fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) - f.(RTLPar.fn_params); + f.(fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; @@ -703,7 +703,7 @@ Definition transf_module (f: function) : mon HTL.module := Integers.Int.max_unsigned with | left LEDATA, left LECTRL => ret (HTL.mkmodule - f.(RTLPar.fn_params) + f.(fn_params) current_state.(st_datapath) current_state.(st_controllogic) f.(fn_entrypoint) @@ -748,7 +748,7 @@ Definition main_is_internal (p : RTLPar.program) : bool := | _ => false end. -Definition transl_program (p : RTLPar.program) : Errors.res HTL.program := +Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program := if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). |