diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 16:08:09 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 18:33:53 +0100 |
| commit | ed97c6d4edeac9cab96be17b74ef02373ed36888 (patch) | |
| tree | eae4e8641e972428e7e2520d5d0342e6fdbbc5b8 /src/hls/HTLgen.v | |
| parent | 2c5f867a347637cf1b651da7d041d9670493f540 (diff) | |
| download | vericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.tar.gz vericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.zip | |
Tie all modules' clock to main
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 5400e25..42631ca 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -584,7 +584,7 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition transf_module (f: function) : mon HTL.module := +Definition transf_module (main : ident) (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; @@ -593,7 +593,7 @@ Definition transf_module (f: function) : mon HTL.module := do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; - do clk <- create_reg (Some Vinput) 1; + do clk <- map_externctrl main ctrl_clk; do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with @@ -630,10 +630,10 @@ Definition max_state (f: function) : state := (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition transl_module (f : function) : Errors.res HTL.module := - run_mon (max_state f) (transf_module f). +Definition transl_module main (f : function) : Errors.res HTL.module := + run_mon (max_state f) (transf_module main f). -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transl_fundef main := transf_partial_fundef (transl_module main). (* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) @@ -877,5 +877,5 @@ Definition main_is_internal (p : RTL.program) : bool := Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p - then transform_partial_program transl_fundef p + then transform_partial_program (transl_fundef p.(prog_main)) p else Errors.Error (Errors.msg "Main function is not Internal."). |