diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-19 14:45:57 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-19 15:00:40 +0100 |
commit | 74827ee343904cb5d2a5143daf3a79dfd23a6756 (patch) | |
tree | cf8e424439ca1a038b7bad82c5f5cd65fbf9a6b2 /src/hls/HTL.v | |
parent | 9bccd4a26cc9d04536ddba46b3e161eaaa422bf2 (diff) | |
download | vericert-74827ee343904cb5d2a5143daf3a79dfd23a6756.tar.gz vericert-74827ee343904cb5d2a5143daf3a79dfd23a6756.zip |
[WIP] Re-implement translation of calls.
Add an explicit map of local HTL registers to control signals and params
of other modules, used to implement calls.
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r-- | src/hls/HTL.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 5a55a55..4f00c79 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -54,6 +54,20 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> Z.pos p0 <= Integers.Int.max_unsigned. +Inductive controlsignal : Type := + | ctrl_finish : controlsignal + | ctrl_return : controlsignal + | ctrl_start : controlsignal + | ctrl_reset : controlsignal + | ctrl_param (idx : nat) : controlsignal. + +Definition controlsignal_sz (s : controlsignal) : nat := + match s with + | ctrl_param _ => 32 + | ctrl_return => 32 + | _ => 1 + end. + Record module: Type := mkmodule { mod_params : list reg; @@ -70,6 +84,9 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + (** Map from registers in this module to control registers in other modules. + These will be mapped to the same verilog register. *) + mod_externctrl : AssocMap.t (ident * controlsignal); mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. |