From 73d09048bb78826df7ef908918b89fcd2967978b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 22 Sep 2023 10:57:50 +0100 Subject: Add timing of scheduling to Compiler.v --- debug/vericertTest.ml | 78 +++++++++++++++++++++++++-------------------------- src/Compiler.v | 2 +- 2 files changed, 40 insertions(+), 40 deletions(-) diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml index 4d4e55f..48391db 100644 --- a/debug/vericertTest.ml +++ b/debug/vericertTest.ml @@ -104,14 +104,14 @@ let () = (* ] ] ] *) (* then Printf.printf "Passed 1\n" *) (* else Printf.printf "Failed 1\n"); *) - (if schedule_oracle [] - [ const (Some (plit true 1)) 1 0; - const (Some (Por (plit true 1, plit false 1))) 1 1; - ] - [ [ [ const None 1 1; - ] ] ] - then Printf.printf "Passed 1\n" - else Printf.printf "Failed 1\n"); + (* (if schedule_oracle [] *) + (* [ const (Some (plit true 1)) 1 0; *) + (* const (Some (Por (plit true 1, plit false 1))) 1 1; *) + (* ] *) + (* [ [ [ const None 1 1; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) (* (if schedule_oracle [(pred 3, pred 2)] *) (* [ add None 2 1 4; *) (* seteq None 1 10 11; *) @@ -172,35 +172,35 @@ let () = (* ] ] ] *) (* then Printf.printf "Passed 110\n" *) (* else Printf.printf "Failed 102\n"); *) - (* (if schedule_oracle [(pred 3, pred 2)] *) - (* [ *) - (* seteq None 1 10 11; *) - (* seteq None 3 12 13; *) - (* seteq None 2 12 13; *) - (* add None 2 1 4; *) - (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) - (* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *) - (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) - (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) - (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) - (* add (Some (plit true 1)) 1 2 4; *) - (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) - (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) - (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) - (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) - (* ] *) - (* [ [ [ seteq None 1 10 11; *) - (* seteq None 3 12 13; *) - (* seteq None 2 12 13; *) - (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) - (* add None 2 1 4; *) - (* add (Some (plit true 1)) 1 2 4; *) - (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) - (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) - (* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *) - (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) - (* goto None 10; *) - (* ] ] ] *) - (* then Printf.printf "Passed 110\n" *) - (* else Printf.printf "Failed 102\n") *) + (if schedule_oracle [] + [ + seteq None 1 10 11; + seteq None 3 12 13; + seteq None 2 12 13; + add None 2 1 4; + mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; + mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; + goto (Some (Pand (plit false 1, plit false 2))) 10; + mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; + goto (Some (Pand (plit false 1, plit true 2))) 10; + add (Some (plit true 1)) 1 2 4; + mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + goto (Some (Pand (plit true 1, plit false 2))) 10; + mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; + goto (Some (Pand (plit true 1, plit true 2))) 10; + ] + [ [ [ seteq None 1 10 11; + seteq None 3 12 13; + seteq None 2 12 13; + mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; + add None 2 1 4; + add (Some (plit true 1)) 1 2 4; + mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; + mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; + mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + goto None 10; + ] ] ] + then Printf.printf "Passed 110\n" + else Printf.printf "Failed 102\n") diff --git a/src/Compiler.v b/src/Compiler.v index d76db43..d3bcf95 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 @@ print (print_GiblePar 0) @@@ HTLPargen.transl_program @@ print (print_DHTL 0) -- cgit