1 files changed, 6 insertions, 23 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a172b3a..f348ee6 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -1,5 +1,5 @@
 (* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -17,7 +17,7 @@
  *)
 
 open Verilog
-open ValueInt
+open Value
 open Datatypes
 
 open Camlcoq
@@ -26,7 +26,7 @@ open Clflags
 
 open Printf
 
-open CoqupClflags
+open VericertClflags
 
 let concat = String.concat ""
 
@@ -70,30 +70,16 @@ let unop = function
 
 let register a = sprintf "reg_%d" (P.to_int a)
 
-let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
+let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))
 
-let literal_int i = sprintf "32'd%d" i
-
-let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
-
-
-let rec pprint_expr =
-  let array_byte r i = function
-     | 0 -> concat [register r; "["; pprint_expr i; "]"]
-     | n -> concat [register r; "["; pprint_expr i; " + "; literal_int n; "][7:0]"]
-  in function
+let rec pprint_expr = function
   | Vlit l -> literal l
   | Vvar s -> register s
-  | Vvarb0 s -> byte 0 s
-  | Vvarb1 s -> byte 1 s
-  | Vvarb2 s -> byte 2 s
-  | Vvarb3 s -> byte 3 s
   | 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]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
-  | Vload (s, i) -> concat ["{"; array_byte s i 3; ", "; array_byte s i 2; ", "; array_byte s i 1; ", "; array_byte s i 0; "}"]
 
 let rec pprint_stmnt i =
   let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s;
@@ -183,12 +169,9 @@ let testbench = "module testbench;
 
    always #5 clk = ~clk;
 
-   reg [31:0] count;
-   initial count = 0;
    always @(posedge clk) begin
-      count <= count + 1;
       if (finish == 1) begin
-         $display(\"finished: %d cycles %d\", return_val, count);
+         $display(\"finished: %d\", return_val);
          $finish;
       end
    end