diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-30 14:03:40 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-30 14:03:40 +0100 |
commit | ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a (patch) | |
tree | aba30758bbbf10ab3d975367f48a695b81afb179 /src/verilog/ValueInt.v | |
parent | 9d6979baa0e4b505862bcedee1dfd075f36579c3 (diff) | |
download | vericert-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.tar.gz vericert-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.zip |
Add RTLBlock intermediate language
Diffstat (limited to 'src/verilog/ValueInt.v')
-rw-r--r-- | src/verilog/ValueInt.v | 167 |
1 files changed, 0 insertions, 167 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v deleted file mode 100644 index f1fd056..0000000 --- a/src/verilog/ValueInt.v +++ /dev/null @@ -1,167 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -(* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. -From compcert Require Import lib.Integers common.Values. -From vericert Require Import Vericertlib. -(* end hide *) - -(** * Value - -A [value] is a bitvector with a specific size. We are using the implementation -of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. -However, we need to wrap it with an [Inductive] so that we can specify and match -on the size of the [value]. This is necessary so that we can easily store -[value]s of different sizes in a list or in a map. - -Using the default [word], this would not be possible, as the size is part of the type. *) - -Definition value : Type := int. - -(** ** Value conversions - -Various conversions to different number types such as [N], [Z], [positive] and -[int], where the last one is a theory of integers of powers of 2 in CompCert. *) - -Definition valueToNat (v : value) : nat := - Z.to_nat (Int.unsigned v). - -Definition natToValue (n : nat) : value := - Int.repr (Z.of_nat n). - -Definition valueToN (v : value) : N := - Z.to_N (Int.unsigned v). - -Definition NToValue (n : N) : value := - Int.repr (Z.of_N n). - -Definition ZToValue (z : Z) : value := - Int.repr z. - -Definition valueToZ (v : value) : Z := - Int.signed v. - -Definition uvalueToZ (v : value) : Z := - Int.unsigned v. - -Definition posToValue (p : positive) : value := - Int.repr (Z.pos p). - -Definition valueToPos (v : value) : positive := - Z.to_pos (Int.unsigned v). - -Definition intToValue (i : Integers.int) : value := i. - -Definition valueToInt (i : value) : Integers.int := i. - -Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i. - -Definition valueToPtr (i : value) : Integers.ptrofs := - Ptrofs.of_int i. - -Definition valToValue (v : Values.val) : option value := - match v with - | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => Some (ptrToValue off) - | Values.Vundef => Some (ZToValue 0%Z) - | _ => None - end. - -(** Convert a [value] to a [bool], so that choices can be made based on the -result. This is also because comparison operators will give back [value] instead -of [bool], so if they are in a condition, they will have to be converted before -they can be used. *) - -Definition valueToBool (v : value) : bool := - if Z.eqb (uvalueToZ v) 0 then false else true. - -Definition boolToValue (b : bool) : value := - natToValue (if b then 1 else 0). - -(** ** Arithmetic operations *) - -Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -intros; subst; assumption. Defined. - -Lemma unify_word_unfold : - forall sz w, - unify_word sz sz w eq_refl = w. -Proof. auto. Qed. - -Inductive val_value_lessdef: val -> value -> Prop := -| val_value_lessdef_int: - forall i v', - i = valueToInt v' -> - val_value_lessdef (Vint i) v' -| val_value_lessdef_ptr: - forall b off v', - off = valueToPtr v' -> - val_value_lessdef (Vptr b off) v' -| lessdef_undef: forall v, val_value_lessdef Vundef v. - -Inductive opt_val_value_lessdef: option val -> value -> Prop := -| opt_lessdef_some: - forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' -| opt_lessdef_none: forall v, opt_val_value_lessdef None v. - -Lemma valueToZ_ZToValue : - forall z, - (Int.min_signed <= z <= Int.max_signed)%Z -> - valueToZ (ZToValue z) = z. -Proof. auto using Int.signed_repr. Qed. - -Lemma uvalueToZ_ZToValue : - forall z, - (0 <= z <= Int.max_unsigned)%Z -> - uvalueToZ (ZToValue z) = z. -Proof. auto using Int.unsigned_repr. Qed. - -Lemma valueToPos_posToValue : - forall v, - 0 <= Z.pos v <= Int.max_unsigned -> - valueToPos (posToValue v) = v. -Proof. - unfold valueToPos, posToValue. - intros. rewrite Int.unsigned_repr. - apply Pos2Z.id. assumption. -Qed. - -Lemma valueToInt_intToValue : - forall v, - valueToInt (intToValue v) = v. -Proof. auto. Qed. - -Lemma valToValue_lessdef : - forall v v', - valToValue v = Some v' -> - val_value_lessdef v v'. -Proof. - intros. - destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. - unfold valueToInt. unfold intToValue in H1. auto. - inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. -Qed. - -Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, - ptrToValue in *). - -Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. |