Create HTLgen

3 files changed, 5 insertions, 148 deletions

diff --git a/src/translation/DirectTrans.v b/src/translation/DirectTrans.v
deleted file mode 100644
index ca9bc61..0000000
--- a/src/translation/DirectTrans.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(* 
- * 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/HTLgen.v b/src/translation/HTLgen.v
index 705f9ad..9c2e168 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -179,6 +179,11 @@ Definition transf_function (f: function) : Errors.res module :=
   | Error err => Errors.Error err
   end.
 
+Definition example : mon HTL.code := PTree.traverse transf_instr
+  (PTree.set 2%positive (RTL.Icall sig ros args res n) (PTree.set 1%positive (RTL.Iop (Op.Omove) nil 1%positive 2%positive) (PTree.empty RTL.instruction))).
+
+Compute example.
+
 Definition transf_fundef (fd: fundef) : Errors.res moddecl :=
   transf_partial_fundef transf_function fd.
 
diff --git a/src/translation/SMTrans.v b/src/translation/SMTrans.v
deleted file mode 100644
index ca9bc61..0000000
--- a/src/translation/SMTrans.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(* 
- * 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.