diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-03 01:05:32 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-03 01:05:32 +0000 |
commit | 8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 (patch) | |
tree | edb357c24b7c4a50569cdc32e6d4f17f48673ede /src/hls/PrintVerilog.ml | |
parent | 3ddec58aa1ad7d1bd772868d34ab0e11cf8f1ad4 (diff) | |
download | vericert-kvx-8d5047ca436ba42e9253d24d6b5b2c0c62dd7437.tar.gz vericert-kvx-8d5047ca436ba42e9253d24d6b5b2c0c62dd7437.zip |
Fix state generation for if-conversion
Diffstat (limited to 'src/hls/PrintVerilog.ml')
-rw-r--r-- | src/hls/PrintVerilog.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index b2633ec..e40b051 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -79,6 +79,11 @@ let literal l = then sprintf "(- 32'd%ld)" (Int32.neg l') else sprintf "32'd%ld" l' +let compare_expr es1 es2 = + match es1, es2 with + | (Vlit p1, _), (Vlit p2, _) -> compare (camlint_of_coqint p1) (camlint_of_coqint p2) + | _, _ -> -1 + let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s @@ -102,9 +107,10 @@ let rec pprint_stmnt i = indent i; "end\n" ] | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case es; indent (i+1); "default:;\n"; - indent i; "endcase\n" - ] + fold_map pprint_case (List.sort compare_expr es |> List.rev); + indent (i+1); "default:;\n"; + indent i; "endcase\n" + ] | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] |