diff options
| -rw-r--r-- | src/verilog/HTL.v (renamed from src/verilog/VTL.v) | 46 |
1 files changed, 28 insertions, 18 deletions
diff --git a/src/verilog/VTL.v b/src/verilog/HTL.v index 7273f96..1fc6932 100644 --- a/src/verilog/VTL.v +++ b/src/verilog/HTL.v @@ -7,39 +7,51 @@ Definition node := positive. Definition reg := Registers.reg. +Definition ident := AST.ident. + Inductive instruction : Type := | Vnop : node -> instruction | Vnonblock : Op.operation -> list reg -> reg -> node -> instruction | Vload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction | Vstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Vinst : AST.signature -> reg + AST.ident -> list reg -> reg -> node -> instruction -| Vtailinst : AST.signature -> reg + AST.ident -> list reg -> instruction +| Vinst : AST.signature -> ident -> list reg -> reg -> node -> instruction +| Vtailinst : AST.signature -> ident -> list reg -> instruction | Vcond : Op.condition -> list reg -> node -> node -> instruction | Vjumptable : reg -> list node -> instruction | Vfinish : option reg -> instruction. +Record inst : Type := + mkinst { +inst_start : reg; +inst_finish : reg; +inst_result : reg; +inst_args : list reg +}. + Definition code : Type := Maps.PTree.t instruction. +Definition instantiations : Type := Maps.PTree.t inst. + (** Function declaration for VTL also contain a construction which describes the functions that are called in the current function. This information is used to print out *) -Record function : Type := - mkfunction { - fn_sig : AST.signature; - fn_params : list reg; - fn_stacksize : Z; - fn_code : code; - fn_entrypoint : node; - fn_calledfuns : list AST.ident +Record module : Type := + mkmodule { + mod_sig : AST.signature; + mod_params : list reg; + mod_stacksize : Z; + mod_code : code; + mod_insts : inst; + mod_entrypoint : node }. -Definition fundef := AST.fundef function. +Definition moddef := AST.fundef module. -Definition design := AST.program fundef unit. +Definition design := AST.program moddef unit. -Definition funsig (fd : fundef) := - match fd with - | AST.Internal f => fn_sig f +Definition modsig (md : moddef) := + match md with + | AST.Internal m => mod_sig m | AST.External ef => AST.ef_sig ef end. @@ -56,8 +68,6 @@ Section TRANSF. f.(fn_params) f.(fn_stacksize) (Maps.PTree.map transf f.(fn_code)) - f.(fn_entrypoint) - f.(fn_calledfuns). + f.(fn_entrypoint). End TRANSF. - |