From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/hls/Veriloggen.v | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 src/hls/Veriloggen.v (limited to 'src/hls/Veriloggen.v') diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v new file mode 100644 index 0000000..a0be0fa --- /dev/null +++ b/src/hls/Veriloggen.v @@ -0,0 +1,65 @@ +(* + * Vericert: 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 compcert Require Import Maps. +From compcert Require Errors. +From compcert Require Import AST. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. + +Definition transl_list_fun (a : node * Verilog.stmnt) := + let (n, stmnt) := a in + (Vlit (posToValue n), stmnt). + +Definition transl_list st := map transl_list_fun st. + +Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := + match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. + +Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. + +Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := + match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. + +Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. + +Definition transl_module (m : HTL.module) : Verilog.module := + let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in + let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in + let body := + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) + (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + Verilog.mkmodule m.(mod_start) + m.(mod_reset) + m.(mod_clk) + m.(mod_finish) + m.(mod_return) + m.(mod_st) + m.(mod_stk) + m.(mod_stk_len) + m.(mod_params) + body + m.(mod_entrypoint). + +Definition transl_fundef := transf_fundef transl_module. + +Definition transl_program (p: HTL.program) : Verilog.program := + transform_program transl_fundef p. -- cgit