diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-30 14:03:40 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-30 14:03:40 +0100 |
commit | ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a (patch) | |
tree | aba30758bbbf10ab3d975367f48a695b81afb179 | |
parent | 9d6979baa0e4b505862bcedee1dfd075f36579c3 (diff) | |
download | vericert-kvx-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.tar.gz vericert-kvx-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.zip |
Add RTLBlock intermediate language
-rw-r--r-- | Makefile | 7 | ||||
-rw-r--r-- | _CoqProject | 3 | ||||
-rw-r--r-- | default.nix | 2 | ||||
-rw-r--r-- | shell.nix | 4 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 9 | ||||
-rw-r--r-- | src/hls/Array.v (renamed from src/verilog/Array.v) | 0 | ||||
-rw-r--r-- | src/hls/AssocMap.v (renamed from src/verilog/AssocMap.v) | 0 | ||||
-rw-r--r-- | src/hls/HTL.v (renamed from src/verilog/HTL.v) | 0 | ||||
-rw-r--r-- | src/hls/HTLgen.v (renamed from src/translation/HTLgen.v) | 0 | ||||
-rw-r--r-- | src/hls/HTLgenproof.v (renamed from src/translation/HTLgenproof.v) | 2 | ||||
-rw-r--r-- | src/hls/HTLgenspec.v (renamed from src/translation/HTLgenspec.v) | 0 | ||||
-rw-r--r-- | src/hls/Partition.ml | 60 | ||||
-rw-r--r-- | src/hls/PrintHTL.ml (renamed from src/verilog/PrintHTL.ml) | 0 | ||||
-rw-r--r-- | src/hls/PrintRTLBlock.ml | 0 | ||||
-rw-r--r-- | src/hls/PrintVerilog.ml (renamed from src/verilog/PrintVerilog.ml) | 0 | ||||
-rw-r--r-- | src/hls/PrintVerilog.mli (renamed from src/verilog/PrintVerilog.mli) | 0 | ||||
-rw-r--r-- | src/hls/RTLBlock.v | 69 | ||||
-rw-r--r-- | src/hls/RTLBlockgen.v | 39 | ||||
-rw-r--r-- | src/hls/Value.v (renamed from src/verilog/Value.v) | 0 | ||||
-rw-r--r-- | src/hls/ValueInt.v (renamed from src/verilog/ValueInt.v) | 0 | ||||
-rw-r--r-- | src/hls/Verilog.v (renamed from src/verilog/Verilog.v) | 2 | ||||
-rw-r--r-- | src/hls/Veriloggen.v (renamed from src/translation/Veriloggen.v) | 0 | ||||
-rw-r--r-- | src/hls/Veriloggenproof.v (renamed from src/translation/Veriloggenproof.v) | 0 |
23 files changed, 187 insertions, 10 deletions
@@ -9,8 +9,9 @@ endif COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \ MenhirLib cparser -COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \ - -R src/extraction vericert.extraction -R src/translation vericert.translation \ +COQINCLUDES := -R src/common vericert.common \ + -R src/extraction vericert.extraction \ + -R src/hls vericert.hls \ -R src vericert \ $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) @@ -19,7 +20,7 @@ COQMAKE := $(COQBIN)coq_makefile COQDOCFLAGS := --no-lib-name -l -VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v) +VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v) PREFIX ?= . diff --git a/_CoqProject b/_CoqProject index e86312b..72a2e4b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,7 +1,6 @@ -R src/common vericert.common -R src/extraction vericert.extraction --R src/translation vericert.translation --R src/verilog vericert.verilog +-R src/hls vericert.hls -R src vericert -R lib/CompCert/MenhirLib compcert.MenhirLib diff --git a/default.nix b/default.nix index a253285..3c8bc92 100644 --- a/default.nix +++ b/default.nix @@ -30,7 +30,7 @@ stdenv.mkDerivation { buildInputs = [ ncoq ocamlPackages.menhir dune ocaml ocamlPackages.findlib bbv - gcc + gcc ocamlPackages.utop ]; enableParallelBuilding = true; @@ -1,5 +1,7 @@ with import <nixpkgs> {}; mkShell { - buildInputs = (import ./.).buildInputs ++ [ocamlPackages.ocp-indent verilog yosys]; + buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent verilog yosys + ocamlPackages.merlin ocamlPackages.utop + ]; } diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index b1a885e..e6ee512 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -16,7 +16,11 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From vericert Require Verilog Value Compiler. +From vericert Require + Verilog + Value + Compiler + RTLBlockgen. From Coq Require DecidableClass. @@ -162,12 +166,15 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false". Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". +Extract Constant RTLBlockgen.partition => "Partition.partition". + (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls + RTLBlockgen.transl_program Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/verilog/Array.v b/src/hls/Array.v index fe0f6b2..fe0f6b2 100644 --- a/src/verilog/Array.v +++ b/src/hls/Array.v diff --git a/src/verilog/AssocMap.v b/src/hls/AssocMap.v index 8d8788a..8d8788a 100644 --- a/src/verilog/AssocMap.v +++ b/src/hls/AssocMap.v diff --git a/src/verilog/HTL.v b/src/hls/HTL.v index 620ef14..620ef14 100644 --- a/src/verilog/HTL.v +++ b/src/hls/HTL.v diff --git a/src/translation/HTLgen.v b/src/hls/HTLgen.v index 68e0293..68e0293 100644 --- a/src/translation/HTLgen.v +++ b/src/hls/HTLgen.v diff --git a/src/translation/HTLgenproof.v b/src/hls/HTLgenproof.v index bf63800..22f8f57 100644 --- a/src/translation/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1,4 +1,4 @@ -(* + (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * diff --git a/src/translation/HTLgenspec.v b/src/hls/HTLgenspec.v index 541f9fa..541f9fa 100644 --- a/src/translation/HTLgenspec.v +++ b/src/hls/HTLgenspec.v diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml new file mode 100644 index 0000000..9241abe --- /dev/null +++ b/src/hls/Partition.ml @@ -0,0 +1,60 @@ +(* + * 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/>. + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlock + +(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_backedge i n = + let succ = RTL.successors_instr i in + List.filter (fun s -> P.lt n s) succ + +let find_backedges c = + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let rec bblock_from_RTL (c : RTL.code) i = + let succ = List.map (fun i -> PTree.get i c) (RTL.successors_instr i) in + match i, succ with + | RTL.Inop _, Some i::[] -> begin + match bblock_from_RTL c i with + | Errors.OK bb -> Errors.OK (prepend_instr RBnop bb) + | Errors.Error msg -> Errors.Error msg + end + | RTL.Iop (op, rs, dst, _), Some i::[] -> begin + match bblock_from_RTL c i with + | Errors.OK bb + end + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + { fn_sig = f.RTL.fn_entrypoint; + fn_stacksize = f.RTL.fn_stacksize; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = f.RTL.fn_code + } diff --git a/src/verilog/PrintHTL.ml b/src/hls/PrintHTL.ml index 44f8b01..44f8b01 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/hls/PrintHTL.ml diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/src/hls/PrintRTLBlock.ml diff --git a/src/verilog/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 0f64066..0f64066 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml diff --git a/src/verilog/PrintVerilog.mli b/src/hls/PrintVerilog.mli index 6a15ee9..6a15ee9 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/hls/PrintVerilog.mli diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v new file mode 100644 index 0000000..7169d4a --- /dev/null +++ b/src/hls/RTLBlock.v @@ -0,0 +1,69 @@ +(* + * 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/>. + *) + +From compcert Require Import + Coqlib + AST + Maps + Op + RTL + Registers. + +Definition node := positive. + +Inductive instruction : Type := +| RBnop : instruction +| RBop : operation -> list reg -> reg -> instruction +| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction +| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction. + +Definition bblock_body : Type := list instruction. + +Inductive control_flow_inst : Type := +| RBcall : signature -> ident -> list reg -> reg -> node -> control_flow_inst +| RBtailcall : signature -> ident -> list reg -> control_flow_inst +| RBbuiltin : external_function -> list (builtin_arg reg) -> + builtin_res reg -> node -> control_flow_inst +| RBcond : condition -> list reg -> node -> node -> control_flow_inst +| RBjumptable : reg -> list node -> control_flow_inst +| RBredurn : option reg -> control_flow_inst. + +Record bblock : Type := mk_bblock { + bb_body: bblock_body; + bb_exit: option control_flow_inst + }. + +Definition code : Type := PTree.t bblock. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v new file mode 100644 index 0000000..05f9a32 --- /dev/null +++ b/src/hls/RTLBlockgen.v @@ -0,0 +1,39 @@ +(* + * 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/>. + *) + +From compcert Require + RTL. +From compcert Require Import + AST + Maps. +From vericert Require Import + RTLBlock. + +Parameter partition : RTL.code -> code. + +Definition transl_function (f : RTL.function) : function := + mkfunction f.(RTL.fn_sig) + f.(RTL.fn_params) + f.(RTL.fn_stacksize) + (partition f.(RTL.fn_code)) + f.(RTL.fn_entrypoint). + +Definition transl_fundef := transf_fundef transl_function. + +Definition transl_program : RTL.program -> program := + transform_program transl_fundef. diff --git a/src/verilog/Value.v b/src/hls/Value.v index d6a3d8b..d6a3d8b 100644 --- a/src/verilog/Value.v +++ b/src/hls/Value.v diff --git a/src/verilog/ValueInt.v b/src/hls/ValueInt.v index f1fd056..f1fd056 100644 --- a/src/verilog/ValueInt.v +++ b/src/hls/ValueInt.v diff --git a/src/verilog/Verilog.v b/src/hls/Verilog.v index 3b0dd0a..c5dab9e 100644 --- a/src/verilog/Verilog.v +++ b/src/hls/Verilog.v @@ -29,7 +29,7 @@ Require Import Lia. Import ListNotations. -From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array. +From vericert Require Import Vericertlib Show ValueInt AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. diff --git a/src/translation/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..a0be0fa 100644 --- a/src/translation/Veriloggen.v +++ b/src/hls/Veriloggen.v diff --git a/src/translation/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..9abbd4b 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v |