diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-07-29 13:49:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-29 13:49:03 +0100 |
commit | 502e49e2f8c95b40cd0761cbb69c863904169f8b (patch) | |
tree | e417f9a1d17f84a25ecd00be1ccb9cdda8b8e6ea /src/hls/DVeriloggen.v | |
parent | 93117b6e766c25c5aeecdc20a963d5114fb91e59 (diff) | |
download | vericert-502e49e2f8c95b40cd0761cbb69c863904169f8b.tar.gz vericert-502e49e2f8c95b40cd0761cbb69c863904169f8b.zip |
Add beginning to memory generation proof
Diffstat (limited to 'src/hls/DVeriloggen.v')
-rw-r--r-- | src/hls/DVeriloggen.v | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/src/hls/DVeriloggen.v b/src/hls/DVeriloggen.v new file mode 100644 index 0000000..3f8a0b7 --- /dev/null +++ b/src/hls/DVeriloggen.v @@ -0,0 +1,101 @@ +(* + * 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 compcert.common.AST. +Require compcert.common.Errors. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.DHTL. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. + +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 inst_ram clk ram := + Valways (Vnegedge clk) + (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) + (Vseq (Vcond (Vvar (ram_wr_en ram)) + (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) + (Vvar (ram_d_in ram))) + (Vnonblock (Vvar (ram_d_out ram)) + (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) + (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) + Vskip). + +Definition transl_module (m : DHTL.module) : Verilog.module := + let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in + match m.(DHTL.mod_ram) with + | Some ram => + let body := + Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(DHTL.mod_st)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) +(Vcase (Vvar m.(DHTL.mod_st)) case_el_data (Some Vskip))) + :: inst_ram m.(DHTL.mod_clk) ram + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + Verilog.mkmodule m.(DHTL.mod_start) + m.(DHTL.mod_reset) + m.(DHTL.mod_clk) + m.(DHTL.mod_finish) + m.(DHTL.mod_return) + m.(DHTL.mod_st) + m.(DHTL.mod_stk) + m.(DHTL.mod_stk_len) + m.(DHTL.mod_params) + body + m.(DHTL.mod_entrypoint) + | None => + let body := + Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(DHTL.mod_st)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) +(Vcase (Vvar m.(DHTL.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.(DHTL.mod_start) + m.(DHTL.mod_reset) + m.(DHTL.mod_clk) + m.(DHTL.mod_finish) + m.(DHTL.mod_return) + m.(DHTL.mod_st) + m.(DHTL.mod_stk) + m.(DHTL.mod_stk_len) + m.(DHTL.mod_params) + body + m.(DHTL.mod_entrypoint) + end. + +Definition transl_fundef := transf_fundef transl_module. + +Definition transl_program (p: DHTL.program) : Verilog.program := + transform_program transl_fundef p. |