aboutsummaryrefslogtreecommitdiffstats
path: root/src/Compiler.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2023-09-17 12:09:25 +0100
committerYann Herklotz <git@yannherklotz.com>2023-09-17 12:09:25 +0100
commit6a74d2e648903e54300f276a024e396978629b30 (patch)
tree09ca1e0a809df82c01338d313857a4562bdf8f74 /src/Compiler.v
parentc9d0a0bea2f547a9706e9524f20baf9778df805a (diff)
downloadvericert-6a74d2e648903e54300f276a024e396978629b30.tar.gz
vericert-6a74d2e648903e54300f276a024e396978629b30.zip
Add unhashed functions for comparisons
Diffstat (limited to 'src/Compiler.v')
-rw-r--r--src/Compiler.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index d76db43..8e28792 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -293,7 +293,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
@@ print (print_GibleSeq 4)
@@@ DeadBlocks.transf_program
@@ print (print_GibleSeq 5)
- @@@ GiblePargen.transl_program
+ @@@ time "Scheduling" GiblePargen.transl_program_unhashed
@@ print (print_GiblePar 0)
@@@ HTLPargen.transl_program
@@ print (print_DHTL 0)