diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:12:25 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:12:25 +0100 |
| commit | 7ee0ca8263632536582646eb83b909f78f9e6fe4 (patch) | |
| tree | 2fe0d6ca1704cd436e9943adbf0371cf200d43ba | |
| parent | 8f370a52a5424389d9f0b4b044020932a2febfd4 (diff) | |
| download | vericert-7ee0ca8263632536582646eb83b909f78f9e6fe4.tar.gz vericert-7ee0ca8263632536582646eb83b909f78f9e6fe4.zip | |
Add hex notation to values
| -rw-r--r-- | src/verilog/Value.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 241534c..1d31110 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -18,6 +18,7 @@ (* begin hide *) From bbv Require Import Word. +From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith. From compcert Require Import lib.Integers. (* end hide *) @@ -211,3 +212,11 @@ Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. + +Module HexNotationValue. + Export HexNotation. + Import WordScope. + + Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). + +End HexNotationValue. |