aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Verilog.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/Verilog.v')
-rw-r--r--src/hls/Verilog.v14
1 files changed, 14 insertions, 0 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index a7db3ba..ca5abd4 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -251,6 +251,20 @@ Definition posToLit (p : positive) : expr :=
Definition fext := unit.
Definition fextclk := nat -> fext.
+Definition map_body (f : list module_item -> list module_item) (m : module) :=
+ mkmodule
+ (mod_start m)
+ (mod_reset m)
+ (mod_clk m)
+ (mod_finish m)
+ (mod_return m)
+ (mod_st m)
+ (mod_stk m)
+ (mod_stk_len m)
+ (mod_args m)
+ (f (mod_body m))
+ (mod_entrypoint m).
+
(** ** State
The [state] contains the following items: