aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTL.v
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-04-30 16:08:09 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-04-30 18:33:53 +0100
commited97c6d4edeac9cab96be17b74ef02373ed36888 (patch)
treeeae4e8641e972428e7e2520d5d0342e6fdbbc5b8 /src/hls/HTL.v
parent2c5f867a347637cf1b651da7d041d9670493f540 (diff)
downloadvericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.tar.gz
vericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.zip
Tie all modules' clock to main
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r--src/hls/HTL.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 4f00c79..8474878 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -59,6 +59,7 @@ Inductive controlsignal : Type :=
| ctrl_return : controlsignal
| ctrl_start : controlsignal
| ctrl_reset : controlsignal
+ | ctrl_clk : controlsignal
| ctrl_param (idx : nat) : controlsignal.
Definition controlsignal_sz (s : controlsignal) : nat :=