From f96332369cbb2420e29a588d0ad9cd9810315423 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 25 Mar 2020 23:44:19 +0000 Subject: Create HTLgen --- src/translation/DirectTrans.v | 74 ------------------------------------------- src/translation/HTLgen.v | 5 +++ src/translation/SMTrans.v | 74 ------------------------------------------- 3 files changed, 5 insertions(+), 148 deletions(-) delete mode 100644 src/translation/DirectTrans.v delete mode 100644 src/translation/SMTrans.v (limited to 'src') 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 - * - * 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 . - *) - -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 - * - * 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 . - *) - -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. -- cgit