From 18a888d24e5bfcc75122a682b690ec4788584dd2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Apr 2020 17:28:21 +0100 Subject: Create Value module for bitvectors --- src/verilog/Value.v | 217 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 217 insertions(+) create mode 100644 src/verilog/Value.v (limited to 'src') diff --git a/src/verilog/Value.v b/src/verilog/Value.v new file mode 100644 index 0000000..5242d9b --- /dev/null +++ b/src/verilog/Value.v @@ -0,0 +1,217 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * 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 . + *) + +(* begin hide *) +From bbv Require Import Word. +From Coq Require Import ZArith.ZArith. +From compcert Require Import lib.Integers. +(* 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. *) + +Record value : Type := + mkvalue { + vsize: nat; + vword: word vsize + }. + +(** ** 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 wordToValue : forall sz : nat, word sz -> value := mkvalue. + +Definition valueToWord : forall v : value, word (vsize v) := vword. + +Definition valueToNat (v : value) : nat := + wordToNat (vword v). + +Definition natToValue sz (n : nat) : value := + mkvalue sz (natToWord sz n). + +Definition valueToN (v : value) : N := + wordToN (vword v). + +Definition NToValue sz (n : N) : value := + mkvalue sz (NToWord sz n). + +Definition posToValue sz (p : positive) : value := + mkvalue sz (posToWord sz p). + +Definition posToValueAuto (p : positive) : value := + let size := Z.to_nat (Z.succ (log_inf p)) in + mkvalue size (Word.posToWord size p). + +Definition ZToValue (s : nat) (z : Z) : value := + mkvalue s (ZToWord s z). + +Definition valueToZ (v : value) : Z := + wordToZ (vword v). + +Definition uvalueToZ (v : value) : Z := + uwordToZ (vword v). + +Definition intToValue (i : Integers.int) : value := + ZToValue Int.wordsize (Int.unsigned i). + +(** 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 := + negb (weqb (@wzero (vsize v)) (vword v)). + +Definition boolToValue (sz : nat) (b : bool) : value := + natToValue sz (if b then 1 else 0). + +(** ** Arithmetic operations *) + +Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +Proof. intros; subst; assumption. Qed. + +Definition value_eq_size: + forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. +Proof. + intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?. + left; apply Nat.eqb_eq in Heqb; assumption. + right; trivial. +Defined. + +Definition value_eq_size_nat: + forall (sz : nat) (v : value), { sz = vsize v } + { True }. +Proof. + intros; destruct (Nat.eqb sz (vsize v)) eqn:?. + left; apply Nat.eqb_eq in Heqb; assumption. + right; trivial. +Defined. + +Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + (EQ : vsize v1 = vsize v2) : A := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + f (vword v1) w2. + +Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + : option A := + match value_eq_size v1 v2 with + | left EQ => + Some (map_any v1 v2 f EQ) + | _ => None + end. + +Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value := + mkvalue (vsize v) (f (vsize v) (vword v)). + +Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + (EQ : (vsize v1 = vsize v2)) : value := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + mkvalue (vsize v1) (f (vsize v1) (vword v1) w2). + +Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (map_word2 f v1 v2 EQ) + | _ => None + end. + +Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (f EQ) + | _ => None + end. + +(** Arithmetic operations over [value], interpreting them as signed or unsigned +depending on the operation. + +The arithmetic operations over [word] are over [N] by default, however, can also +be called over [Z] explicitly, which is where the bits are interpreted in a +signed manner. *) + +Definition vplus v1 v2 := map_word2 wplus v1 v2. +Definition vminus v1 v2 := map_word2 wminus v1 v2. +Definition vmul v1 v2 := map_word2 wmult v1 v2. +Definition vdiv v1 v2 := map_word2 wdiv v1 v2. +Definition vmod v1 v2 := map_word2 wmod v1 v2. + +Definition vmuls v1 v2 := map_word2 wmultZ v1 v2. +Definition vdivs v1 v2 := map_word2 wdivZ v1 v2. +Definition vmods v1 v2 := map_word2 wremZ v1 v2. + +(** ** Bitwise operations + +Bitwise operations over [value], which is independent of whether the number is +signed or unsigned. *) + +Definition vnot v := map_word wnot v. +Definition vneg v := map_word wneg v. +Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)). +Definition vor v1 v2 := map_word2 wor v1 v2. +Definition vand v1 v2 := map_word2 wand v1 v2. +Definition vxor v1 v2 := map_word2 wxor v1 v2. + +(** ** Comparison operators + +Comparison operators that return a bool, there should probably be an equivalent +which returns another number, however I might just add that as an explicit +conversion. *) + +Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)). +Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ). + +Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ). +Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ). + +Definition vltb v1 v2 := map_any v1 v2 wltb. +Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)). +Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ). +Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ). + +Definition vltsb v1 v2 := map_any v1 v2 wsltb. +Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)). +Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ). +Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ). + +Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ). +Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ). +Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ). +Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ). + +Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ). +Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ). +Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ). +Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ). + +(** ** Shift operators + +Shift operators on values. *) + +Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) := + f w1 (wordToNat w2). + +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. -- cgit