From 8a0bd7b74939b65a89b81352b238d1d8252fb278 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 17 Dec 2020 10:04:21 +0000
Subject: Add extraction and loop pipelining stage

---
 src/Compiler.v              |  5 ++++-
 src/extraction/Extraction.v |  6 ++++--
 src/hls/Pipeline.v          | 11 +++++++++++
 3 files changed, 19 insertions(+), 3 deletions(-)
 create mode 100644 src/hls/Pipeline.v

(limited to 'src')

diff --git a/src/Compiler.v b/src/Compiler.v
index 7df00d8..5895e1d 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -74,7 +74,8 @@ From vericert Require
      HTLgen
      RTLBlock
      RTLBlockgen
-     HTLSchedulegen.
+     HTLSchedulegen
+     Pipeline.
 
 From compcert Require Import Smallstep.
 
@@ -240,6 +241,8 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
+   @@ Pipeline.transf_program
+   @@ print (print_RTL 8)
   @@@ RTLBlockgen.transl_program
    @@ print print_RTLBlock
   @@@ HTLSchedulegen.transl_program
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index e8cfe50..7736bfa 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -22,7 +22,8 @@ From vericert Require
      RTLBlockgen
      RTLBlock
      HTLSchedulegen
-     HTLgen.
+     HTLgen
+     Pipeline.
 
 From Coq Require DecidableClass.
 
@@ -169,6 +170,7 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
 Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
 Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
+Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline".
 Extract Constant RTLBlockgen.partition => "Partition.partition".
 Extract Constant HTLSchedulegen.transl_module => "Schedule.transl_module".
 
@@ -179,9 +181,9 @@ Cd "src/extraction".
 Separate Extraction
          Verilog.module vericert.Compiler.transf_hls
          vericert.Compiler.transf_hls_temp
-         vericert.Compiler.transf_hls_opt
          RTLBlockgen.transl_program RTLBlock.successors_instr
          HTLgen.tbl_to_case_expr
+         Pipeline.pipeline
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v
new file mode 100644
index 0000000..ea0c32e
--- /dev/null
+++ b/src/hls/Pipeline.v
@@ -0,0 +1,11 @@
+From compcert Require Import
+     Maps
+     AST
+     RTL.
+
+Parameter pipeline : function -> function.
+
+Definition transf_fundef := transf_fundef pipeline.
+
+Definition transf_program : program -> program :=
+  transform_program transf_fundef.
-- 
cgit