diff options
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r-- | src/verilog/Verilog.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 4144632..7d5e3c0 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -144,7 +144,8 @@ Inductive binop : Type := | Vor : binop (** or (binary [|]) *) | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) -| Vshr : binop. (** shift right ([>>]) *) +| Vshr : binop (** shift right ([>>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) (** ** Unary Operators *) @@ -320,6 +321,7 @@ Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> | Vxor => vxor | Vshl => vshl | Vshr => vshr + | Vshru => vshr (* FIXME: should not be the same operation. *) end. Definition unop_run (op : unop) : value -> value := |