diff options
| -rw-r--r-- | driver/CoqupDriver.ml | 4 | ||||
| -rw-r--r-- | src/Compiler.v | 2 | ||||
| -rw-r--r-- | src/CoqupClflags.ml | 1 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 1 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 2 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
| -rw-r--r-- | test/array.c | 7 | ||||
| -rw-r--r-- | test/matrix.c | 16 |
8 files changed, 23 insertions, 12 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml index afbe4d0..0b64f48 100644 --- a/driver/CoqupDriver.ml +++ b/driver/CoqupDriver.ml @@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile = set_dest Coqup.PrintClight.destination option_dclight ".light.c"; set_dest Coqup.PrintCminor.destination option_dcminor ".cm"; set_dest Coqup.PrintRTL.destination option_drtl ".rtl"; + set_dest Coqup.PrintHTL.destination option_dhtl ".htl"; set_dest Coqup.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Coqup.PrintLTL.destination option_dltl ".ltl"; set_dest Coqup.PrintMach.destination option_dmach ".mach"; @@ -253,6 +254,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -dclight Save generated Clight in <file>.light.c -dcminor Save generated Cminor in <file>.cm -drtl Save RTL at various optimization points in <file>.rtl.<n> + -dhtl Save HTL before Verilog generation <file>.htl -dltl Save LTL after register allocation in <file>.ltl -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s @@ -377,6 +379,7 @@ let cmdline_actions = Exact "-dclight", Set option_dclight; Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; + Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; @@ -388,6 +391,7 @@ let cmdline_actions = option_dclight := true; option_dcminor := true; option_drtl := true; + option_dhtl := true; option_dltl := true; option_dalloctrace := true; option_dmach := true; diff --git a/src/Compiler.v b/src/Compiler.v index 98ef429..a34b359 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -51,6 +51,7 @@ From coqup Require HTLgen. Parameter print_RTL: Z -> RTL.program -> unit. +Parameter print_HTL: HTL.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -79,6 +80,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@@ Inlining.transf_program @@ print (print_RTL 1) @@@ HTLgen.transl_program + @@ print print_HTL @@ Veriloggen.transl_program. Definition transf_frontend (p: Csyntax.program) : res RTL.program := diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml index 83dd31d..5b40ce6 100644 --- a/src/CoqupClflags.ml +++ b/src/CoqupClflags.ml @@ -3,3 +3,4 @@ let option_simulate = ref false let option_hls = ref true let option_debug_hls = ref false let option_initial = ref false +let option_dhtl = ref false diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index ba87af6..df21dc4 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -128,6 +128,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". +Extract Constant Compiler.print_HTL => "PrintHTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 6d10887..5265c97 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -78,7 +78,7 @@ let rec pprint_expr = function | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] - | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"] + | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] let rec pprint_stmnt i = diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 6544e52..62bf63f 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -16,6 +16,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +val pprint_stmnt : int -> Verilog.stmnt -> string + val print_value : out_channel -> Value.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit diff --git a/test/array.c b/test/array.c index e33d47b..7d78a61 100644 --- a/test/array.c +++ b/test/array.c @@ -1,4 +1,7 @@ int main() { - int x[5] = {1, 2, 3, 4, 5}; - return x[2]; + int x[3] = {1, 2, 3}; + int sum = 0, incr = 1; + for (int i = 0; i < 3; i=i+incr) + sum += x[i]; + return sum; } diff --git a/test/matrix.c b/test/matrix.c index 2bb17e7..daa00ae 100644 --- a/test/matrix.c +++ b/test/matrix.c @@ -1,10 +1,8 @@ -#define N 4 - -void matrix_multiply(int first[N][N], int second[N][N], int multiply[N][N]) { +void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { int sum = 0; - for (int c = 0; c < N; c++) { - for (int d = 0; d < N; d++) { - for (int k = 0; k < N; k++) { + for (int c = 0; c < 2; c++) { + for (int d = 0; d < 2; d++) { + for (int k = 0; k < 2; k++) { sum = sum + first[c][k]*second[k][d]; } multiply[c][d] = sum; @@ -14,9 +12,9 @@ void matrix_multiply(int first[N][N], int second[N][N], int multiply[N][N]) { } int main() { - int f[N][N] = {{1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}}; - int s[N][N] = {{5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}}; - int m[N][N] = {{0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}}; + int f[2][2] = {{1, 2}, {3, 4}}; + int s[2][2] = {{5, 6}, {7, 8}}; + int m[2][2] = {{0, 0}, {0, 0}}; matrix_multiply(f, s, m); return m[1][1]; |