Add Verilog generation from HTL

1 files changed, 135 insertions, 0 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
new file mode 100644
index 0000000..8edc889
--- /dev/null
+++ b/src/translation/Veriloggen.v
@@ -0,0 +1,135 @@
+(*
+ * 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 coqup Require Import HTL Verilog Coquplib.
+
+From compcert Require Errors.
+
+Definition node : Type := positive.
+Definition reg : Type := positive.
+
+Inductive statetrans : Type :=
+  | StateGoto (p : node)
+  | StateCond (c : expr) (t f : node).
+
+Record state: Type := mkstate {
+  st_variables: PositiveMap.t (nat * expr);
+  st_stm : PositiveMap.t stmnt;
+  st_statetrans : PositiveMap.t statetrans;
+}.
+
+Definition init_state : state :=
+  mkstate (PositiveMap.empty (nat * expr)) (PositiveMap.empty stmnt) (PositiveMap.empty statetrans).
+
+Inductive res (A: Type) (S: Type): Type :=
+  | Error: Errors.errmsg -> res A S
+  | OK: A -> S -> res A S.
+
+Arguments OK [A S].
+Arguments Error [A S].
+
+Definition mon (A: Type) : Type := res A state.
+
+Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s.
+
+Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
+    match f with
+    | Error msg => Error msg
+    | OK a s => g a
+    end.
+
+Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+  bind f (fun xy => g (fst xy) (snd xy)).
+
+Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B :=
+  match f with
+  | Error msg => Error msg
+  | OK a s => g a s
+  end.
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+   (at level 200, X ident, A at level 100, B at level 200).
+Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B))
+   (at level 200, X ident, Y ident, A at level 100, B at level 200).
+
+Definition handle_error {A: Type} (f g: mon A) : mon A :=
+  match f with
+  | OK a s' => OK a s'
+  | Error _ => g
+  end.
+
+Module PTree.
+  Export Maps.PTree.
+
+  Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B)
+           (m : t A) (s : state) (i : positive)
+           {struct m} : mon (t B) :=
+    match m with
+    | Leaf => OK Leaf s
+    | Node l o r =>
+      let newo :=
+          match o with
+          | None => OK None s
+          | Some x =>
+            match f (prev i) x s with
+            | Error err => Error err
+            | OK val s' => OK (Some val) s'
+            end
+          end in
+      match newo with
+      | OK no s =>
+        do (nl, s') <- xtraverse f l s (xO i);
+        do (nr, s'') <- xtraverse f r s' (xI i);
+        OK (Node nl no nr) s''
+      | Error msg => Error msg
+      end
+    end.
+
+  Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m :=
+    xtraverse f m init_state xH.
+
+  Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f).
+
+End PTree.
+
+Definition translate_instr
+
+Definition add_instr (n : node) (n' : node) (s : state) (st : stmnt) : mon node :=
+  OK n' (mkstate s.(st_variables)
+                 (PositiveMap.add n st s.(st_stm))
+                 (PositiveMap.add n (StateGoto n') s.(st_statetrans))).
+
+Definition transf_instr (n : node) (i : instruction) (s : state) : mon node :=
+  match i with
+  | Hnop n' =>
+    add_instr n n' s Skip
+  | Hnonblock op args dst n' =>
+    add_instr n n' s (Nonblocking (Var dst) )
+  | _ => Error (Errors.msg "Hello")
+  end.
+
+(** To start out with, the assumption is made that there is only one
+    function/module in the original code. *)
+Definition transf_function (m: module) : Errors.res verilog :=
+  match PTree.traverse transf_instr m.(mod_code) with
+  | OK _ s =>
+    Errors.OK (Verilog nil)
+  | Error err => Errors.Error err
+  end.