diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-14 16:37:45 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-14 16:37:45 +0100 |
| commit | 63e84ca844c04562e05c1aae2606526d7288675f (patch) | |
| tree | e396730116d39848a2af314765891567ccf3531a /src/verilog | |
| parent | 8e3c89bad3a20c0bb9c88b83d966565d79822ff1 (diff) | |
| parent | 9215c5c6ec3312a44a0808481d03210baa859beb (diff) | |
| download | vericert-63e84ca844c04562e05c1aae2606526d7288675f.tar.gz vericert-63e84ca844c04562e05c1aae2606526d7288675f.zip | |
Merge branch 'develop'
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 3 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 4 |
2 files changed, 5 insertions, 2 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 700b8e3..a0f3ab3 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -58,7 +58,8 @@ let pprint_binop l r = | Vor -> unsigned "|" | Vxor -> unsigned "^" | Vshl -> unsigned "<<" - | Vshr -> unsigned ">>" + | Vshr -> signed ">>>" + | Vshru -> unsigned ">>" let unop = function | Vneg -> " ~ " diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b4b2f00..b80678e 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -130,7 +130,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 *) @@ -305,6 +306,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 := |