Create a new direct translation

2 files changed, 125 insertions, 14 deletions

diff --git a/src/translation/DirectTrans.v b/src/translation/DirectTrans.v
new file mode 100644
index 0000000..ca9bc61
--- /dev/null
+++ b/src/translation/DirectTrans.v
@@ -0,0 +1,74 @@
+(* 
+ * 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 compcert.backend Require RTL.
+
+From coqup.verilog Require VerilogAST.
+
+Definition trans_instr (rtl : RTL.instruction) : VerilogAST.stmnt :=
+  match rtl with
+  | RTL.Inop s =>
+    (** Nop instruction should just become a Skip in Verilog, which is just a
+        semicolon. *)
+    VerilogAST.Skip
+  | RTL.Iop op args res s =>
+    (** Perform an arithmetic operation over registers.  This will just become
+        one binary operation in Verilog.  This will contain a list of registers,
+        so these will just become a chain of binary operations in Verilog. *)
+    VerilogAST.Skip
+  | RTL.Iload chunk addr args dst s =>
+    (** Load from memory, which will maybe become a load from RAM, however, I'm
+        not sure yet how memory will be implemented or how it will formalised
+        be. *)
+    VerilogAST.Skip
+  | RTL.Istore chunk addr args src s =>
+    (** How memory will be laid out will also affect how stores are handled.  For
+        now hopefully these can be ignored, and hopefull they are not used that
+        often when they are not required in C. *)
+    VerilogAST.Skip
+  | RTL.Icall sig ros args res s =>
+    (** Function call should become a module instantiation with start and end
+        signals appropriately wired up. *)
+    VerilogAST.Skip
+  | RTL.Itailcall sig ros args =>
+    (** Should be converted into a reset of the modules state, setting the
+        initial variables correctly.  This would simulate a tailcall as it is
+        similar to jumping back to the top of the function in assembly. *)
+    VerilogAST.Skip
+  | RTL.Ibuiltin ef args res s =>
+    (** Builtin functions will have to supported manually, by implementing the
+        Verilog myself. *)
+    VerilogAST.Skip
+  | RTL.Icond cond args s1 s2 =>
+    (** Will be converted into two separate processes that are combined by a mux
+        at the end, with a start flag that propagates in the construct that should
+        be chosen. *)
+    VerilogAST.Skip
+  | RTL.Ijumptable arg tbl =>
+    (** A jump to a specific instruction in the list, this will require setting
+        the state in the state machine appropriately.  This is trivial to
+        implement if no scheduling is involved, but as soon as that isn't the
+        case it might be difficult to find that location.  It would help to
+        transform the CFG to a few basic blocks first which cannot have any
+        branching. *)
+    VerilogAST.Skip
+  | RTL.Ireturn r =>
+    (** The return value of the function, which will just mean that the finished
+        signal goes high and the result is stored in the result register. *)
+    VerilogAST.Skip
+  end.
diff --git a/src/translation/SMTrans.v b/src/translation/SMTrans.v
index 33a65d5..ca9bc61 100644
--- a/src/translation/SMTrans.v
+++ b/src/translation/SMTrans.v
@@ -20,18 +20,55 @@ From compcert.backend Require RTL.
 
 From coqup.verilog Require VerilogAST.
 
-Definition translation (rtl : RTL.code) : Verilog.verilog :=
+Definition trans_instr (rtl : RTL.instruction) : VerilogAST.stmnt :=
   match rtl with
-  | RTL.Inop ->
-    (** Nop instruction should just become a Skip in Verilog, which is just a semicolon *)
-  | RTL.op ->
-    (** Perform an arithmetic operation over registers. This will just become one binary operation in
-        Verilog. This will contain a list of registers, so these will just become a chain of binary
-        operations in Verilog. *)
-  | RTL.Iload ->
-    (** Load from memory, which will maybe become a load from RAM, however, I'm not sure yet how memory
-        will be implemented or how it will be formalised. *)
-  | RTL.Istore ->
-    (** How memory will be laid out will also affect how stores are handled. For now hopefully these can
-        be ignored, and hopefull they are not used that often when they are not required in C. *)
-  | RTL.Icall -> 
+  | RTL.Inop s =>
+    (** Nop instruction should just become a Skip in Verilog, which is just a
+        semicolon. *)
+    VerilogAST.Skip
+  | RTL.Iop op args res s =>
+    (** Perform an arithmetic operation over registers.  This will just become
+        one binary operation in Verilog.  This will contain a list of registers,
+        so these will just become a chain of binary operations in Verilog. *)
+    VerilogAST.Skip
+  | RTL.Iload chunk addr args dst s =>
+    (** Load from memory, which will maybe become a load from RAM, however, I'm
+        not sure yet how memory will be implemented or how it will formalised
+        be. *)
+    VerilogAST.Skip
+  | RTL.Istore chunk addr args src s =>
+    (** How memory will be laid out will also affect how stores are handled.  For
+        now hopefully these can be ignored, and hopefull they are not used that
+        often when they are not required in C. *)
+    VerilogAST.Skip
+  | RTL.Icall sig ros args res s =>
+    (** Function call should become a module instantiation with start and end
+        signals appropriately wired up. *)
+    VerilogAST.Skip
+  | RTL.Itailcall sig ros args =>
+    (** Should be converted into a reset of the modules state, setting the
+        initial variables correctly.  This would simulate a tailcall as it is
+        similar to jumping back to the top of the function in assembly. *)
+    VerilogAST.Skip
+  | RTL.Ibuiltin ef args res s =>
+    (** Builtin functions will have to supported manually, by implementing the
+        Verilog myself. *)
+    VerilogAST.Skip
+  | RTL.Icond cond args s1 s2 =>
+    (** Will be converted into two separate processes that are combined by a mux
+        at the end, with a start flag that propagates in the construct that should
+        be chosen. *)
+    VerilogAST.Skip
+  | RTL.Ijumptable arg tbl =>
+    (** A jump to a specific instruction in the list, this will require setting
+        the state in the state machine appropriately.  This is trivial to
+        implement if no scheduling is involved, but as soon as that isn't the
+        case it might be difficult to find that location.  It would help to
+        transform the CFG to a few basic blocks first which cannot have any
+        branching. *)
+    VerilogAST.Skip
+  | RTL.Ireturn r =>
+    (** The return value of the function, which will just mean that the finished
+        signal goes high and the result is stored in the result register. *)
+    VerilogAST.Skip
+  end.