diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-03-31 15:32:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-31 15:32:00 +0100 |
| commit | 34ea564d72230931b879f4a9a26d62c5d6573464 (patch) | |
| tree | ea237471de54ad8af8071564e7461257ea0a333b /src/verilog | |
| parent | 2d11fe952455efbb66a4cf9a59d9e39425bd522c (diff) | |
| download | vericert-34ea564d72230931b879f4a9a26d62c5d6573464.tar.gz vericert-34ea564d72230931b879f4a9a26d62c5d6573464.zip | |
Add more operators and print them
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 6 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 13 |
2 files changed, 15 insertions, 4 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 016a626..04a35de 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -49,6 +49,10 @@ let pprint_binop = function | Vshl -> " << " | Vshr -> " >> " +let unop = function + | Vneg -> " ~ " + | Vnot -> " ! " + let register a = P.to_int a let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) @@ -56,7 +60,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> sprintf "reg_%d" (register s) - | Vunop e -> concat ["(~"; pprint_expr e; ")"] + | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 09eb914..50a6809 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -54,12 +54,18 @@ Inductive binop : Type := | Vadd : binop (** addition (binary [+]) *) | Vsub : binop (** subtraction (binary [-]) *) | Vmul : binop (** multiplication (binary [*]) *) -| Vdiv : binop (** multiplication (binary [*]) *) -| Vmod : binop (** division ([/]) *) +| Vdiv : binop (** division (binary [/]) *) +| Vdivu : binop (** division unsigned (binary [/]) *) +| Vmod : binop (** remainder ([%]) *) +| Vmodu : binop (** remainder unsigned ([/]) *) | Vlt : binop (** less than ([<]) *) +| Vltu : binop (** less than unsigned ([<]) *) | Vgt : binop (** greater than ([>]) *) +| Vgtu : binop (** greater than unsigned ([>]) *) | Vle : binop (** less than or equal ([<=]) *) +| Vleu : binop (** less than or equal unsigned ([<=]) *) | Vge : binop (** greater than or equal ([>=]) *) +| Vgeu : binop (** greater than or equal unsigned ([>=]) *) | Veq : binop (** equal to ([==]) *) | Vne : binop (** not equal to ([!=]) *) | Vand : binop (** and (binary [&]) *) @@ -69,7 +75,8 @@ Inductive binop : Type := | Vshr : binop. (** shift left ([<<]) *) Inductive unop : Type := -| Vneg : unop. (** negation ([~]) *) +| Vneg (** negation ([~]) *) +| Vnot. (** not operation [!] *) Inductive expr : Type := | Vlit : value -> expr |