From 3d3f165bc97774c8d6b9bcbea9e06daf688e617d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:36:18 +0100 Subject: Generate Verilog from HTL --- src/verilog/Verilog.v | 183 +++++++++++++++++++++++++++++++------------------- 1 file changed, 114 insertions(+), 69 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 845d706..b4b2f00 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -87,6 +87,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). +Inductive scl_decl : Type := Scalar (sz : nat). +Inductive arr_decl : Type := Array (sz : nat) (ln : nat). (** * Verilog AST @@ -181,9 +183,17 @@ Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). The declarations are always register declarations as combinational logic can be done using combinational always block instead of continuous assignments. *) +Inductive io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. + +Inductive declaration : Type := +| Vdecl : option io -> reg -> nat -> declaration +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. + Inductive module_item : Type := -| Vdecl : reg -> nat -> module_item -| Vdeclarr : reg -> nat -> nat -> module_item +| Vdeclaration : declaration -> module_item | Valways : edge -> stmnt -> module_item | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. @@ -200,15 +210,22 @@ Inductive module_item : Type := *) Record module : Type := mkmodule { - mod_start : szreg; - mod_reset : szreg; - mod_clk : szreg; - mod_finish : szreg; - mod_return : szreg; - mod_state : szreg; (**r Variable that defines the current state, it should be internal. *) - mod_args : list szreg; + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_st : reg; (**r Variable that defines the current state, it should be internal. *) + mod_stk : reg; + mod_args : list reg; mod_body : list module_item; - }. + mod_entrypoint : node; +}. + +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := @@ -241,18 +258,28 @@ retrieved and set appropriately. which determines which part of the Verilog is executed. This is then the part of the Verilog that should match with the RTL. *) +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (assoc : assocmap), + stackframe. + Inductive state : Type := -| State: - forall (m : module) - (assoc : reg_associations) - (assoc : arr_associations) - (f : fextclk) - (cycle : nat) - (stvar : value), - state -| Finishstate: - forall v : value, - state. +| State : + forall (stack : list stackframe) + (m : module) + (st : node) + (reg_assoc : assocmap) + (arr_assoc : AssocMap.t (list value)), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := match op with @@ -383,14 +410,14 @@ Definition access_fext (f : fext) (r : reg) : res value := (** Return the location of the lhs of an assignment. *) Inductive location : Type := -| Reg (_ : reg) -| Array (_ : reg) (_ : nat). +| LocReg (_ : reg) +| LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := -| Base : forall f asr asa r, location_is f asr asa (Vvar r) (Reg r) +| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) | Indexed : forall f asr asa r iexp iv, expr_runp f asr asa iexp iv -> - location_is f asr asa (Vvari r iexp) (Array r (valueToNat iv)). + location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). (* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) (* match e with *) @@ -508,28 +535,28 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 | stmnt_runp_Vblock_reg: forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) (block_reg r asr rhsval) asa | stmnt_runp_Vnonblock_reg: forall lhs r rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) (nonblock_reg r asr rhsval) asa | stmnt_runp_Vblock_arr: forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) asr (block_arr r i asa rhsval) | stmnt_runp_Vnonblock_arr: forall lhs r i rhs rhsval asr asa f, - location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) -> + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) @@ -565,8 +592,8 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 | mi_stepp_Vdecl : - forall f sr sa lhs rhs, - mi_stepp f sr sa (Vdecl lhs rhs) sr sa. + forall f sr sa lhs rhs io, + mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa. Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> @@ -607,8 +634,8 @@ other arguments to the module are also to be supported. *) Definition initial_fextclk (m : module) : fextclk := fun x => match x with - | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap) - | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap) + | S O => (AssocMap.set (mod_reset m) (ZToValue 1 1) empty_assocmap) + | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap) end. (*Definition module_run (n : nat) (m : module) : res assocmap := @@ -655,42 +682,60 @@ Qed. *) -Definition genv := Genv.t unit unit. - -Inductive step : state -> state -> Prop := -| step_module : - forall m stvar stvar' cycle f - asr0 asa0 asr1 asa1 - asr' asa', - mis_stepp (f cycle) asr0 asa0 - m.(mod_body) asr1 asa1 -> - asr' = merge_associations asr1 -> - asa' = merge_associations asa1 -> - Some stvar' = asr'.(assoc_blocking)!(fst m.(mod_state)) -> - step (State m asr0 asa0 f cycle stvar) - (State m asr' asa' f (S cycle) stvar') +Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') + | _, _ => empty_assocmap + end. + +Definition genv := Globalenvs.Genv.t fundef unit. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := + | step_module : + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g, + mis_stepp f (mkassociations asr empty_assocmap) + (mkassociations asa (AssocMap.empty (list value))) + m.(mod_body) + (mkassociations basr1 nasr1) + (mkassociations basa1 nasa1)-> + asr' = merge_assocmap nasr1 basr1 -> + asa' = AssocMapExt.merge (list value) nasa1 basa1 -> + asr'!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : - forall m asr asa f cycle stvar result, - asr.(assoc_blocking)!(fst m.(mod_finish)) = Some (1'h"1") -> - asr.(assoc_blocking)!(fst m.(mod_return)) = Some result -> - step (State m asr asa f cycle stvar) - (Finishstate result). + forall asr asa sf retval m st g, + asr!(m.(mod_finish)) = Some (1'h"1") -> + asr!(m.(mod_return)) = Some retval -> + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g res m args, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint)) + (init_params args m.(mod_args))) + (AssocMap.empty (list value))) +| step_return : + forall g m asr i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) + (AssocMap.empty (list value))). Hint Constructors step : verilog. -(*Inductive initial_state (m: module): state -> Prop := -| initial_state_intro: - forall hmi tmi, - hmi::tmi = mod_body m -> - initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH). - -(** A final state is a [Returnstate] with an empty call stack. *) - -Inductive final_state: state -> Integers.int -> Prop := - | final_state_intro: forall v, - final_state (Finishstate v) (valueToInt v). - -(** The small-step semantics for a module. *) - -Definition semantics (p: module) := - Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil). -*) +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + initial_state p (Callstate nil m nil). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + retvali = valueToInt retval -> + final_state (Returnstate nil retval) retvali. + +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). -- cgit From 5355eb2e4346043d8a4ea4cb574a5b47b5a3a1f3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:36:36 +0100 Subject: Remove Test.v --- src/verilog/Test.v | 99 ------------------------------------------------------ 1 file changed, 99 deletions(-) delete mode 100644 src/verilog/Test.v (limited to 'src/verilog') diff --git a/src/verilog/Test.v b/src/verilog/Test.v deleted file mode 100644 index 90c5312..0000000 --- a/src/verilog/Test.v +++ /dev/null @@ -1,99 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz - * - * 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 . - *) - -From coqup Require Import Verilog Veriloggen Coquplib Value. -From compcert Require Import AST Errors Maps Op Integers. -From compcert Require RTL. -From Coq Require Import FSets.FMapPositive. -From bbv Require Import Word. -Import ListNotations. -Import HexNotationValue. -Import WordScope. - -Local Open Scope word_scope. - -Definition test_module : module := - let mods := [ - Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5))) - (Vnonblock (Vvar 7%positive) - (Vvar 6%positive))) - ] in - mkmodule (1%positive, 1%nat) - (2%positive, 1%nat) - (3%positive, 1%nat) - (4%positive, 1%nat) - (5%positive, 32%nat) - (6%positive, 32%nat) - nil - mods. - -Definition test_input : RTL.function := - let sig := mksignature nil Tvoid cc_default in - let params := nil in - let stacksize := 0 in - let entrypoint := 3%positive in - let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive)) - (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive) - (PTree.empty RTL.instruction)) in - RTL.mkfunction sig params stacksize code entrypoint. - -Definition test_input_program : RTL.program := - mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive. - -Compute transf_program test_input_program. - -Definition test_output_module : module := - {| mod_start := (4%positive, 1%nat); - mod_reset := (5%positive, 1%nat); - mod_clk := (6%positive, 1%nat); - mod_finish := (2%positive, 1%nat); - mod_return := (3%positive, 32%nat); - mod_state := (7%positive, 32%nat); - mod_args := []; - mod_body := - [Valways_ff (Vposedge 6%positive) - (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1")) - (Vnonblock (Vvar 7%positive) (32'h"3")) - (Vcase (Vvar 7%positive) - [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1")); - (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))] - (Some Vskip))); - Valways_ff (Vposedge 6%positive) - (Vcase (Vvar 7%positive) - [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1"))) - (Vblock (Vvar 3%positive) (Vvar 1%positive))); - (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))] - (Some Vskip)); - Vdecl 1%positive 32; Vdecl 7%positive 32] |}. - -Lemma valid_test_output : - transf_program test_input_program = OK test_output_module. -Proof. trivial. Qed. - -Definition test_fextclk := initial_fextclk test_output_module. - -Lemma manual_simulation : - step (State test_output_module empty_assocmap empty_assocmap - test_fextclk 1 (32'h"1")) - (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap) - empty_assocmap test_fextclk 2 (32'h"3")). -Proof. - repeat (econstructor; eauto); - try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); - apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat. -Qed. -- cgit From 7ad63f341fe3c28ef20bfde755bdf21403077504 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:38:14 +0100 Subject: Remove Verilog proofs --- src/verilog/HTL.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/verilog') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 2e4ef1a..c07d672 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -47,7 +47,12 @@ Record module: Type := mod_st : reg; mod_stk : reg; mod_finish : reg; - mod_return : reg + mod_return : reg; + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); + mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); }. Definition fundef := AST.fundef module. -- cgit From d4a2e1ced4deabe9be6b32919cc4c1499751c433 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 11:38:28 +0100 Subject: Fix printing of Verilog with new datatypes --- src/verilog/PrintVerilog.ml | 42 ++++++++++++++++++++++++++---------------- src/verilog/PrintVerilog.mli | 2 +- 2 files changed, 27 insertions(+), 17 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index bdd8581..d81bf18 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -21,6 +21,7 @@ open Value open Datatypes open Camlcoq +open AST open Printf @@ -107,21 +108,30 @@ let pprint_edge_top i = function | Valledge -> "@*" | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] -let declare i t = +let declare t = function (r, sz) -> - concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; ";\n" ] -let declarearr i t = +let declarearr t = function (r, sz, ln) -> - concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] +let print_io = function + | Some Vinput -> "input" + | Some Voutput -> "output reg" + | Some Vinout -> "inout" + | None -> "reg" + +let decl i = function + | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] + | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] + (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function - | Vdecl (r, sz) -> declare i "reg" (r, sz) - | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln) + | Vdeclaration d -> decl i d | Valways (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] | Valways_ff (e, s) -> @@ -138,10 +148,6 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"] let compose f g x = g x |> f -let init_inputs i r = declare i "input" r - -let init_outputs i r = declare i "output reg" r - let testbench = "module testbench; reg start, reset, clk; wire finish; @@ -171,17 +177,13 @@ endmodule 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 (compose register fst) (inputs @ outputs))); ");\n"; - fold_map (init_inputs (i+1)) inputs; - fold_map (init_outputs (i+1)) outputs; + concat [ indent i; "module "; (extern_atom n); + "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; indent i; "endmodule\n\n"; testbench ] -let print_program pp v = pstr pp (pprint_module 0 "main" v) - let print_result pp lst = let rec print_result_in pp = function | [] -> fprintf pp "]\n" @@ -192,3 +194,11 @@ let print_result pp lst = print_result_in pp lst let print_value pp v = fprintf pp "%s" (literal v) + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> pstr pp (pprint_module 0 id f) + | _ -> () + +let print_program pp prog = + List.iter (print_globdef pp) prog.prog_defs diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index c9fca8e..0df9d06 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,6 +18,6 @@ val print_value : out_channel -> Value.value -> unit -val print_program : out_channel -> Verilog.coq_module -> unit +val print_program : out_channel -> Verilog.program -> unit val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit -- cgit From 0f9ab38389000edfa2376fabace69d2366d32647 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 13:18:40 +0100 Subject: Fix declaring function arguments correctly --- src/verilog/PrintVerilog.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index d81bf18..700b8e3 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -180,8 +180,7 @@ let pprint_module i n m = concat [ indent i; "module "; (extern_atom n); "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; - indent i; "endmodule\n\n"; - testbench + indent i; "endmodule\n\n" ] let print_result pp lst = @@ -201,4 +200,5 @@ let print_globdef pp (id, gd) = | _ -> () let print_program pp prog = - List.iter (print_globdef pp) prog.prog_defs + List.iter (print_globdef pp) prog.prog_defs; + pstr pp testbench -- cgit