diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-08 23:34:36 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-08 23:34:47 +0100 |
| commit | 7dbed3811e57479c78e4e82806d343d9285576c1 (patch) | |
| tree | 1d195941660d4e939dc389e73104dc0d47dfcb6d | |
| parent | 32990af23915c15e5cfd4cfe32c47cafa508f11d (diff) | |
| download | vericert-7dbed3811e57479c78e4e82806d343d9285576c1.tar.gz vericert-7dbed3811e57479c78e4e82806d343d9285576c1.zip | |
Add lessdef for values
| -rw-r--r-- | src/verilog/Value.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index a96d67c..cde98d4 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,8 +19,8 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith. -From compcert Require Import lib.Integers. +From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From compcert Require Import lib.Integers common.Values. (* end hide *) (** * Value @@ -48,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. Definition valueToWord : forall v : value, word (vsize v) := vword. -Definition valueToNat (v : value) : nat := +Definition valueToNat (v :value) : nat := wordToNat (vword v). Definition natToValue sz (n : nat) : value := @@ -284,3 +284,10 @@ Module HexNotationValue. Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). End HexNotationValue. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + Integers.Int.unsigned i = valueToZ v' -> + val_value_lessdef (Vint i) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. |