diff options
| -rw-r--r-- | .ocamlformat | 0 | ||||
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | _CoqProject | 5 | ||||
| -rw-r--r-- | benchmarks/polybench-syn/linear-algebra/solvers/durbin.c | 47 | ||||
| -rw-r--r-- | benchmarks/polybench-syn/stencils/fdtd-2d.c | 7 | ||||
| -rw-r--r-- | default.nix | 2 | ||||
| -rw-r--r-- | driver/VericertDriver.ml | 16 | ||||
| -rw-r--r-- | example/explanation.org | 81 | ||||
| -rw-r--r-- | example/interesting.v | 36 | ||||
| -rw-r--r-- | include/hls.h | 72 | ||||
| -rw-r--r-- | shell.nix | 4 | ||||
| -rw-r--r-- | src/Compiler.v | 100 | ||||
| -rw-r--r-- | src/VericertClflags.ml | 2 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 287 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 17 | ||||
| -rw-r--r-- | src/hls/Array.v (renamed from src/verilog/Array.v) | 0 | ||||
| -rw-r--r-- | src/hls/AssocMap.v (renamed from src/verilog/AssocMap.v) | 0 | ||||
| -rw-r--r-- | src/hls/HTL.v (renamed from src/verilog/HTL.v) | 0 | ||||
| -rw-r--r-- | src/hls/HTLBlockgen.v | 655 | ||||
| -rw-r--r-- | src/hls/HTLSchedulegen.v | 42 | ||||
| -rw-r--r-- | src/hls/HTLgen.v (renamed from src/translation/HTLgen.v) | 8 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v (renamed from src/translation/HTLgenproof.v) | 29 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v (renamed from src/translation/HTLgenspec.v) | 0 | ||||
| -rw-r--r-- | src/hls/Partition.ml | 125 | ||||
| -rw-r--r-- | src/hls/PrintHTL.ml (renamed from src/verilog/PrintHTL.ml) | 0 | ||||
| -rw-r--r-- | src/hls/PrintRTLBlock.ml | 119 | ||||
| -rw-r--r-- | src/hls/PrintVerilog.ml (renamed from src/verilog/PrintVerilog.ml) | 0 | ||||
| -rw-r--r-- | src/hls/PrintVerilog.mli (renamed from src/verilog/PrintVerilog.mli) | 0 | ||||
| -rw-r--r-- | src/hls/RTLBlock.v | 170 | ||||
| -rw-r--r-- | src/hls/RTLBlockgen.v | 32 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 99 | ||||
| -rw-r--r-- | src/hls/Schedule.ml | 610 | ||||
| -rw-r--r-- | src/hls/Value.v (renamed from src/verilog/Value.v) | 0 | ||||
| -rw-r--r-- | src/hls/ValueInt.v (renamed from src/verilog/ValueInt.v) | 0 | ||||
| -rw-r--r-- | src/hls/ValueVal.v | 209 | ||||
| -rw-r--r-- | src/hls/Verilog.v (renamed from src/verilog/Verilog.v) | 4 | ||||
| -rw-r--r-- | src/hls/Veriloggen.v (renamed from src/translation/Veriloggen.v) | 0 | ||||
| -rw-r--r-- | src/hls/Veriloggenproof.v (renamed from src/translation/Veriloggenproof.v) | 0 | ||||
| -rw-r--r-- | test/array.c | 6 | ||||
| -rw-r--r-- | test/loop.c | 3 | ||||
| -rwxr-xr-x | test/test_all.sh | 8 |
41 files changed, 2767 insertions, 40 deletions
diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/.ocamlformat @@ -8,17 +8,20 @@ endif COMPCERTRECDIRS := lib common verilog backend cfrontend driver exportclight cparser -COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \ - -R src/extraction vericert.extraction -R src/translation vericert.translation \ +COQINCLUDES := -R src/common vericert.common \ + -R src/extraction vericert.extraction \ + -R src/hls vericert.hls \ -R src vericert \ - $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) + $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \ + -R lib/CompCert/flocq Flocq \ + -R lib/CompCert/MenhirLib MenhirLib COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := $(COQBIN)coq_makefile COQDOCFLAGS := --no-lib-name -l -VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v) +VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v) PREFIX ?= . @@ -35,6 +38,7 @@ lib/COMPCERTSTAMP: install: install -d $(PREFIX)/bin + sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini install -C _build/default/driver/compcert.ini $(PREFIX)/bin/. install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert diff --git a/_CoqProject b/_CoqProject index 7d455a5..69d12c1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,17 +1,14 @@ -R src/common vericert.common -R src/extraction vericert.extraction --R src/translation vericert.translation --R src/verilog vericert.verilog +-R src/hls vericert.hls -R src vericert --R lib/CompCert/MenhirLib compcert.MenhirLib -R lib/CompCert/backend compcert.backend -R lib/CompCert/cfrontend compcert.cfrontend -R lib/CompCert/common compcert.common -R lib/CompCert/cparser compcert.cparser -R lib/CompCert/driver compcert.driver -R lib/CompCert/exportclight compcert.exportclight --R lib/CompCert/flocq compcert.flocq -R lib/CompCert/lib compcert.lib -R lib/CompCert/verilog compcert.verilog -R lib/CompCert/flocq Flocq diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c b/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c index dd6d05e..5c853a7 100644 --- a/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c +++ b/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c @@ -9,6 +9,48 @@ */ /* durbin.c: this file is part of PolyBench/C */ +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +unsigned int divider(unsigned int x, unsigned int y) +{ + unsigned int r0, q0, y0, y1; + + r0 = x; + q0 = 0; + y0 = y; + y1 = y; + do + { + y1 = 2 * y1; + } while (y1 <= x); + do + { + y1 = y1 / 2; + q0 = 2 * q0; + if (r0 >= y1) + { + r0 = r0 - y1; + q0 = q0 + 1; + } + } while ((int)y1 != (int)y0); + return q0; +} + +int sdivider(int N, int D) { + if (D < 0) { + if (N < 0) + return divider(-N, -D); + else + return -divider(N, -D); + } else { + if (N < 0) + return -divider(-N, D); + else + return divider(N, D); + } +} unsigned int divider(unsigned int x, unsigned int y) { @@ -79,6 +121,10 @@ int print_array(int n, res += y[i]; } +#ifndef SYNTHESIS + printf("finished = %u\n", res); +#endif + return res; } @@ -105,7 +151,6 @@ void kernel_durbin(int n, sum += r[k-i-ONE]*y[i]; } alpha = - sdivider(r[k] + sum, beta); - //alpha = - (r[k] + sum) / beta; for (i=0; i<k; plus(i)) { z[i] = y[i] + alpha*y[k-i-ONE]; diff --git a/benchmarks/polybench-syn/stencils/fdtd-2d.c b/benchmarks/polybench-syn/stencils/fdtd-2d.c index 17acd34..f9f4a84 100644 --- a/benchmarks/polybench-syn/stencils/fdtd-2d.c +++ b/benchmarks/polybench-syn/stencils/fdtd-2d.c @@ -9,6 +9,9 @@ */ /* fdtd-2d.c: this file is part of PolyBench/C */ +#ifndef SYNTHESIS +#include <stdio.h> +#endif #define plus(i) i = i + ONE static @@ -64,6 +67,10 @@ int print_array(int nx, res ^= hz[i][j]; } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + return res; } diff --git a/default.nix b/default.nix index a253285..3c8bc92 100644 --- a/default.nix +++ b/default.nix @@ -30,7 +30,7 @@ stdenv.mkDerivation { buildInputs = [ ncoq ocamlPackages.menhir dune ocaml ocamlPackages.findlib bbv - gcc + gcc ocamlPackages.utop ]; enableParallelBuilding = true; diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index f500499..0c02aeb 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintClight.destination option_dclight ".light.c"; set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; + set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -91,7 +92,11 @@ let compile_c_file sourcename ifile ofile = close_out oc end else begin let verilog = - match Vericert.Compiler0.transf_hls csyntax with + let translation = if !option_hls_schedule + then Vericert.Compiler0.transf_hls_temp + else Vericert.Compiler0.transf_hls_opt + in + match translation csyntax with | Vericert.Errors.OK v -> v | Vericert.Errors.Error msg -> @@ -242,6 +247,9 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -falign-branch-targets <n> Set alignment (in bytes) of branch targets -falign-cond-branches <n> Set alignment (in bytes) of conditional branches -fcommon Put uninitialized globals in the common section [on]. + +HLS Optimisations: + -fschedule Schedule the resulting hardware [off]. |} ^ target_help ^ toolchain_help ^ @@ -254,6 +262,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -dclight Save generated Clight in <file>.light.c -dcminor Save generated Cminor in <file>.cm -drtl Save RTL at various optimization points in <file>.rtl.<n> + -drtlblock Save RTLBlock <file>.rtlblock -dhtl Save HTL before Verilog generation <file>.htl -dltl Save LTL after register allocation in <file>.ltl -dmach Save generated Mach code in <file>.mach @@ -351,7 +360,7 @@ let cmdline_actions = Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n); Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n); - Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @ + Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n); ] @ f_opt "common" option_fcommon @ (* Target processor options *) (if Vericert.Configuration.arch = "arm" then @@ -379,6 +388,7 @@ let cmdline_actions = Exact "-dclight", Set option_dclight; Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; + Exact "-drtlblock", Set option_drtlblock; Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; @@ -391,6 +401,7 @@ let cmdline_actions = option_dclight := true; option_dcminor := true; option_drtl := true; + option_drtlblock := true; option_dhtl := true; option_dltl := true; option_dalloctrace := true; @@ -422,6 +433,7 @@ let cmdline_actions = (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) + @ f_opt "schedule" option_hls_schedule @ [ (* Catch options that are not handled *) Prefix "-", Self (fun s -> diff --git a/example/explanation.org b/example/explanation.org new file mode 100644 index 0000000..793c890 --- /dev/null +++ b/example/explanation.org @@ -0,0 +1,81 @@ +#+title: Interesting edge case in Simulation and Synthesis Mismatch + +I have always known about situations where the simulation might not match the synthesised result, for example when blocking assignment is used in one always block and is read from another. However, the following mismatch is slightly surprising to me because I feel like simulators should be giving the same result as synthesis tools, as it seems to be quite common. Otherwise, it also seems fair that the synthesis tool should implement what the simulator is showing, as it is strange to get such different results. + +I tested the following with the Quartus 20.1 and Yosys 0.9+2406 synthesis tool (which both gave the same result) and the icarus verilog, verilator and ModelSim simulators which also agreed with each other. + +Assuming we want to implement the following design. My expectation would be that it just basically assigns ~a~ to ~x~ whenever ~a~ changes. + +#+begin_src verilog +module top(a, x); + reg [3:0] tmp; + input [3:0] a; + output reg [3:0] x; + + always @* begin + x = tmp; + tmp = a; + end +endmodule // top +#+end_src + +This seems to be correct when looking at the synthesised design printed by Yosys. + +#+begin_src verilog +/* Generated by Yosys 0.9+2406 (git sha1 000fd08198, clang++ 7.1.0 -fPIC -Os) */ +module top_synth(a, x); + input [3:0] a; + wire [3:0] tmp; + output [3:0] x; + assign tmp = a; + assign x = a; +endmodule +#+end_src + +However, when simulating it with the following testbench, it instead acts like a shift register. + +#+begin_src verilog +module main; + reg [3:0] a; + wire [3:0] x, x_synth; + + top top(a, x); + top_synth top_synth(a, x_synth); + + initial begin + a = 0; + #10 a = 1; + #10 $display("x: %d\nx_synth: %d", x, x_synth); + $finish; + end +endmodule +#+end_src + +The test bench above prints + +#+begin_src text +x: 0 +x_synth: 1 +#+end_src + +showing that the synthesised design does not match the simulated design. + +Is the test bench that I wrote slightly broken? Or is this expected to be this different. In the latter case, how come simulators don't implement the correct behaviour? This could be done by recursing and reevaluating the always block when an element in the sensitivity list changed, even if that was in the same always block. + +Even in simulation I would expect these two snippets to act the same + +#+begin_src verilog +always @* begin + x = tmp; + tmp = a; +end +#+end_src + +#+begin_src verilog +always @* begin + tmp = a; + x = tmp; +end +#+end_src + +Because ~a~ and ~tmp~ are both in the sensitivity list, meaning in the first code snippet, it should reevaluate the always block and update the ~x~ register with the correct value which is ~a~. diff --git a/example/interesting.v b/example/interesting.v new file mode 100644 index 0000000..c76f92a --- /dev/null +++ b/example/interesting.v @@ -0,0 +1,36 @@ +module top(a, x); + reg [3:0] tmp; + input [3:0] a; + output reg [3:0] x; + + always @* begin + x = tmp; + tmp = a; + end +endmodule // top + +`ifndef SYNTHESIS +/* Generated by Yosys 0.9+2406 (git sha1 000fd08198, clang++ 7.1.0 -fPIC -Os) */ +module top_synth(a, x); + input [3:0] a; + wire [3:0] tmp; + output [3:0] x; + assign tmp = a; + assign x = a; +endmodule + +module main; + reg [3:0] a; + wire [3:0] x, x_synth; + + top top(a, x); + top_synth top_synth(a, x_synth); + + initial begin + a = 0; + #10 a = 1; + #10 $display("x: %d\nx_synth: %d", x, x_synth); + $finish; + end +endmodule +`endif diff --git a/include/hls.h b/include/hls.h new file mode 100644 index 0000000..61c336b --- /dev/null +++ b/include/hls.h @@ -0,0 +1,72 @@ +#ifndef VERICERT_HLS_H +#define VERICERT_HLS_H + +/* + * Divider C implementation for faster frequency division. + */ +unsigned divider_fast(unsigned x, unsigned y) { + unsigned r0, q0, y0, y1; + + r0 = x; + q0 = 0; + y0 = y; + y1 = y; + do { + y1 = 2 * y1; + } while (y1 <= x); + do { + y1 /= 2; + q0 *= 2; + if (r0 >= y1) { + r0 -= y1; + q0++; + } + } while ((int)y1 != (int)y0); + return q0; +} + +unsigned divider(unsigned x, unsigned y) { + unsigned q0, acc; + q0 = 0; + acc = y; + + while (acc <= x) { + q0++; + acc += y; + } + + return q0; +} + +/* + * Signed division operation for faster frequency division. + */ +int sdivider(int N, int D) { + if (D < 0) { + if (N < 0) + return divider(-N, -D); + else + return -divider(N, -D); + } else { + if (N < 0) + return -divider(-N, D); + else + return divider(N, D); + } +} + +int sdivider_fast(int N, int D) { + if (D < 0) { + if (N < 0) + return divider_fast(-N, -D); + else + return -divider_fast(N, -D); + } else { + if (N < 0) + return -divider_fast(-N, D); + else + return divider_fast(N, D); + } +} + +#endif @@ -1,5 +1,7 @@ with import <nixpkgs> {}; mkShell { - buildInputs = (import ./.).buildInputs ++ [ocamlPackages.ocp-indent verilog yosys]; + buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent verilog yosys + ocamlPackages.merlin ocamlPackages.utop + ]; } diff --git a/src/Compiler.v b/src/Compiler.v index 6efd7a2..8eeea6b 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -51,12 +51,16 @@ From vericert Require Verilog Veriloggen Veriloggenproof - HTLgen. + HTLgen + RTLBlock + RTLBlockgen + HTLSchedulegen. From compcert Require Import Smallstep. Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. +Parameter print_RTLBlock: RTLBlock.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -80,13 +84,45 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. +Definition total_if {A: Type} + (flag: unit -> bool) (f: A -> A) (prog: A) : A := + if flag tt then f prog else prog. + +Definition partial_if {A: Type} + (flag: unit -> bool) (f: A -> res A) (prog: A) : res A := + if flag tt then f prog else OK prog. + +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + +Definition transf_backend_opt (r : RTL.program) : res Verilog.program := + OK r + @@@ Inlining.transf_program + @@ print (print_RTL 1) + @@ Renumber.transf_program + @@ print (print_RTL 2) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ print (print_RTL 3) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ print (print_RTL 4) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ print (print_RTL 5) + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ print (print_RTL 6) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 7) + @@@ HTLgen.transl_program + @@ print print_HTL + @@ Veriloggen.transl_program. + Definition transf_backend (r : RTL.program) : res Verilog.program := OK r @@@ Inlining.transf_program - @@ print (print_RTL 1) + @@ print (print_RTL 1) + @@ Renumber.transf_program + @@ print (print_RTL 2) @@@ HTLgen.transl_program - @@ print print_HTL - @@ Veriloggen.transl_program. + @@ print print_HTL + @@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@ -96,9 +132,48 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program - @@ print (print_RTL 0) + @@ print (print_RTL 0) @@@ transf_backend. +Definition transf_hls_opt (p : Csyntax.program) : res Verilog.program := + OK p + @@@ SimplExpr.transl_program + @@@ SimplLocals.transf_program + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ Selection.sel_program + @@@ RTLgen.transl_program + @@ print (print_RTL 0) + @@@ transf_backend_opt. + +Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := + OK p + @@@ SimplExpr.transl_program + @@@ SimplLocals.transf_program + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ Selection.sel_program + @@@ RTLgen.transl_program + @@@ Inlining.transf_program + @@ print (print_RTL 1) + @@ Renumber.transf_program + @@ print (print_RTL 2) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ print (print_RTL 3) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ print (print_RTL 4) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ print (print_RTL 5) + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ print (print_RTL 6) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 7) + @@@ RTLBlockgen.transl_program + @@ print print_RTLBlock + @@@ HTLSchedulegen.transl_program + @@ print print_HTL + @@ Veriloggen.transl_program. + Local Open Scope linking_scope. Definition CompCert's_passes := @@ -109,6 +184,7 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass Inliningproof.match_prog + ::: mkpass Renumberproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -132,8 +208,9 @@ Proof. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. - destruct (HTLgen.transl_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := Veriloggen.transl_program p8) in *. + set (p8 := Renumber.transf_program p7) in *. + destruct (HTLgen.transl_program p8) as [p9|e] eqn:P9; simpl in T; try discriminate. + set (p10 := Veriloggen.transl_program p9) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -142,8 +219,9 @@ Proof. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply Inliningproof.transf_program_match; auto. - exists p8; split. apply HTLgenproof.transf_program_match; auto. - exists p9; split. apply Veriloggenproof.transf_program_match; auto. + exists p8; split. apply Renumberproof.transf_program_match; auto. + exists p9; split. apply HTLgenproof.transf_program_match; auto. + exists p10; split. apply Veriloggenproof.transf_program_match; auto. inv T. reflexivity. Qed. @@ -171,7 +249,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p9)). + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -188,6 +266,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. + eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. eapply Veriloggenproof.transf_program_correct; eassumption. } diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index ca591de..26b4053 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -4,3 +4,5 @@ let option_hls = ref true let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false +let option_drtlblock = ref false +let option_hls_schedule = ref false diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index c9b5dbd..f44cac2 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -362,4 +362,291 @@ Module IntExtra. rewrite testbit_repr; auto. Abort. + Lemma div_divs_equiv : + forall x y, + signed x >= 0 -> + signed y >= 0 -> + divs x y = divu x y. + Proof. + unfold divs, divu. + intros. + rewrite !signed_eq_unsigned; + try rewrite Zquot.Zquot_Zdiv_pos; try reflexivity; + lazymatch goal with + | |- unsigned _ <= max_signed => + solve [rewrite <- signed_positive; assumption] + | |- 0 <= unsigned _ => solve [apply unsigned_range_2] + end. + Qed. + + Lemma neg_signed' : + forall x : int, + unsigned x <> 2147483648 -> + signed (neg x) = - signed x. + Proof. + intros x Hhalf. + Transparent repr. + unfold signed. + simpl. + rewrite Z_mod_modulus_eq. + replace modulus with 4294967296; auto. + replace half_modulus with 2147483648; auto. + repeat match goal with | |- context[if ?x then _ else _] => destruct x end. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e. auto. + + pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296). + assert (4294967296 <> 0) by lia. + apply H in H0. + rewrite H0 in l. + pose proof (Z.mod_small (unsigned x) 4294967296). + assert (0 <= unsigned x < 4294967296). + pose proof (unsigned_range_2 x). lia. + apply H1 in H2. rewrite H2 in l. lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz; try lia. + rewrite Z.opp_sub_distr. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). + simplify; lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + simplify; lia. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e in *. rewrite Z.opp_0 in *. rewrite Zmod_0_l in g. lia. + + rewrite Z.mod_opp_l_nz; try lia. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz in g; try lia. + rewrite Z.mod_small in g. + assert (unsigned x < 2147483648) by lia. lia. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in * by auto. lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in * by auto. lia. + Qed. + + Lemma neg_divs_distr_l : + forall x y, + unsigned x <> 2147483648 -> + neg (divs x y) = divs (neg x) y. + Proof. + intros x y Hhalf. unfold divs, neg. + set (x' := signed x). set (y' := signed y). + apply eqm_samerepr. + apply eqm_trans with (- (Z.quot x' y')). + auto with ints. + replace (- (Z.quot x' y')) with (Z.quot (- x') y') + by (rewrite Zquot.Zquot_opp_l; auto). + unfold x'. + rewrite <- neg_signed'. + auto with ints. + assumption. + Qed. + + Lemma neg_signed : + forall x : int, + unsigned x <> 2147483648 -> + signed x < 0 -> + signed (neg x) >= 0. + Proof. + intros. + rewrite neg_signed'. lia. + assumption. + Qed. + + Lemma shl_signed_positive : + forall y, + unsigned y <= 30 -> + signed (shl one y) >= 0. + Proof. + intros. + unfold signed, shl. + destruct (zlt (unsigned (repr (Z.shiftl (unsigned one) (unsigned y)))) half_modulus). + - rewrite unsigned_repr. + + rewrite Z.shiftl_1_l. + apply Z.le_ge. apply Z.pow_nonneg. lia. + + rewrite Z.shiftl_1_l. split. + apply Z.pow_nonneg. lia. + simplify. + replace (4294967295) with (2 ^ 32 - 1); try lia. + transitivity (2 ^ 31); try lia. + apply Z.pow_le_mono_r; lia. + - simplify. rewrite Z.shiftl_1_l in g. + unfold half_modulus, modulus, wordsize, + Wordsize_32.wordsize in *. unfold two_power_nat in *. simplify. + unfold Z_mod_modulus in *. + destruct (2 ^ unsigned y) eqn:?. + apply Z.ge_le in g. exfalso. + replace (4294967296 / 2) with (2147483648) in g; auto. + rewrite Z.shiftl_1_l. rewrite Heqz. + unfold wordsize in *. unfold Wordsize_32.wordsize in *. + rewrite Zbits.P_mod_two_p_eq in *. + replace (4294967296 / 2) with (2147483648) in g; auto. + rewrite <- Heqz in g. + rewrite Z.mod_small in g. + replace (2147483648) with (2 ^ 31) in g. + pose proof (Z.pow_le_mono_r 2 (unsigned y) 30). + apply Z.ge_le in g. + assert (0 < 2) by lia. apply H0 in H1. lia. assumption. lia. + split. lia. rewrite two_power_nat_equiv. + apply Z.pow_lt_mono_r; lia. + + pose proof (Zlt_neg_0 p). + pose proof (pow2_nonneg (unsigned y)). rewrite <- Heqz in H0. + lia. + Qed. + + Lemma is_power2_shl : + forall y, + unsigned y <= 30 -> + is_power2 (shl one y) = Some y. + Proof. + intros. + unfold is_power2, shl. + destruct (Zbits.Z_is_power2 (unsigned (repr (Z.shiftl (unsigned one) (unsigned y))))) eqn:?. + - simplify. + rewrite Z_mod_modulus_eq in Heqo. + rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo. + rewrite <- two_p_correct in Heqo. + rewrite Zbits.Z_is_power2_complete in Heqo. inv Heqo. + rewrite repr_unsigned. auto. + pose proof (unsigned_range_2 y). lia. + rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize. + rewrite two_power_nat_equiv. + split. apply pow2_nonneg. + apply Z.pow_lt_mono_r; lia. + - simplify. + rewrite Z_mod_modulus_eq in Heqo. + rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo. + rewrite <- two_p_correct in Heqo. + rewrite Zbits.Z_is_power2_complete in Heqo. discriminate. + pose proof (unsigned_range_2 y). lia. + rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize. + rewrite two_power_nat_equiv. + split. apply pow2_nonneg. + apply Z.pow_lt_mono_r; lia. + Qed. + + Definition shrx_alt (x y : int) : int := + if zlt (signed x) 0 + then neg (shru (neg x) y) + else shru x y. + + Lemma shrx_shrx_alt_equiv_ne : + forall x y, + unsigned x <> 2147483648 -> + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros x y Hhalf H. + unfold shrx, shrx_alt, lt. + destruct (Z_ge_lt_dec (signed x) 0); + [rewrite zlt_false | rewrite zlt_true]; + + repeat lazymatch goal with + | |- is_power2 _ = Some _ => apply is_power2_shl + | |- signed (shl one _) >= 0 => apply shl_signed_positive + | |- signed (neg _) >= 0 => apply neg_signed + | |- divs _ _ = divu _ _ => apply div_divs_equiv + | |- divs ?x (shl one ?y) = neg (shru (neg ?x) ?y) => + rewrite <- neg_involutive at 1; rewrite neg_divs_distr_l; + try assumption; f_equal + | |- divs ?x (shl one ?y) = shru ?x ?y => + let H := fresh "H" in + pose proof (divu_pow2 x (shl one y) y) as H; + rewrite <- H + end; try assumption. + Qed. + + Lemma shrx_shrx_alt_equiv_eq : + forall x y, + unsigned x = 2147483648 -> + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros. + repeat unfold shrx, shrx_alt, signed, divs, neg. + replace half_modulus with 2147483648 by auto. + replace modulus with 4294967296 by auto. + simplify. + rewrite !Z_mod_modulus_eq. + rewrite !H. + simplify. + assert (Hshl: Z.shiftl 1 (unsigned y) mod 4294967296 = Z.shiftl 1 (unsigned y)). + { apply Z.mod_small. + rewrite Z.shiftl_1_l. + split. + apply pow2_nonneg. + replace 4294967296 with (2^32) by auto. + apply Z.le_lt_trans with (m := 2 ^ 31); try lia. + apply Z.pow_le_mono_r; lia. + } + rewrite !Hshl. + f_equal. + assert ((Z.shiftl 1 (unsigned y)) < 2147483648). + rewrite Z.shiftl_1_l. + replace 2147483648 with (2^31) by auto. + apply Z.le_lt_trans with (m := 2 ^ 30); try lia. + apply Z.pow_le_mono_r; lia. + destruct (zlt (Z.shiftl 1 (unsigned y)) 2147483648); try lia. + replace (-2147483648 mod 4294967296) with 2147483648 by auto. + assert (Hmodeq : Z.shiftr 2147483648 (unsigned y) mod 4294967296 + = Z.shiftr 2147483648 (unsigned y)). + { apply Z.mod_small. split. + apply Z.shiftr_nonneg. lia. + rewrite Z.shiftr_div_pow2. + replace 4294967296 with (Z.succ 4294967295); auto. + apply Zle_lt_succ. + replace 4294967295 with (4294967295 * (2 ^ unsigned y) / (2 ^ unsigned y)). + 2: { + apply Z.div_mul. + pose proof (Z.pow_pos_nonneg 2 (unsigned y)). + apply not_eq_sym. + apply Z.le_neq. apply H2; try lia. + apply unsigned_range_2. + } + + apply Z.div_le_mono. + apply Z.pow_pos_nonneg. lia. + apply unsigned_range_2. + transitivity 4294967295; try lia. + apply Z.le_mul_diag_r; try lia. + replace 1 with (Z.succ 0) by auto. + apply Z.le_succ_l. + apply Z.pow_pos_nonneg; try lia. + apply unsigned_range_2. apply unsigned_range_2. + } + rewrite !Hmodeq. + replace (-2147483648) with (Z.opp 2147483648) by auto. + rewrite Zquot.Zquot_opp_l. + f_equal. + rewrite Zquot.Zquot_Zdiv_pos. + rewrite Z.shiftr_div_pow2. + rewrite Z.shiftl_1_l. auto. + apply unsigned_range_2. + lia. + rewrite Z.shiftl_1_l. + apply Z.lt_le_incl. + apply Z.pow_pos_nonneg; try lia. + apply unsigned_range_2. + Qed. + + Theorem shrx_shrx_alt_equiv : + forall x y, + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros. + destruct (Z.eq_dec (unsigned x) 2147483648); + [ apply shrx_shrx_alt_equiv_eq | apply shrx_shrx_alt_equiv_ne]; auto. + Qed. + End IntExtra. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index b1a885e..c2b3951 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -16,7 +16,14 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From vericert Require Verilog Value Compiler. +From vericert Require + Verilog + Value + Compiler + RTLBlockgen + RTLBlock + HTLSchedulegen + HTLgen. From Coq Require DecidableClass. @@ -128,6 +135,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". +Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". @@ -162,12 +170,19 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false". Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". +Extract Constant RTLBlockgen.partition => "Partition.partition". +Extract Constant HTLSchedulegen.transl_module => "Schedule.transl_module". + (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls + vericert.Compiler.transf_hls_temp + vericert.Compiler.transf_hls_opt + RTLBlockgen.transl_program RTLBlock.successors_instr + HTLgen.tbl_to_case_expr Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/verilog/Array.v b/src/hls/Array.v index fe0f6b2..fe0f6b2 100644 --- a/src/verilog/Array.v +++ b/src/hls/Array.v diff --git a/src/verilog/AssocMap.v b/src/hls/AssocMap.v index 8d8788a..8d8788a 100644 --- a/src/verilog/AssocMap.v +++ b/src/hls/AssocMap.v diff --git a/src/verilog/HTL.v b/src/hls/HTL.v index 620ef14..620ef14 100644 --- a/src/verilog/HTL.v +++ b/src/hls/HTL.v diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v new file mode 100644 index 0000000..5f40962 --- /dev/null +++ b/src/hls/HTLBlockgen.v @@ -0,0 +1,655 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +(*From compcert Require Import Maps. +From compcert Require Errors Globalenvs Integers. +From compcert Require Import AST. +From vericert Require Import RTLBlock Verilog HTL Vericertlib AssocMap ValueInt Statemonad. + +Hint Resolve AssocMap.gempty : htlh. +Hint Resolve AssocMap.gso : htlh. +Hint Resolve AssocMap.gss : htlh. +Hint Resolve Ple_refl : htlh. +Hint Resolve Ple_succ : htlh. + +Record state: Type := mkstate { + st_st : reg; + st_freshreg: reg; + st_freshstate: node; + st_scldecls: AssocMap.t (option io * scl_decl); + st_arrdecls: AssocMap.t (option io * arr_decl); + st_datapath: datapath; + st_controllogic: controllogic; +}. + +Definition init_state (st : reg) : state := + mkstate st + 1%positive + 1%positive + (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty (option io * arr_decl)) + (AssocMap.empty stmnt) + (AssocMap.empty stmnt). + +Module HTLState <: State. + + Definition st := state. + + Inductive st_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (forall n, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2. + Hint Constructors st_incr : htlh. + + Definition st_prop := st_incr. + Hint Unfold st_prop : htlh. + + Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + + Lemma st_trans : + forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. + - destruct H4 with n; destruct H8 with n; intuition congruence. + - destruct H5 with n; destruct H9 with n; intuition congruence. + Qed. + +End HTLState. +Export HTLState. + +Module HTLMonad := Statemonad(HTLState). +Export HTLMonad. + +Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). +Import HTLMonadExtra. +Export MonadNotation. + +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue n)). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). + +Definition check_empty_node_datapath: + forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. +Proof. + intros. case (s.(st_datapath)!n); tauto. +Defined. + +Definition check_empty_node_controllogic: + forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. +Proof. + intros. case (s.(st_controllogic)!n); tauto. +Defined. + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Lemma declare_reg_state_incr : + forall i s r sz, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Proof. auto with htlh. Qed. + +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := + fun s => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr i s r sz). + +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Lemma add_instr_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Lemma add_node_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_node_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))) + (add_node_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. +Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. + +Definition bop (op : binop) (r1 r2 : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)). + +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue l)). + +Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) + | Integers.Cne, r1::nil => ret (boplit Vne r1 i) + | Integers.Clt, r1::nil => ret (boplit Vlt r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) + | Integers.Cle, r1::nil => ret (boplit Vle r1 i) + | Integers.Cge, r1::nil => ret (boplit Vge r1 i) + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2) + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Clt, r1::nil => ret (boplit Vltu r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) + | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) + | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i) + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := + match c, args with + | Op.Ccomp c, _ => translate_comparison c args + | Op.Ccompu c, _ => translate_comparisonu c args + | Op.Ccompimm c i, _ => translate_comparison_imm c args i + | Op.Ccompuimm c i, _ => translate_comparison_immu c args i + | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") + | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") + end. + +Definition check_address_parameter_signed (p : Z) : bool := + Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.max_signed. + +Definition check_address_parameter_unsigned (p : Z) : bool := + Z.leb p Integers.Ptrofs.max_unsigned. + +Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds") + | Op.Ascaled scale offset, r1::nil => + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter_signed offset) + then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds") + | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vlit (ZToValue a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") + end. + +(** Translate an instruction to a statement. FIX mulhs mulhu *) +Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := + match op, args with + | Op.Omove, r::nil => ret (Vvar r) + | Op.Ointconst n, _ => ret (Vlit (intToValue n)) + | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) + | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulimm n, r::nil => ret (boplit Vmul r n) + | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") + | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) + | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) + | Op.Oandimm n, r::nil => ret (boplit Vand r n) + | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) + | Op.Oorimm n, r::nil => ret (boplit Vor r n) + | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2) + | Op.Oxorimm n, r::nil => ret (boplit Vxor r n) + | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2) + | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) + | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) + | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) + | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm") + (*ret (Vbinop Vdiv (Vvar r) + (Vbinop Vshl (Vlit (ZToValue 1)) + (Vlit (intToValue n))))*) + | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) + | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) + | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) + | Op.Ocmp c, _ => translate_condition c args + | Op.Osel c AST.Tint, r1::r2::rl => + do tc <- translate_condition c rl; + ret (Vternary tc (Vvar r1) (Vvar r2)) + | Op.Olea a, _ => translate_eff_addressing a args + | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") + end. + +Lemma add_branch_instr_state_incr: + forall s e n n1 n2, + (st_datapath s) ! n = None -> + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). +Proof. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. + +Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left NSTM, left NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) + | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") + end. + +Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) + (args : list reg) (stack : reg) : mon expr := + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vvari stack (Vlit (ZToValue (a / 4)))) + else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") + end. + +Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := + match ns with + | n :: ns' => (i, n) :: enumerate (i+1) ns' + | nil => nil + end. + +Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := + List.map (fun a => match a with + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + end) + (enumerate 0 ns). + +Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := + match ni with + (n, i) => + match i with + | Inop n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + add_instr n n' Vskip + else error (Errors.msg "State is larger than 2^32.") + | Iop op args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst instr) + else error (Errors.msg "State is larger than 2^32.") + | Iload mem addr args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst src) + else error (Errors.msg "State is larger than 2^32.") + | Istore mem addr args src n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do dst <- translate_arr_access mem addr args stack; + add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + else error (Errors.msg "State is larger than 2^32.") + | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") + | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") + | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") + | Icond cond args n1 n2 => + if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then + do e <- translate_condition cond args; + add_branch_instr e n n1 n2 + else error (Errors.msg "State is larger than 2^32.") + | Ijumptable r tbl => + (*do s <- get; + add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) + error (Errors.msg "Ijumptable: Case statement not supported.") + | Ireturn r => + match r with + | Some r' => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) + | None => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) + end + end + end. + +Lemma create_reg_state_incr: + forall s sz i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg (i : option io) (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s sz i). + +Lemma create_arr_state_incr: + forall s sz ln i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := + fun s => let r := s.(st_freshreg) in + OK (r, ln) (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)) + (create_arr_state_incr s sz ln i). + +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). + +Definition max_pc_map (m : Maps.PTree.t stmnt) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). +Proof. + intros until i. unfold max_pc_function. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. + +Lemma max_pc_wf : + forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + +Definition transf_module (f: function) : mon module := + if stack_correct f.(fn_stacksize) then + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end + else error (Errors.msg "Stack size misalignment."). + +Definition max_state (f: function) : state := + let st := Pos.succ (max_reg_function f) in + mkstate st + (Pos.succ st) + (Pos.succ (max_pc_function f)) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) + (st_arrdecls (init_state st)) + (st_datapath (init_state st)) + (st_controllogic (init_state st)). + +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +Definition transl_fundef := transf_partial_fundef transl_module. + +(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) + +(*Definition transl_main_fundef f : Errors.res HTL.fundef := + match f with + | Internal f => transl_fundef (Internal f) + | External f => Errors.Error (Errors.msg "Could not find internal main function") + end. + +(** Translation of a whole program. *) + +Definition transl_program (p: RTL.program) : Errors.res HTL.program := + transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i + then transl_fundef f + else transl_main_fundef f) + (fun i v => Errors.OK v) p. +*) + +Definition main_is_internal (p : RTLBlock.program) : bool := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. + +Definition transl_program (p : RTLBlock.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). +*) diff --git a/src/hls/HTLSchedulegen.v b/src/hls/HTLSchedulegen.v new file mode 100644 index 0000000..1ae3bf6 --- /dev/null +++ b/src/hls/HTLSchedulegen.v @@ -0,0 +1,42 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +From compcert Require Import Maps. +From compcert Require Errors Globalenvs Integers. +From compcert Require Import AST. +From vericert Require Import RTLBlock Verilog HTL Vericertlib AssocMap ValueInt Statemonad. + +Parameter transl_module : function -> Errors.res module. + +Definition transl_fundef := transf_partial_fundef transl_module. + +Definition main_is_internal (p : RTLBlock.program) : bool := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. + +Definition transl_program (p : RTLBlock.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/translation/HTLgen.v b/src/hls/HTLgen.v index 68e0293..5f0f8bf 100644 --- a/src/translation/HTLgen.v +++ b/src/hls/HTLgen.v @@ -358,10 +358,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm") - (*ret (Vbinop Vdiv (Vvar r) - (Vbinop Vshl (Vlit (ZToValue 1)) - (Vlit (intToValue n))))*) + | Op.Oshrximm n, r::nil => + ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) + (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) + (Vbinop Vshru (Vvar r) (Vlit n))) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") diff --git a/src/translation/HTLgenproof.v b/src/hls/HTLgenproof.v index bf63800..213fe7d 100644 --- a/src/translation/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1,4 +1,4 @@ -(* + (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -470,7 +470,11 @@ Section CORRECTNESS. | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H - | |- Verilog.expr_runp _ _ _ _ _ => econstructor + | |- Verilog.expr_runp _ _ _ ?f _ => + match f with + | Verilog.Vternary _ _ _ => idtac + | _ => econstructor + end | |- val_value_lessdef (?f _ _) _ => unfold f | |- val_value_lessdef (?f _) _ => unfold f | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ => @@ -716,6 +720,24 @@ Section CORRECTNESS. repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor. Qed. + Lemma eval_correct_Oshrximm : + forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st n, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> + (RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') -> + Op.eval_operation ge sp (Op.Oshrximm n) + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> + translate_instr (Op.Oshrximm n) args s = OK e s' i -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + Proof. + intros s sp rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st n MSTATE INSTR EVAL TR_INSTR. + pose proof MSTATE as MSTATE_2. inv MSTATE. + inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; + unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL. + (*repeat (simplify; eval_correct_tac; unfold valueToInt in * ). + destruct (Z_lt_ge_dec (Int.signed i0) 0). + econstructor.*) + Abort. + Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> @@ -754,6 +776,7 @@ Section CORRECTNESS. - rewrite Heqb in Heqb0. discriminate. (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, repeat (rewrite Int.unsigned_repr). auto.*) + - admit. - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + unfold translate_eff_addressing in *. repeat (unfold_match H1). destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac. @@ -876,7 +899,7 @@ Section CORRECTNESS. destruct (Int.unsigned x0 ==Z Int.unsigned Int.zero); try discriminate. rewrite <- Z.eqb_neq in n0. rewrite Int.unsigned_zero in n0. rewrite n0. auto. constructor. - Qed. + Admitted. (** The proof of semantic preservation for the translation of instructions is a simulation argument based on diagrams of the following form: diff --git a/src/translation/HTLgenspec.v b/src/hls/HTLgenspec.v index 541f9fa..541f9fa 100644 --- a/src/translation/HTLgenspec.v +++ b/src/hls/HTLgenspec.v diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml new file mode 100644 index 0000000..d9bccad --- /dev/null +++ b/src/hls/Partition.ml @@ -0,0 +1,125 @@ + (* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlock + +(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_edge i n = + let succ = RTL.successors_instr i in + let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in + ((match filt with [] -> [] | _ -> [n]), filt) + +let find_edges c = + PTree.fold (fun l n i -> + let f = find_edge i n in + (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let translate_inst = function + | RTL.Inop _ -> Some RBnop + | RTL.Iop (op, ls, dst, _) -> Some (RBop (op, ls, dst)) + | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (m, addr, ls, dst)) + | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (m, addr, ls, src)) + | _ -> None + +let translate_cfi = function + | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n)) + | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls)) + | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n)) + | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2)) + | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls)) + | RTL.Ireturn r -> Some (RBreturn r) + | _ -> None + +let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = + let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in + let trans_inst = (translate_inst i, translate_cfi i) in + match trans_inst, succ with + | (None, Some i'), _ -> + if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) } + else + Errors.OK { bb_body = []; bb_exit = Some i' } + | (Some i', None), (s', Some i_n)::[] -> + if List.exists (fun x -> x = s) (fst e) then + Errors.OK { bb_body = [i']; bb_exit = Some (RBgoto s') } + else if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) } + else begin + match next_bblock_from_RTL false e c s' i_n with + | Errors.OK bb -> + Errors.OK (prepend_instr i' bb) + | Errors.Error msg -> Errors.Error msg + end + | _, _ -> + Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) + +let rec traverseacc f l c = + match l with + | [] -> Errors.OK c + | x::xs -> + match f x c with + | Errors.Error msg -> Errors.Error msg + | Errors.OK x' -> + match traverseacc f xs x' with + | Errors.Error msg -> Errors.Error msg + | Errors.OK xs' -> Errors.OK xs' + +let rec translate_all edge c s res = + let c_bb, translated = res in + if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else + (match PTree.get s c with + | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all.")) + | Some i -> + match next_bblock_from_RTL true edge c s i with + | Errors.Error msg -> Errors.Error msg + | Errors.OK {bb_exit = None; _} -> + Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all")) + | Errors.OK {bb_body = bb; bb_exit = Some e} -> + let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in + (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c', t') -> + Errors.OK (PTree.set s {bb_body = bb; bb_exit = Some e} c', t'))) + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + let e = find_edges f.RTL.fn_code in + match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c, _) -> + Errors.OK { fn_sig = f.RTL.fn_sig; + fn_stacksize = f.RTL.fn_stacksize; + fn_params = f.RTL.fn_params; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = c + } + +let partition = function_from_RTL diff --git a/src/verilog/PrintHTL.ml b/src/hls/PrintHTL.ml index 44f8b01..44f8b01 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/hls/PrintHTL.ml diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml new file mode 100644 index 0000000..45bd253 --- /dev/null +++ b/src/hls/PrintRTLBlock.ml @@ -0,0 +1,119 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlock +open PrintAST + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(op, ls, dst) -> + fprintf pp "%a = %a\n" + reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]\n" + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a\n" + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + +let print_bblock_exit pp i = + fprintf pp "\t\t"; + match i with + | Some(RBcall(_, fn, args, res, _)) -> + fprintf pp "%a = %a(%a)\n" + reg res ros fn regs args; + | Some(RBtailcall(_, fn, args)) -> + fprintf pp "tailcall %a(%a)\n" + ros fn regs args + | Some(RBbuiltin(ef, args, res, _)) -> + fprintf pp "%a = %s(%a)\n" + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args + | Some(RBcond(cond, args, s1, s2)) -> + fprintf pp "if (%a) goto %d else goto %d\n" + (PrintOp.print_condition reg) (cond, args) + (P.to_int s1) (P.to_int s2) + | Some(RBjumptable(arg, tbl)) -> + let tbl = Array.of_list tbl in + fprintf pp "jumptable (%a)\n" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | Some(RBreturn None) -> + fprintf pp "return\n" + | Some(RBreturn (Some arg)) -> + fprintf pp "return %a\n" reg arg + | Some(RBgoto n) -> + fprintf pp "goto %d\n" (P.to_int n) + | None -> fprintf pp "\n" + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (print_bblock_body pp) i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program oc prog; + close_out oc diff --git a/src/verilog/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 44710b8..44710b8 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml diff --git a/src/verilog/PrintVerilog.mli b/src/hls/PrintVerilog.mli index 6a15ee9..6a15ee9 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/hls/PrintVerilog.mli diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v new file mode 100644 index 0000000..dc505ed --- /dev/null +++ b/src/hls/RTLBlock.v @@ -0,0 +1,170 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. + +Definition node := positive. + +Inductive instruction : Type := +| RBnop : instruction +| RBop : operation -> list reg -> reg -> instruction +| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction +| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction. + +Definition bblock_body : Type := list instruction. + +Inductive control_flow_inst : Type := +| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst +| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst +| RBbuiltin : external_function -> list (builtin_arg reg) -> + builtin_res reg -> node -> control_flow_inst +| RBcond : condition -> list reg -> node -> node -> control_flow_inst +| RBjumptable : reg -> list node -> control_flow_inst +| RBreturn : option reg -> control_flow_inst +| RBgoto : node -> control_flow_inst. + +Record bblock : Type := mk_bblock { + bb_body: bblock_body; + bb_exit: option control_flow_inst + }. + +Definition code : Type := PTree.t bblock. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. + +Definition successors_instr (i : control_flow_inst) : list node := + match i with + | RBcall sig ros args res s => s :: nil + | RBtailcall sig ros args => nil + | RBbuiltin ef args res s => s :: nil + | RBcond cond args ifso ifnot => ifso :: ifnot :: nil + | RBjumptable arg tbl => tbl + | RBreturn optarg => nil + | RBgoto n => n :: nil + end. + +(* Definition genv := Genv.t fundef unit. +Definition regset := Regmap.t val. + +Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := + match rl, vl with + | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) + | _, _ => Regmap.init Vundef + end. + +Inductive stackframe : Type := + | Stackframe: + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (pc: node) (**r program point in calling function *) + (rs: regset), (**r register state in calling function *) + stackframe. + +Inductive cont : Type := + | C + | N. + +Inductive state : Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (m: mem) (**r memory state *) + (bblock: bblock) (**r bblock being executed *) + (c : cont), + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. + +Section RELSEM. + +Variable ge: genv. + +Definition find_function + (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +Inductive step : state -> trace -> state -> Prop := + | exec_RBnop : + forall s f sp pc rs m ls ci, + step (State s f sp pc rs m (mk_bblock (RBnop :: ls) ci) C) E0 + (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C) + | exec_RBop : + forall s f sp pc rs m ls args op res ci v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp pc rs m (mk_bblock (RBop op args res :: ls) ci) C) E0 + (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C) + | exec_RBload: + forall s f sp pc rs m chunk addr args dst a v ls ci, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step (State s f sp pc rs m (mk_bblock (RBload chunk addr args dst :: ls) ci) C) + E0 (State s f sp (Pos.succ pc) (rs#dst <- v) m (mk_bblock ls ci) C) + | exec_RBstore: + forall s f sp pc rs m chunk addr args src a m' ls ci, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + step (State s f sp pc rs m (mk_bblock (RBstore chunk addr args src :: ls) ci) C) + E0 (State s f sp (Pos.succ pc) rs m' (mk_bblock ls ci) C) + | exec_RBcond: + forall s f sp pc rs m cond args ifso ifnot b pc', + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C) + E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N) +. + +End RELSEM. +*) diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v new file mode 100644 index 0000000..6b3e9c3 --- /dev/null +++ b/src/hls/RTLBlockgen.v @@ -0,0 +1,32 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +From compcert Require + RTL. +From compcert Require Import + AST + Maps. +From vericert Require Import + RTLBlock. + +Parameter partition : RTL.function -> Errors.res function. + +Definition transl_fundef := transf_partial_fundef partition. + +Definition transl_program : RTL.program -> Errors.res program := + transform_partial_program transl_fundef. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v new file mode 100644 index 0000000..af3f28b --- /dev/null +++ b/src/hls/RTLPar.v @@ -0,0 +1,99 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +From compcert Require Import Coqlib Maps. +From compcert Require Import AST Integers Values Events Memory Globalenvs Smallstep. +From compcert Require Import Op Registers. + +Definition node := positive. + +Inductive instruction : Type := +| RPnop : instruction +| RPop : operation -> list reg -> reg -> instruction +| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction +| RPstore : memory_chunk -> addressing -> list reg -> reg -> instruction. + +Definition bblock_body : Type := list (list instruction). + +Inductive control_flow_inst : Type := +| RPcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst +| RPtailcall : signature -> reg + ident -> list reg -> control_flow_inst +| RPbuiltin : external_function -> list (builtin_arg reg) -> + builtin_res reg -> node -> control_flow_inst +| RPcond : condition -> list reg -> node -> node -> control_flow_inst +| RPjumptable : reg -> list node -> control_flow_inst +| RPreturn : option reg -> control_flow_inst +| RPgoto : node -> control_flow_inst. + +Record bblock : Type := mk_bblock { + bb_body: bblock_body; + bb_exit: option control_flow_inst + }. + +Definition code : Type := PTree.t bblock. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. + +Definition successors_instr (i : control_flow_inst) : list node := + match i with + | RPcall sig ros args res s => s :: nil + | RPtailcall sig ros args => nil + | RPbuiltin ef args res s => s :: nil + | RPcond cond args ifso ifnot => ifso :: ifnot :: nil + | RPjumptable arg tbl => tbl + | RPreturn optarg => nil + | RPgoto n => n :: nil + end. + +(*Inductive state : Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. +*) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml new file mode 100644 index 0000000..982aa0e --- /dev/null +++ b/src/hls/Schedule.ml @@ -0,0 +1,610 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlock +open HTL +open Verilog +open HTLgen +open HTLMonad +open HTLMonadExtra + +module IMap = Map.Make (struct + type t = int + + let compare = compare +end) + +type dfg = { nodes : instruction list; edges : (int * int) list } +(** The DFG type defines a list of instructions with their data dependencies as [edges], which are + the pairs of integers that represent the index of the instruction in the [nodes]. The edges + always point from left to right. *) + +let print_list f out_chan a = + fprintf out_chan "[ "; + List.iter (fprintf out_chan "%a " f) a; + fprintf out_chan "]" + +let print_tuple out_chan a = + let l, r = a in + fprintf out_chan "(%d,%d)" l r + +let print_dfg out_chan dfg = + fprintf out_chan "{ nodes = %a, edges = %a }" + (print_list PrintRTLBlock.print_bblock_body) + dfg.nodes (print_list print_tuple) dfg.edges + +let read_process command = + let buffer_size = 2048 in + let buffer = Buffer.create buffer_size in + let string = Bytes.create buffer_size in + let in_channel = Unix.open_process_in command in + let chars_read = ref 1 in + while !chars_read <> 0 do + chars_read := input in_channel string 0 buffer_size; + Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read + done; + ignore (Unix.close_process_in in_channel); + Buffer.contents buffer + +(** Add a dependency if it uses a register that was written to previously. *) +let add_dep i tree deps curr = + match PTree.get curr tree with None -> deps | Some ip -> (ip, i) :: deps + +(** This function calculates the dependencies of each instruction. The nodes correspond to previous + register that were allocated and show which instruction caused it. + + This function only gathers the RAW constraints, and will therefore only be active for operations + that modify registers, which is this case only affects loads and operations. *) +let accumulate_RAW_deps dfg curr = + let i, dst_map, { edges; nodes } = dfg in + let acc_dep_instruction rs dst = + ( i + 1, + PTree.set dst i dst_map, + { + nodes; + edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges; + } ) + in + let acc_dep_instruction_nodst rs = + ( i + 1, + dst_map, + { + nodes; + edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges; + } ) + in + match curr with + | RBop (_, rs, dst) -> acc_dep_instruction rs dst + | RBload (_mem, _addr, rs, dst) -> acc_dep_instruction rs dst + | RBstore (_mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) + | _ -> (i + 1, dst_map, { edges; nodes }) + +(** Finds the next write to the [dst] register. This is a small optimisation so that only one + dependency is generated for a data dependency. *) +let rec find_next_dst_write i dst i' curr = + let check_dst dst' curr' = + if dst = dst' then Some (i, i') + else find_next_dst_write i dst (i' + 1) curr' + in + match curr with + | [] -> None + | RBop (_, _, dst') :: curr' -> check_dst dst' curr' + | RBload (_, _, _, dst') :: curr' -> check_dst dst' curr' + | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr' + +let rec find_all_next_dst_read i dst i' curr = + let check_dst rs curr' = + if List.exists (fun x -> x = dst) rs + then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr' + else find_all_next_dst_read i dst (i' + 1) curr' + in + match curr with + | [] -> [] + | RBop (_, rs, _) :: curr' -> check_dst rs curr' + | RBload (_, _, rs, _) :: curr' -> check_dst rs curr' + | RBstore (_, _, rs, src) :: curr' -> check_dst (src :: rs) curr' + | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' + +let drop i lst = + let rec drop' i' lst' = + match lst' with + | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls + | [] -> [] + in + if i = 0 then lst else drop' 1 lst + +let take i lst = + let rec take' i' lst' = + match lst' with + | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls + | [] -> [] + in + if i = 0 then [] else take' 1 lst + +let rec next_store i = function + | [] -> None + | RBstore (_, _, _, _) :: _ -> Some i + | _ :: rst -> next_store (i + 1) rst + +let rec next_load i = function + | [] -> None + | RBload (_, _, _, _) :: _ -> Some i + | _ :: rst -> next_load (i + 1) rst + +let accumulate_RAW_mem_deps dfg curr = + let i, { nodes; edges } = dfg in + match curr with + | RBload (_, _, _, _) -> ( + match next_store 0 (take i nodes |> List.rev) with + | None -> (i + 1, { nodes; edges }) + | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) ) + | _ -> (i + 1, { nodes; edges }) + +let accumulate_WAR_mem_deps dfg curr = + let i, { nodes; edges } = dfg in + match curr with + | RBstore (_, _, _, _) -> ( + match next_load 0 (take i nodes |> List.rev) with + | None -> (i + 1, { nodes; edges }) + | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) ) + | _ -> (i + 1, { nodes; edges }) + +let accumulate_WAW_mem_deps dfg curr = + let i, { nodes; edges } = dfg in + match curr with + | RBstore (_, _, _, _) -> ( + match next_store 0 (take i nodes |> List.rev) with + | None -> (i + 1, { nodes; edges }) + | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) ) + | _ -> (i + 1, { nodes; edges }) + +(** This function calculates the WAW dependencies, which happen when two writes are ordered one + after another and therefore have to be kept in that order. This accumulation might be redundant + if register renaming is done before hand, because then these dependencies can be avoided. *) +let accumulate_WAW_deps dfg curr = + let i, { edges; nodes } = dfg in + let dst_dep dst = + match find_next_dst_write i dst (i + 1) (drop (i + 1) nodes) with + | Some d -> (i + 1, { nodes; edges = d :: edges }) + | _ -> (i + 1, { nodes; edges }) + in + match curr with + | RBop (_, _, dst) -> dst_dep dst + | RBload (_, _, _, dst) -> dst_dep dst + | RBstore (_, _, _, _) -> ( + match next_store (i + 1) (drop (i + 1) nodes) with + | None -> (i + 1, { nodes; edges }) + | Some i' -> (i + 1, { nodes; edges = (i, i') :: edges }) ) + | _ -> (i + 1, { nodes; edges }) + +let accumulate_WAR_deps dfg curr = + let i, { edges; nodes } = dfg in + let dst_dep dst = + let dep_list = find_all_next_dst_read i dst 0 (take i nodes |> List.rev) + |> List.map (function (d, d') -> (i - d' - 1, d)) + in + (i + 1, { nodes; edges = List.append dep_list edges }) + in + match curr with + | RBop (_, _, dst) -> dst_dep dst + | RBload (_, _, _, dst) -> dst_dep dst + | _ -> (i + 1, { nodes; edges }) + +let assigned_vars vars = function + | RBnop -> vars + | RBop (_, _, dst) -> dst :: vars + | RBload (_, _, _, dst) -> dst :: vars + | RBstore (_, _, _, _) -> vars + +(** All the nodes in the DFG have to come after the source of the basic block, and should terminate + before the sink of the basic block. After that, there should be constraints for data + dependencies between nodes. *) +let gather_bb_constraints debug bb = + let _, _, dfg = + List.fold_left accumulate_RAW_deps + (0, PTree.empty, { nodes = bb.bb_body; edges = [] }) + bb.bb_body + in + if debug then printf "DFG : %a\n" print_dfg dfg else (); + let _, dfg' = List.fold_left accumulate_WAW_deps (0, dfg) bb.bb_body in + if debug then printf "DFG': %a\n" print_dfg dfg' else (); + let _, dfg'' = List.fold_left accumulate_WAR_deps (0, dfg') bb.bb_body in + if debug then printf "DFG'': %a\n" print_dfg dfg'' else (); + let _, dfg''' = + List.fold_left accumulate_RAW_mem_deps (0, dfg'') bb.bb_body + in + if debug then printf "DFG''': %a\n" print_dfg dfg''' else (); + let _, dfg'''' = + List.fold_left accumulate_WAR_mem_deps (0, dfg''') bb.bb_body + in + if debug then printf "DFG'''': %a\n" print_dfg dfg'''' else (); + let _, dfg''''' = + List.fold_left accumulate_WAW_mem_deps (0, dfg'''') bb.bb_body + in + if debug then printf "DFG''''': %a\n" print_dfg dfg''''' else (); + match bb.bb_exit with + | None -> assert false + | Some e -> (List.length bb.bb_body, dfg''''', successors_instr e) + +let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s + +let gen_bb_name_ssrc = gen_bb_name "ssrc" + +let gen_bb_name_ssnk = gen_bb_name "ssnk" + +let gen_var_name s c i = sprintf "v%d%s_%d" (P.to_int i) s c + +let gen_var_name_b = gen_var_name "b" + +let gen_var_name_e = gen_var_name "e" + +let print_lt0 = sprintf "%s - %s <= 0;\n" + +let print_bb_order i c = if P.to_int c < P.to_int i then + print_lt0 (gen_bb_name_ssnk i) (gen_bb_name_ssrc c) else + "" + +let print_src_order i c = + print_lt0 (gen_bb_name_ssrc i) (gen_var_name_b c i) + ^ print_lt0 (gen_var_name_e c i) (gen_bb_name_ssnk i) + ^ sprintf "%s - %s = 1;\n" (gen_var_name_e c i) (gen_var_name_b c i) + +let print_src_type i c = + sprintf "int %s;\n" (gen_var_name_e c i) + ^ sprintf "int %s;\n" (gen_var_name_b c i) + +let print_data_dep_order c (i, j) = + print_lt0 (gen_var_name_e i c) (gen_var_name_b j c) + +let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr = + if List.exists (fun x -> P.eq x curr) completed then + (completed, (bvars, constraints, types)) + else + match PTree.get curr c with + | None -> assert false + | Some (num_iters, dfg, next) -> + let constraints' = + constraints + ^ String.concat "" (List.map (print_bb_order curr) next) + ^ String.concat "" + (List.map (print_src_order curr) + (List.init num_iters (fun x -> x))) + ^ String.concat "" (List.map (print_data_dep_order curr) dfg.edges) + in + let types' = + types + ^ String.concat "" + (List.map (print_src_type curr) + (List.init num_iters (fun x -> x))) + ^ sprintf "int %s;\n" (gen_bb_name_ssrc curr) + ^ sprintf "int %s;\n" (gen_bb_name_ssnk curr) + in + let bvars' = + List.append + (List.map + (fun x -> gen_var_name_b x curr) + (List.init num_iters (fun x -> x))) + bvars + in + let next' = List.filter (fun x -> P.lt x curr) next in + List.fold_left + (fun compl curr' -> gather_cfg_constraints compl c curr') + (curr :: completed, (bvars', constraints', types')) + next' + +let rec intersperse s = function + | [] -> [] + | [ a ] -> [ a ] + | x :: xs -> x :: s :: intersperse s xs + +let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] + +let parse_soln tree s = + let r = Str.regexp "v\([0-9]+\)b_\([0-9]+\)[ ]+\([0-9]+\)" in + if Str.string_match r s 0 then + IMap.update + (Str.matched_group 1 s |> int_of_string) + (update_schedule + ( Str.matched_group 2 s |> int_of_string, + Str.matched_group 3 s |> int_of_string )) + tree + else tree + +let solve_constraints vars constraints types = + let oc = open_out "lpsolve.txt" in + fprintf oc "min: "; + List.iter (fprintf oc "%s") (intersperse " + " vars); + fprintf oc ";\n"; + fprintf oc "%s" constraints; + fprintf oc "%s" types; + close_out oc; + Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") + |> drop 3 + |> List.fold_left parse_soln IMap.empty + +let find_min = function + | [] -> assert false + | l :: ls -> + let rec find_min' current = function + | [] -> current + | l' :: ls' -> + if snd l' < current then find_min' (snd l') ls' + else find_min' current ls' + in + find_min' (snd l) ls + +let find_max = function + | [] -> assert false + | l :: ls -> + let rec find_max' current = function + | [] -> current + | l' :: ls' -> + if snd l' > current then find_max' (snd l') ls' + else find_max' current ls' + in + find_max' (snd l) ls + +type registers = { reg_finish : reg; reg_return : reg; reg_stk : reg } + +let ( >>= ) = bind + +let translate_control_flow r curr_st instr = + match instr with + | RBgoto n -> + fun state -> + OK + ( (), + { + state with + st_controllogic = + PTree.set curr_st (state_goto state.st_st n) + state.st_controllogic; + } ) + | RBcond (c, rs, n1, n2) -> + translate_condition c rs >>= fun ce state -> + OK + ( (), + { + state with + st_controllogic = + PTree.set curr_st + (state_cond state.st_st ce n1 n2) + state.st_controllogic; + } ) + | RBreturn ret -> ( + let new_state state = state.st_freshstate in + match ret with + | None -> + let fin = + Vseq + ( HTLgen.block r.reg_finish + (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))), + HTLgen.block r.reg_return + (Vlit (ValueInt.coq_ZToValue (Z.of_uint 0))) ) + in + fun state -> + OK + ( (), + { + state with + st_datapath = + PTree.set (new_state state) fin state.st_datapath; + st_controllogic = + PTree.set curr_st + (state_goto state.st_st (new_state state)) + state.st_controllogic; + st_freshstate = P.succ state.st_freshstate; + } ) + | Some ret' -> + let fin = + Vseq + ( HTLgen.block r.reg_finish + (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))), + HTLgen.block r.reg_return (Vvar ret') ) + in + fun state -> + OK + ( (), + { + state with + st_datapath = + PTree.set (new_state state) fin state.st_datapath; + st_controllogic = + PTree.set curr_st + (state_goto state.st_st (new_state state)) + state.st_controllogic; + st_freshstate = P.succ state.st_freshstate; + } ) ) + | RBjumptable (r, tbl) -> + fun state -> + OK ( (), + { + state with + st_controllogic = PTree.set curr_st (Vcase (Vvar r, HTLgen.tbl_to_case_expr state.st_st tbl, Some Vskip)) state.st_controllogic + }) + | _ -> + error + (Errors.msg + (coqstring_of_camlstring + "Control flow instructions not implemented.")) + +let translate_instr r curr_st instr = + let prev_instr state = + match PTree.get curr_st state.st_datapath with None -> Vskip | Some v -> v + in + match instr with + | RBnop -> + fun state -> + OK + ( (), + { + state with + st_datapath = + PTree.set curr_st (prev_instr state) state.st_datapath; + } ) + | RBop (op, rs, dst) -> + translate_instr op rs >>= fun instr -> + declare_reg None dst (Nat.of_int 32) >>= fun _ state -> + let stmnt = Vseq (prev_instr state, nonblock dst instr) in + OK + ( (), + { state with st_datapath = PTree.set curr_st stmnt state.st_datapath } + ) + | RBload (mem, addr, rs, dst) -> + translate_arr_access mem addr rs r.reg_stk >>= fun src -> + declare_reg None dst (Nat.of_int 32) >>= fun _ state -> + let stmnt = Vseq (prev_instr state, nonblock dst src) in + OK + ( (), + { state with st_datapath = PTree.set curr_st stmnt state.st_datapath } + ) + | RBstore (mem, addr, rs, src) -> + translate_arr_access mem addr rs r.reg_stk >>= fun dst state -> + OK + ( (), + { + state with + st_datapath = + PTree.set curr_st + (Vseq (prev_instr state, Vnonblock (dst, Vvar src))) + state.st_datapath; + } ) + +let combine_bb_schedule schedule s = + let i, st = s in + IMap.update st (update_schedule i) schedule + +let add_schedules r bb_body min_sched curr ischedule = + let i, schedule = ischedule in + let curr_state = curr - i + min_sched in + let instrs = List.map (List.nth bb_body) schedule in + if curr_state = 20 then printf "HII: curr_state: %d : curr: %d\n" curr_state curr; + collectlist (translate_instr r (P.of_int curr_state)) instrs >>= fun _ -> + translate_control_flow r (P.of_int curr_state) + (RBgoto (curr_state - 1 |> P.of_int)) + +(** Should generate the [HTL] code based on the input [RTLBlock] description. *) +let transf_htl r c (schedule : (int * int) list IMap.t) = + let f bbs = + let i, bb = bbs in + match bb with + | { bb_body = []; bb_exit = Some c } -> translate_control_flow r i c + | { bb_body = bb_body'; bb_exit = Some ctrl_flow } -> + let i_sched = + try IMap.find (P.to_int i) schedule + with Not_found -> ( + printf "Could not find %d\n" (P.to_int i); + IMap.iter + (fun d -> printf "%d: %a\n" d (print_list print_tuple)) + schedule; + assert false + ) + in + let min_state = find_min i_sched in + let max_state = find_max i_sched in + let i_sched_tree = + List.fold_left combine_bb_schedule IMap.empty i_sched + in + collectlist + (add_schedules r bb_body' min_state (P.to_int i)) + (IMap.to_seq i_sched_tree |> List.of_seq) + >>= fun _ -> + printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1); + printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i); + (match ctrl_flow with + | RBgoto _ -> + translate_control_flow r (P.of_int (P.to_int i - max_state + min_state)) ctrl_flow + | _ -> + translate_control_flow r (P.of_int (P.to_int i - max_state + min_state - 1)) ctrl_flow) + | _ -> + coqstring_of_camlstring "Illegal state reached in scheduler" + |> Errors.msg |> error + in + collectlist f c + +let second = function (_, a, _) -> a + +let schedule entry r (c : code) = + let debug = true in + let c' = PTree.map1 (gather_bb_constraints false) c in + let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in + let _, (vars, constraints, types) = + gather_cfg_constraints ([], ([], "", "")) c' entry + in + let schedule' = solve_constraints vars constraints types in + IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule'; + (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) + transf_htl r (PTree.elements c) schedule' + +let transl_module' (f : RTLBlock.coq_function) : HTL.coq_module mon = + create_reg (Some Voutput) (Nat.of_int 1) >>= fun fin -> + create_reg (Some Voutput) (Nat.of_int 32) >>= fun rtrn -> + create_arr None (Nat.of_int 32) (Nat.of_int (Z.to_int f.fn_stacksize / 4)) + >>= fun stack_var -> + let stack, stack_len = stack_var in + schedule f.fn_entrypoint + { reg_finish = fin; reg_return = rtrn; reg_stk = stack } + f.fn_code + >>= fun _ -> + collectlist (fun r -> declare_reg (Some Vinput) r (Nat.of_int 32)) f.fn_params + >>= fun _ -> + create_reg (Some Vinput) (Nat.of_int 1) >>= fun start -> + create_reg (Some Vinput) (Nat.of_int 1) >>= fun rst -> + create_reg (Some Vinput) (Nat.of_int 1) >>= fun clk current_state -> + let m = + { + HTL.mod_params = f.fn_params; + HTL.mod_datapath = current_state.st_datapath; + HTL.mod_controllogic = current_state.st_controllogic; + HTL.mod_entrypoint = f.fn_entrypoint; + HTL.mod_st = current_state.st_st; + HTL.mod_stk = stack; + HTL.mod_stk_len = stack_len; + HTL.mod_finish = fin; + HTL.mod_return = rtrn; + HTL.mod_start = start; + HTL.mod_reset = rst; + HTL.mod_clk = clk; + HTL.mod_scldecls = current_state.st_scldecls; + HTL.mod_arrdecls = current_state.st_arrdecls; + } + in + OK (m, current_state) + +let max_state f = + let st = P.of_int 10000 in + { + (init_state st) with + st_st = st; + st_freshreg = P.succ st; + st_freshstate = P.of_int 10000; + st_scldecls = + AssocMap.AssocMap.set st (None, Nat.of_int 32) (init_state st).st_scldecls; + } + +let transl_module (f : RTLBlock.coq_function) : HTL.coq_module Errors.res = + run_mon (max_state f) (transl_module' f) diff --git a/src/verilog/Value.v b/src/hls/Value.v index d6a3d8b..d6a3d8b 100644 --- a/src/verilog/Value.v +++ b/src/hls/Value.v diff --git a/src/verilog/ValueInt.v b/src/hls/ValueInt.v index f1fd056..f1fd056 100644 --- a/src/verilog/ValueInt.v +++ b/src/hls/ValueInt.v diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v new file mode 100644 index 0000000..b882dc6 --- /dev/null +++ b/src/hls/ValueVal.v @@ -0,0 +1,209 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +(* begin hide *) +From bbv Require Import Word. +From bbv Require HexNotation WordScope. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. +From compcert Require Export lib.Integers common.Values. +From vericert Require Import Vericertlib. +(* end hide *) + +(** * Value + +A [value] is a bitvector with a specific size. We are using the implementation +of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. +However, we need to wrap it with an [Inductive] so that we can specify and match +on the size of the [value]. This is necessary so that we can easily store +[value]s of different sizes in a list or in a map. + +Using the default [word], this would not be possible, as the size is part of the type. *) + +(* Definition value : Type := val. + +(** ** Value conversions + +Various conversions to different number types such as [N], [Z], [positive] and +[int], where the last one is a theory of integers of powers of 2 in CompCert. *) + +Definition valueToNat (v : value) : nat := + match v with + | value_bool b => Nat.b2n b + | value_int i => Z.to_nat (Int.unsigned i) + | value_int64 i => Z.to_nat (Int64.unsigned i) + end. + +Definition natToValue (n : nat) : value := + value_int (Int.repr (Z.of_nat n)). + +Definition natToValue64 (n : nat) : value := + value_int64 (Int64.repr (Z.of_nat n)). + +Definition valueToN (v : value) : N := + match v with + | value_bool b => N.b2n b + | value_int i => Z.to_N (Int.unsigned i) + | value_int64 i => Z.to_N (Int64.unsigned i) + end. + +Definition NToValue (n : N) : value := + value_int (Int.repr (Z.of_N n)). + +Definition NToValue64 (n : N) : value := + value_int64 (Int64.repr (Z.of_N n)). + +Definition ZToValue (z : Z) : value := + value_int (Int.repr z). + +Definition ZToValue64 (z : Z) : value := + value_int64 (Int64.repr z). + +Definition valueToZ (v : value) : Z := + match v with + | value_bool b => Z.b2z b + | value_int i => Int.signed i + | value_int64 i => Int64.signed i + end. + +Definition uvalueToZ (v : value) : Z := + match v with + | value_bool b => Z.b2z b + | value_int i => Int.unsigned i + | value_int64 i => Int64.unsigned i + end. + +Definition posToValue (p : positive) : value := + value_int (Int.repr (Z.pos p)). + +Definition posToValue64 (p : positive) : value := + value_int64 (Int64.repr (Z.pos p)). + +Definition valueToPos (v : value) : positive := + match v with + | value_bool b => 1%positive + | value_int i => Z.to_pos (Int.unsigned i) + | value_int64 i => Z.to_pos (Int64.unsigned i) + end. + +Definition intToValue (i : Integers.int) : value := value_int i. + +Definition int64ToValue (i : Integers.int64) : value := value_int64 i. + +Definition valueToInt (v : value) : Integers.int := + match v with + | value_bool b => Int.repr (if b then 1 else 0) + | value_int i => i + | value_int64 i => Int.repr (Int64.unsigned i) + end. + +(*Definition ptrToValue (i : ptrofs) : value := + value_int (Ptrofs.to_int i). + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.of_int i. + +Definition valToValue (v : Values.val) : option value := + match v with + | Values.Vint i => Some (intToValue i) + | Values.Vint64 i => Some (intToValue i) + | Values.Vptr b off => Some (ptrToValue off) + | Values.Vundef => Some (ZToValue 0%Z) + | _ => None + end. + +(** Convert a [value] to a [bool], so that choices can be made based on the +result. This is also because comparison operators will give back [value] instead +of [bool], so if they are in a condition, they will have to be converted before +they can be used. *) + +Definition valueToBool (v : value) : bool := + if Z.eqb (uvalueToZ v) 0 then false else true. + +Definition boolToValue (b : bool) : value := + natToValue (if b then 1 else 0). + +(** ** Arithmetic operations *) + +Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +intros; subst; assumption. Defined. + +Lemma unify_word_unfold : + forall sz w, + unify_word sz sz w eq_refl = w. +Proof. auto. Qed. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + i = valueToInt v' -> + val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = valueToPtr v' -> + val_value_lessdef (Vptr b off) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. + +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + +Lemma valueToZ_ZToValue : + forall z, + (Int.min_signed <= z <= Int.max_signed)%Z -> + valueToZ (ZToValue z) = z. +Proof. auto using Int.signed_repr. Qed. + +Lemma uvalueToZ_ZToValue : + forall z, + (0 <= z <= Int.max_unsigned)%Z -> + uvalueToZ (ZToValue z) = z. +Proof. auto using Int.unsigned_repr. Qed. + +Lemma valueToPos_posToValue : + forall v, + 0 <= Z.pos v <= Int.max_unsigned -> + valueToPos (posToValue v) = v. +Proof. + unfold valueToPos, posToValue. + intros. rewrite Int.unsigned_repr. + apply Pos2Z.id. assumption. +Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. auto. Qed. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' -> + val_value_lessdef v v'. +Proof. + intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + unfold valueToInt. unfold intToValue in H1. auto. + inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. +Qed. + +Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, + ptrToValue in *) + +(*Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.*) +*) diff --git a/src/verilog/Verilog.v b/src/hls/Verilog.v index 3b0dd0a..e5f86d5 100644 --- a/src/verilog/Verilog.v +++ b/src/hls/Verilog.v @@ -29,7 +29,7 @@ Require Import Lia. Import ListNotations. -From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array. +From vericert Require Import Vericertlib Show ValueInt AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. @@ -149,7 +149,7 @@ Inductive binop : Type := (** ** Unary Operators *) Inductive unop : Type := -| Vneg (** negation ([~]) *) +| Vneg (** negation ([-]) *) | Vnot. (** not operation [!] *) (** ** Expressions *) diff --git a/src/translation/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..a0be0fa 100644 --- a/src/translation/Veriloggen.v +++ b/src/hls/Veriloggen.v diff --git a/src/translation/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..9abbd4b 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v diff --git a/test/array.c b/test/array.c index 7d78a61..0f23cc8 100644 --- a/test/array.c +++ b/test/array.c @@ -1,7 +1,7 @@ int main() { int x[3] = {1, 2, 3}; - int sum = 0, incr = 1; - for (int i = 0; i < 3; i=i+incr) - sum += x[i]; + int sum = 0; + for (int i = 0; i < 3; i++) + sum = x[i]; return sum; } diff --git a/test/loop.c b/test/loop.c index 52e4fe9..bece7f2 100644 --- a/test/loop.c +++ b/test/loop.c @@ -1,10 +1,9 @@ int main() { int max = 5; int acc = 0; - int b = 1; int c = 2; - for (int i = 0; i < max; i = i + b) { + for (int i = 0; i < max; i++) { acc += i; } diff --git a/test/test_all.sh b/test/test_all.sh index d43e2ac..92d3967 100755 --- a/test/test_all.sh +++ b/test/test_all.sh @@ -27,10 +27,14 @@ echo "--------------------------------------------------" for cfile in $test_dir/*.c; do echo "Testing $cfile" outbase=$mytmpdir/$(basename $cfile) - gcc -o $outbase.gcc $cfile + gcc -o $outbase.gcc $cfile >/dev/null 2>&1 $outbase.gcc expected=$? - ./bin/vericert -drtl -o $outbase.v $cfile + ./bin/vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1 + if [[ ! -f $outbase.v ]]; then + echo "ERROR" + continue + fi iverilog -o $outbase.iverilog $outbase.v actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/') if [[ $expected = $actual ]]; then |