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/verilog/HTL.v | 171 ------------------------------------------------------ 1 file changed, 171 deletions(-) delete mode 100644 src/verilog/HTL.v (limited to 'src/verilog/HTL.v') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v deleted file mode 100644 index 620ef14..0000000 --- a/src/verilog/HTL.v +++ /dev/null @@ -1,171 +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 Coq Require Import FSets.FMapPositive. -From vericert Require Import Vericertlib ValueInt AssocMap Array. -From vericert Require Verilog. -From compcert Require Events Globalenvs Smallstep Integers Values. -From compcert Require Import Maps. - -(** The purpose of the hardware transfer language (HTL) is to create a more -hardware-like layout that is still similar to the register transfer language -(RTL) that it came from. The main change is that function calls become module -instantiations and that we now describe a state machine instead of a -control-flow graph. *) - -Local Open Scope assocmap. - -Definition reg := positive. -Definition node := positive. - -Definition datapath := PTree.t Verilog.stmnt. -Definition controllogic := PTree.t Verilog.stmnt. - -Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := - forall p0 : positive, - In p0 (map fst (Maps.PTree.elements m)) -> - Z.pos p0 <= Integers.Int.max_unsigned. - -Record module: Type := - mkmodule { - mod_params : list reg; - mod_datapath : datapath; - mod_controllogic : controllogic; - mod_entrypoint : node; - mod_st : reg; - mod_stk : reg; - mod_stk_len : nat; - mod_finish : 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); - mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); - }. - -Definition fundef := AST.fundef module. - -Definition program := AST.program fundef unit. - -Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := - match rl, vl with - | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl') - | _, _ => empty_assocmap - end. - -Definition empty_stack (m : module) : Verilog.assocmap_arr := - (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). - -(** * Operational Semantics *) - -Definition genv := Globalenvs.Genv.t fundef unit. - -Inductive stackframe : Type := - Stackframe : - forall (res : reg) - (m : module) - (pc : node) - (reg_assoc : Verilog.assocmap_reg) - (arr_assoc : Verilog.assocmap_arr), - stackframe. - -Inductive state : Type := -| State : - forall (stack : list stackframe) - (m : module) - (st : node) - (reg_assoc : Verilog.assocmap_reg) - (arr_assoc : Verilog.assocmap_arr), state -| Returnstate : - forall (res : list stackframe) - (v : value), state -| Callstate : - forall (stack : list stackframe) - (m : module) - (args : list value), state. - -Inductive step : genv -> state -> Events.trace -> state -> Prop := -| step_module : - forall g m st sf ctrl data - asr asa - basr1 basa1 nasr1 nasa1 - basr2 basa2 nasr2 nasa2 - asr' asa' - f pstval, - asr!(mod_reset m) = Some (ZToValue 0) -> - asr!(mod_finish m) = Some (ZToValue 0) -> - asr!(m.(mod_st)) = Some (posToValue st) -> - m.(mod_controllogic)!st = Some ctrl -> - m.(mod_datapath)!st = Some data -> - Verilog.stmnt_runp f - (Verilog.mkassociations asr empty_assocmap) - (Verilog.mkassociations asa (empty_stack m)) - ctrl - (Verilog.mkassociations basr1 nasr1) - (Verilog.mkassociations basa1 nasa1) -> - basr1!(m.(mod_st)) = Some (posToValue st) -> - Verilog.stmnt_runp f - (Verilog.mkassociations basr1 nasr1) - (Verilog.mkassociations basa1 nasa1) - data - (Verilog.mkassociations basr2 nasr2) - (Verilog.mkassociations basa2 nasa2) -> - asr' = Verilog.merge_regs nasr2 basr2 -> - asa' = Verilog.merge_arrs nasa2 basa2 -> - asr'!(m.(mod_st)) = Some (posToValue pstval) -> - Z.pos pstval <= Integers.Int.max_unsigned -> - step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') -| step_finish : - forall g m st asr asa retval sf, - asr!(m.(mod_finish)) = Some (ZToValue 1) -> - asr!(m.(mod_return)) = Some retval -> - step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) -| step_call : - forall g m args res, - step g (Callstate res m args) Events.E0 - (State res m m.(mod_entrypoint) - (AssocMap.set (mod_reset m) (ZToValue 0) - (AssocMap.set (mod_finish m) (ZToValue 0) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))))) - (empty_stack m)) -| step_return : - forall g m asr asa i r sf pc mst, - mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). -Hint Constructors step : htl. - -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