From 6981b4f28b7e005820679f70b965f0fa91b2f2a8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 29 Mar 2020 21:45:55 +0100
Subject: Complete conversion from HTL to Verilog

---
 src/translation/Veriloggen.v | 99 ++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 91 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 8edc889..dbf1c80 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -20,10 +20,11 @@ From Coq Require Import FSets.FMapPositive.
 
 From coqup Require Import HTL Verilog Coquplib.
 
-From compcert Require Errors.
+From compcert Require Errors Op AST.
 
 Definition node : Type := positive.
 Definition reg : Type := positive.
+Definition ident : Type := positive.
 
 Inductive statetrans : Type :=
   | StateGoto (p : node)
@@ -109,27 +110,109 @@ Module PTree.
 
 End PTree.
 
-Definition translate_instr
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+
+(** Translate an instruction to a statement. *)
+Definition translate_instr (op : Op.operation) (args : list reg) (dst : reg) : option stmnt :=
+  let assign := nonblock dst in
+  match op, args with
+  | Op.Omove, v::nil => Some (assign (Vvar v))
+  | Op.Ointconst n, _ => Some (assign (Vlit (intToValue n)))
+  | Op.Oneg, _ => None
+  | Op.Osub, _ => None
+  | Op.Omul, _ => None
+  | Op.Omulimm n, _ => None
+  | Op.Omulhs, _ => None
+  | Op.Omulhu, _ => None
+  | Op.Odiv, _ => None
+  | Op.Odivu, _ => None
+  | Op.Omod, _ => None
+  | Op.Omodu, _ => None
+  | Op.Oand, _ => None
+  | Op.Oandimm n, _ => None
+  | Op.Oor, _ => None
+  | Op.Oorimm n, _ => None
+  | Op.Oxor, _ => None
+  | Op.Oxorimm n, _ => None
+  | Op.Onot, _ => None
+  | Op.Oshl, _ => None
+  | Op.Oshlimm n, _ => None
+  | Op.Oshr, _ => None
+  | Op.Oshrimm n, _ => None
+  | Op.Oshrximm n, _ => None
+  | Op.Oshru, _ => None
+  | Op.Oshruimm n, _ => None
+  | Op.Ororimm n, _ => None
+  | Op.Oshldimm n, _ => None
+  | _, _ => None
+  end.
 
 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 option_err {A : Type} (str : string) (v : option A) (s : state) : mon A :=
+  match v with
+  | Some v' => OK v' s
+  | _ => Error (Errors.msg str)
+  end.
+
 Definition transf_instr (n : node) (i : instruction) (s : state) : mon node :=
   match i with
   | Hnop n' =>
-    add_instr n n' s Skip
+    add_instr n n' s Vskip
   | Hnonblock op args dst n' =>
-    add_instr n n' s (Nonblocking (Var dst) )
-  | _ => Error (Errors.msg "Hello")
+    match (translate_instr op args dst) with
+    | Some instr => add_instr n n' s instr
+    | _ => Error (Errors.msg "Instruction is not implemented.")
+    end
+  | _ => Error (Errors.msg "The other things were also not implemented")
+  end.
+
+Definition make_stm_cases (s : positive * stmnt) : expr * stmnt :=
+  match s with (a, b) => (posToExpr a, b) end.
+
+Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt :=
+  Vcase (Vvar r) (map make_stm_cases (PositiveMap.elements s)).
+
+Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt :=
+  match st with
+  | (n, StateGoto n') => (posToExpr n, nonblock r (posToExpr n'))
+  | (n, StateCond c n1 n2) => (posToExpr n, nonblock r (Vternary c (posToExpr n1) (posToExpr n2)))
   end.
 
+Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
+  Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)).
+
+Definition make_globals (globals : PositiveMap.t (nat * expr)) : verilog := nil.
+
+Definition make_verilog (s : state) : verilog :=
+  let r := 500%positive in
+  (make_statetrans r s.(st_statetrans)) :: (make_stm r s.(st_stm))
+                                        :: (make_globals s.(st_variables)).
+
 (** 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 :=
+Definition transf_module (m: module) : Errors.res verilog :=
   match PTree.traverse transf_instr m.(mod_code) with
-  | OK _ s =>
-    Errors.OK (Verilog nil)
+  | OK _ s => Errors.OK (make_verilog s)
   | Error err => Errors.Error err
   end.
+
+Fixpoint main_module (main : ident) (flist : list (ident * AST.globdef moddecl unit))
+         {struct flist} : option module :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_module main xs
+  | _ :: xs => main_module main xs
+  | nil => None
+  end.
+
+Definition transf_function (d : design) : Errors.res verilog :=
+  match main_module d.(AST.prog_main) d.(AST.prog_defs) with
+  | Some m => transf_module m
+  | _ => Errors.Error (Errors.msg "Could not find main module")
+  end.
-- 
cgit