From a23cc48f449ffbfd347f833965c1e04b88e0009a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 Jun 2020 14:12:38 +0100 Subject: Add more unproven instructions, Admitted equiv to spec --- src/verilog/Verilog.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/verilog/Verilog.v') 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 := -- cgit