Redefine HTL for intermediate Verilog language

2 files changed, 87 insertions, 76 deletions

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 <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 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 <https://www.gnu.org/licenses/>.
  *)
 
-(** 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.