aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTL.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-02-25 18:32:35 +0000
committerYann Herklotz <git@yannherklotz.com>2022-02-25 18:32:35 +0000
commit5f34267c4bccb471c71fd5698ec49adc99940850 (patch)
treed8d807f9f81bf8bcca9048201e9f7663e4a8c813 /src/hls/HTL.v
parent8d71333042d9ed87a80cffd4005daa0a0acc1810 (diff)
downloadvericert-5f34267c4bccb471c71fd5698ec49adc99940850.tar.gz
vericert-5f34267c4bccb471c71fd5698ec49adc99940850.zip
Fix up some more documentation
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r--src/hls/HTL.v11
1 files changed, 4 insertions, 7 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 551c66e..47f2092 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -36,13 +36,10 @@ Require Import ValueInt.
Local Open Scope positive.
-(*|
-The purpose of the hardware transfer language (HTL) is to create a more
-hardware-like layout that is still similar to the register transfer language
-(RTL) that it came from. The main change is that function calls become module
-instantiations and that we now describe a state machine instead of a
-control-flow graph.
-|*)
+(** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout
+that is still similar to the register transfer language (RTL) that it came from. The main change is
+that function calls become module instantiations and that we now describe a state machine instead of
+a control-flow graph. *)
Local Open Scope assocmap.