diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-07 10:13:22 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-07 10:13:22 +0000 |
| commit | 56ea621762c865c1c71bdc7ad99afc4f2c291d5c (patch) | |
| tree | dd7d0a853fe6e52fbef018b8b37b42275e5c2746 | |
| parent | 8c9f2c7ae763f21f605248baef6f512bce005bbe (diff) | |
| download | vericert-kvx-56ea621762c865c1c71bdc7ad99afc4f2c291d5c.tar.gz vericert-kvx-56ea621762c865c1c71bdc7ad99afc4f2c291d5c.zip | |
Update definition of Vneg
| -rw-r--r-- | src/common/IntegerExtra.v | 2 | ||||
| -rw-r--r-- | src/hls/Verilog.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 8b11823..f44cac2 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -639,7 +639,7 @@ Module IntExtra. apply unsigned_range_2. Qed. - Lemma shrx_shrx_alt_equiv : + Theorem shrx_shrx_alt_equiv : forall x y, unsigned y <= 30 -> shrx x y = shrx_alt x y. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index c5dab9e..e5f86d5 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -149,7 +149,7 @@ Inductive binop : Type := (** ** Unary Operators *) Inductive unop : Type := -| Vneg (** negation ([~]) *) +| Vneg (** negation ([-]) *) | Vnot. (** not operation [!] *) (** ** Expressions *) |