diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-03-23 20:44:12 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-23 20:44:12 +0000 |
commit | 5fceb6772ae35c4d3847aa07ee414b79224f1fb3 (patch) | |
tree | 1f06d7fee7d0ebafc4e056b26fa8739a5e52db49 /src/verilog/HTL.v | |
parent | dfc519d9f0775025ec3db7253af3cd7c3012d96a (diff) | |
download | vericert-kvx-5fceb6772ae35c4d3847aa07ee414b79224f1fb3.tar.gz vericert-kvx-5fceb6772ae35c4d3847aa07ee414b79224f1fb3.zip |
Rename to HTL
Diffstat (limited to 'src/verilog/HTL.v')
-rw-r--r-- | src/verilog/HTL.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v new file mode 100644 index 0000000..1fc6932 --- /dev/null +++ b/src/verilog/HTL.v @@ -0,0 +1,73 @@ +From coqup.common Require Import Coquplib. + +From compcert Require Op Maps. +From compcert Require AST Memory Registers. + +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 -> 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 module : Type := + mkmodule { + mod_sig : AST.signature; + mod_params : list reg; + mod_stacksize : Z; + mod_code : code; + mod_insts : inst; + mod_entrypoint : node + }. + +Definition moddef := AST.fundef module. + +Definition design := AST.program moddef unit. + +Definition modsig (md : moddef) := + match md with + | AST.Internal m => mod_sig m + | AST.External ef => AST.ef_sig ef + end. + +(** Describes the transformation of VTL instruction by instruction. This applies + the transformation to each instruction in the function and returns the new + function with the modified instructions. *) +Section TRANSF. + + Variable transf : node -> instruction -> instruction. + + Definition transf_function (f : function) : function := + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + (Maps.PTree.map transf f.(fn_code)) + f.(fn_entrypoint). + +End TRANSF. |