aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/HTL.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-03-29 16:41:09 +0100
committerYann Herklotz <git@yannherklotz.com>2020-03-29 16:41:09 +0100
commit65f30c5524280b5639a94674828986f0635b2477 (patch)
treebe05fd2acf456773a02dbc8a61135f9c187bc46e /src/verilog/HTL.v
parentc3106c7a61ecb79c1f1be0922aef32dffc92cc41 (diff)
downloadvericert-kvx-65f30c5524280b5639a94674828986f0635b2477.tar.gz
vericert-kvx-65f30c5524280b5639a94674828986f0635b2477.zip
Remove unnecessary examples from HTL
Diffstat (limited to 'src/verilog/HTL.v')
-rw-r--r--src/verilog/HTL.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 202a8b7..f2620a7 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -60,19 +60,19 @@ Definition modsig (md : moddecl) :=
| AST.External ef => AST.ef_sig ef
end.
-(** Describes the transformation of VTL instruction by instruction. This applies
+(** Describes various transformations that can be applied to HTL. 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.
+ Variable transf_instr : node -> instruction -> instruction.
- Definition transf_function (m : module) : module :=
+ Definition transf_module (m : module) : module :=
mkmodule
m.(mod_sig)
m.(mod_params)
m.(mod_stacksize)
- (PTree.map transf m.(mod_code))
+ (PTree.map transf_instr m.(mod_code))
m.(mod_insts)
m.(mod_entrypoint).