From 981b6238573548b696d0a4a50eb7605387245c0b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 1 Apr 2020 19:24:29 +0100 Subject: Update compilation --- src/Compiler.v | 4 ++-- src/extraction/Extraction.v | 2 +- src/verilog/PrintVerilog.ml | 52 +++++++++++++++++++++++++++++++++++++------- src/verilog/PrintVerilog.mli | 2 +- src/verilog/Verilog.v | 41 +++++++++++++++++++++++++++++----- 5 files changed, 84 insertions(+), 17 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index 7a88839..5b4ef0a 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -74,7 +74,7 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. -Definition transf_backend (r : RTL.program) : res Verilog.verilog := +Definition transf_backend (r : RTL.program) : res Verilog.module := OK r @@@ Veriloggen.transf_program. @@ -88,7 +88,7 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program := @@@ RTLgen.transl_program @@ print (print_RTL 0). -Definition transf_hls (p : Csyntax.program) : res Verilog.verilog := +Definition transf_hls (p : Csyntax.program) : res Verilog.module := OK p @@@ transf_frontend @@@ transf_backend. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 4403019..c7ebf8e 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -166,7 +166,7 @@ Set Extraction AccessOpaque. Cd "src/Extraction". Separate Extraction - Verilog.verilog Verilog.valueToZ coqup.Compiler.transf_hls + Verilog.module Verilog.valueToZ coqup.Compiler.transf_hls Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 04a35de..5199872 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -53,13 +53,13 @@ let unop = function | Vneg -> " ~ " | Vnot -> " ! " -let register a = P.to_int a +let register a = sprintf "reg_%d" (P.to_int a) let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) let rec pprint_expr = function | Vlit l -> literal l - | Vvar s -> sprintf "reg_%d" (register s) + | Vvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] @@ -69,12 +69,48 @@ let rec pprint_stmnt i = in function | Vskip -> concat [indent i; ";\n"] | Vseq s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"] - | Vcond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n"; - pprint_stmnt (i + 1) st; indent i; "else\n"; - pprint_stmnt (i + 1) sf] - | Vcase (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case es; indent i; "endcase\n"] + | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ")\n"; + pprint_stmnt (i + 1) st; indent i; "else\n"; + pprint_stmnt (i + 1) sf + ] + | Vcase (e, es) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; + fold_map pprint_case es; indent (i+1); "default:;\n"; + indent i; "endcase\n" + ] | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] -let print_program pp v = pstr pp (fold_map (pprint_stmnt 0) v) +let rec pprint_edge = function + | Vposedge r -> concat ["posedge "; register r] + | Vnegedge r -> concat ["negedge "; register r] + | Valledge -> "*" + | Voredge (e1, e2) -> concat [pprint_edge e1; " or "; pprint_edge e2] + +let pprint_edge_top i = function + | Vposedge r -> concat ["@(posedge "; register r; ")"] + | Vnegedge r -> concat ["@(negedge "; register r; ")"] + | Valledge -> "@*" + | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] + +let pprint_module_item i = function + | Vdecl (r, n, e) -> + concat [indent i; "reg ["; sprintf "%d" (Nat.to_int n - 1); ":0] "; register r; " = "; pprint_expr e; ";\n"] + | Valways (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + +let make_io i io r = concat [indent i; io; " "; register r; ";\n"] + +let pprint_module i n m = + let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in + let outputs = [m.mod_finish; m.mod_return] in + concat [ indent i; "module "; n; "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; + fold_map (make_io (i+1) "input") inputs; fold_map (make_io (i+1) "output") outputs; + fold_map (pprint_module_item (i+1)) m.mod_body; indent i; "endmodule\n" + ] + +let print_program pp v = pstr pp (pprint_module 0 "main" v) diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 4197d4a..181a9d2 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -16,4 +16,4 @@ * along with this program. If not, see . *) -val print_program : out_channel -> Verilog.verilog -> unit +val print_program : out_channel -> Verilog.coq_module -> unit diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index e91ca2d..212dbc0 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -39,9 +39,12 @@ Record value : Type := mkvalue { }. Definition posToValue (p : positive) : value := - let size := Z.to_nat (log_sup p) in + let size := Z.to_nat (Z.succ (log_inf p)) in mkvalue size (Word.posToWord size p). +Definition ZToValue (s : nat) (z : Z) : value := + mkvalue s (Word.ZToWord s z). + Definition intToValue (i : Integers.int) : value := mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)). @@ -94,13 +97,41 @@ Inductive stmnt : Type := | Vcond : expr -> stmnt -> stmnt -> stmnt | Vcase : expr -> list (expr * stmnt) -> stmnt | Vblock : expr -> expr -> stmnt -| Vnonblock : expr -> expr -> stmnt -| Vdecl : reg -> nat -> expr -> stmnt. +| Vnonblock : expr -> expr -> stmnt. + +(** [edge] is not part of [stmnt] in this formalisation because is closer to the + semantics that are used. *) +Inductive edge : Type := +| Vposedge : reg -> edge +| Vnegedge : reg -> edge +| Valledge : edge +| Voredge : edge -> edge -> edge. + +Inductive module_item : Type := +| Vdecl : reg -> nat -> expr -> module_item +| Valways : edge -> stmnt -> module_item. + +(** [mod_start] If set, starts the computations in the module. *) +(** [mod_reset] If set, reset the state in the module. *) +(** [mod_clk] The clock that controls the computation in the module. *) +(** [mod_args] The arguments to the module. *) +(** [mod_finish] Bit that is set if the result is ready. *) +(** [mod_return] The return value that was computed. *) +(** [mod_body] The body of the module, including the state machine. *) +Record module : Type := mkmodule { + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_args : list reg; + mod_body : list module_item; +}. +(** Convert a [positive] to an expression directly, setting it to the right + size. *) Definition posToLit (p : positive) : expr := Vlit (posToValue p). -Definition verilog : Type := list stmnt. - Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -- cgit