diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-09-22 10:57:50 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-09-22 10:58:41 +0100 |
| commit | 73d09048bb78826df7ef908918b89fcd2967978b (patch) | |
| tree | 1085f3c5a2ddffed465fa47a08f03c49b3654b21 | |
| parent | 24a34a9e3cbec7aaf2e4c3db20ccc5b541b25f20 (diff) | |
| download | vericert-73d09048bb78826df7ef908918b89fcd2967978b.tar.gz vericert-73d09048bb78826df7ef908918b89fcd2967978b.zip | |
Add timing of scheduling to Compiler.v
| -rw-r--r-- | debug/vericertTest.ml | 78 | ||||
| -rw-r--r-- | 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) |