diff options
| author | James Pollard <james@pollard.dev> | 2020-06-24 17:27:56 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-24 17:27:56 +0100 |
| commit | 0c7a19d7e1fc6ba980586292fc44fbec0dc6ce7e (patch) | |
| tree | 3c773d790941fc011ed20eeb1608ac49cda59bcb /src/verilog/Verilog.v | |
| parent | a67fb83021f3e5d7ade972ff329ab6c3c4b23620 (diff) | |
| parent | e60d6c39dd960da14383a823a382e55f88258588 (diff) | |
| download | vericert-0c7a19d7e1fc6ba980586292fc44fbec0dc6ce7e.tar.gz vericert-0c7a19d7e1fc6ba980586292fc44fbec0dc6ce7e.zip | |
Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proof
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 := |