diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-01 21:04:07 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-01 21:04:07 +0100 |
| commit | 6adade469bb17233e2526765d833ff870daf5d67 (patch) | |
| tree | d0595b9ea6feca35506b670eb567b5d40aae7a16 /src/hls/Veriloggen.v | |
| parent | 58ce9a801a3befd8fb6616edde8f2719679ae575 (diff) | |
| download | vericert-6adade469bb17233e2526765d833ff870daf5d67.tar.gz vericert-6adade469bb17233e2526765d833ff870daf5d67.zip | |
Remove some dead code from Veriloggen
Diffstat (limited to 'src/hls/Veriloggen.v')
| -rw-r--r-- | src/hls/Veriloggen.v | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index ff5dee5..630f35d 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -179,23 +179,6 @@ Section TRANSLATE. (List.filter (fun it => negb (Pos.eqb (fst (snd it)) main_name)) (PTree.elements (HTL.mod_externctrl m)))). - Definition find_module (prog : HTL.program) (name : ident) : Errors.res HTL.module := - match option_map snd (find (fun named_module => Pos.eqb (fst named_module) name) prog.(prog_defs)) with - | Some (Gfun (Internal f)) => OK f - | _ => Error (msg "Veriloggen: Could not find definition for called module") - end. - - Definition max_reg_module (m : HTL.module) : positive := - fold_left Pos.max ( - [ HTL.mod_st m - ; HTL.mod_stk m - ; HTL.mod_finish m - ; HTL.mod_return m - ; HTL.mod_start m - ; HTL.mod_reset m - ; HTL.mod_clk m - ] ++ HTL.mod_params m ++ map fst (PTree.elements (mod_scldecls m)) ++ map fst (PTree.elements (mod_arrdecls m))) 1%positive. - Definition prog_modmap (p : HTL.program) := PTree_Properties.of_list (Option.map_option (fun a => match a with |