From 4bdabd1828c48e74c6b1f701f57a1b3c421a95fb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 23:13:25 +0100 Subject: Redefine HTL for intermediate Verilog language --- src/translation/Veriloggenspec.v | 18 +++++ src/verilog/HTL.v | 145 +++++++++++++++++++-------------------- 2 files changed, 87 insertions(+), 76 deletions(-) (limited to 'src') diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v index 67e2cad..09d08ed 100644 --- a/src/translation/Veriloggenspec.v +++ b/src/translation/Veriloggenspec.v @@ -1,3 +1,21 @@ +(* + * CoqUp: 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 compcert Require RTL Op Maps. From coqup Require Import Coquplib Verilog Veriloggen Value. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 1d156ad..3d863b2 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -16,89 +16,82 @@ * along with this program. If not, see . *) -(** 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. - *) - -From coqup.common Require Import Coquplib. - -From compcert Require Import Maps. -From compcert Require Op AST Memory Registers. - -Definition node := positive. - -Definition reg := Registers.reg. +From Coq Require Import FSets.FMapPositive. +From coqup Require Import Coquplib Value. +From coqup Require Verilog. +From compcert Require Events Globalenvs Smallstep Integers. -Definition ident := AST.ident. +Import HexNotationValue. -Inductive instruction : Type := -| Hnop : node -> instruction -| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction - (** [Hnonblock op args res next] Defines a nonblocking assignment to a - register, using the operation defined in Op.v. *) -| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction -| Hinst : AST.signature -> ident -> reg -> node -> instruction - (** [Hinst sig fun args rst strt end res next] Defines the start of a - module instantiation, meaning the function will run until the result is - returned. *) -| Htailcall : AST.signature -> ident -> list reg -> instruction -| Hcond : Op.condition -> list reg -> node -> node -> instruction -| Hjumptable : reg -> list node -> instruction -| Hfinish : option reg -> instruction. - -Record inst : Type := - mkinst { - inst_moddecl : ident; - inst_args : list reg - }. +(** 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. *) -Definition code : Type := PTree.t instruction. +Notation "a ! b" := (PositiveMap.find b a) (at level 1). -Definition instances : Type := PTree.t inst. +Definition reg := positive. +Definition node := positive. -Definition empty_instances : instances := PTree.empty inst. +Definition datapath := PositiveMap.t Verilog.stmnt. +Definition controllogic := PositiveMap.t Verilog.stmnt. -(** Function declaration for VTL also contain a construction which describes the - functions that are called in the current function. This information is used - to print out *) -Record module : Type := +Record module: Type := mkmodule { - mod_sig : AST.signature; mod_params : list reg; - mod_stacksize : Z; - mod_code : code; - mod_insts : instances; - mod_entrypoint : node + mod_datapath : datapath; + mod_controllogic : controllogic; + mod_entrypoint : node; + mod_st : reg; + mod_finish : reg; + mod_return : reg }. -Definition moddecl := AST.fundef module. - -Definition design := AST.program moddecl unit. - -Definition modsig (md : moddecl) := - match md with - | AST.Internal m => mod_sig m - | AST.External ef => AST.ef_sig ef - end. - -(** Describes various transformations that can be applied to HTL. This applies - the transformation to each instruction in the function and returns the new - function with the modified instructions. *) -Section TRANSF. - - Variable transf_instr : node -> instruction -> instruction. - - Definition transf_module (m : module) : module := - mkmodule - m.(mod_sig) - m.(mod_params) - m.(mod_stacksize) - (PTree.map transf_instr m.(mod_code)) - m.(mod_insts) - m.(mod_entrypoint). - -End TRANSF. +(** * Operational Semantics *) + +Definition genv := Globalenvs.Genv.t unit unit. +Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil. + +Inductive state : Type := +| State : + forall (m : module) + (st : node) + (assoc : Verilog.assocset), + state +| Returnstate : forall v : value, state. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := +| step_module : + forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f, + m.(mod_controllogic)!st = Some ctrl -> + m.(mod_datapath)!st = Some data -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc0 Verilog.empty_assocset) + ctrl + (Verilog.mkassociations assoc1 nbassoc0) -> + Verilog.stmnt_runp f + (Verilog.mkassociations assoc1 nbassoc0) + data + (Verilog.mkassociations assoc2 nbassoc1) -> + assoc3 = Verilog.merge_assocset nbassoc1 assoc2 -> + step g (State m st assoc0) t (State m st assoc3) +| step_finish : + forall g t m st assoc retval, + assoc!(m.(mod_finish)) = Some (1'h"1") -> + assoc!(m.(mod_return)) = Some retval -> + step g (State m st assoc) t (Returnstate retval). +Hint Constructors step : htl. + +Inductive initial_state (m : module) : state -> Prop := +| initial_state_intro : forall st, + st = m.(mod_entrypoint) -> + initial_state m (State m st Verilog.empty_assocset). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + value_int_eqb retval retvali = true -> + final_state (Returnstate retval) retvali. + +Definition semantics (m : module) := + Smallstep.Semantics step (initial_state m) final_state genv_empty. -- cgit