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/translation/Veriloggen.v | 65 -------------------------------------------- 1 file changed, 65 deletions(-) delete mode 100644 src/translation/Veriloggen.v (limited to 'src/translation/Veriloggen.v') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v deleted file mode 100644 index a0be0fa..0000000 --- a/src/translation/Veriloggen.v +++ /dev/null @@ -1,65 +0,0 @@ -(* - * 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