aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/PrintVerilog.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-10-26 20:24:12 +0100
committerYann Herklotz <git@yannherklotz.com>2021-10-26 20:24:12 +0100
commite51e42283ac9f1f0a80c989ebca7d52eb35f08d3 (patch)
treee4e9615be7869348d6c3b1cbbc00bc92cfb7675c /src/hls/PrintVerilog.ml
parentb1ca2f1a6159a313e259a697826380962d7cfa48 (diff)
downloadvericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.tar.gz
vericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.zip
Work more on equivalence of SAT
Diffstat (limited to 'src/hls/PrintVerilog.ml')
-rw-r--r--src/hls/PrintVerilog.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index a5fa554..fbb26c5 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -82,7 +82,7 @@ let register a =
| Some s -> s
| None -> sprintf "reg_%d" (P.to_int a)
-(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*)
+(*let literal l = s printf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*)
let literal l =
let l' = camlint_of_coqint l in