aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Verilog.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-07-07 17:27:08 +0100
committerYann Herklotz <git@yannherklotz.com>2020-07-07 17:27:08 +0100
commit8486b4c046914b1388b68fe906fe267108f84267 (patch)
tree2a09eb912526825848fac77df54fe9e4917cd385 /src/verilog/Verilog.v
parente63fef0613ed9e497279ae47b746413a093e9530 (diff)
downloadvericert-kvx-8486b4c046914b1388b68fe906fe267108f84267.tar.gz
vericert-kvx-8486b4c046914b1388b68fe906fe267108f84267.zip
Fixes to operators
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r--src/verilog/Verilog.v5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 43df3dd..321bdc2 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -143,8 +143,8 @@ Inductive binop : Type :=
| Vxor : binop (** xor (binary [^|]) *)
| Vshl : binop (** shift left ([<<]) *)
| Vshr : binop (** shift right ([>>>]) *)
-| Vshru : binop (** shift right unsigned ([>>]) *)
-| Vror : binop. (** shift right unsigned ([>>]) *)
+| Vshru : binop. (** shift right unsigned ([>>]) *)
+(*| Vror : binop (** shift right unsigned ([>>]) *)*)
(** ** Unary Operators *)
@@ -325,7 +325,6 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value :=
| Vshl => Some (Int.shl v1 v2)
| Vshr => Some (Int.shr v1 v2)
| Vshru => Some (Int.shru v1 v2)
- | Vror => Some (Int.ror v1 v2)
end.
Definition unop_run (op : unop) (v1 : value) : value :=