From be8d929aef8e86c2e22e32c525093c6bfe56a300 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 18:17:31 +0200 Subject: Adding both RV expansion methods in kvx-work --- riscV/RTLpathSE_simplify.v | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'riscV/RTLpathSE_simplify.v') diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 7aca1772..ca049962 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -853,16 +853,6 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. -Remark cast32unsigned_from_cast32signed: - forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). -Proof. - intros. apply Int64.same_bits_eq; intros. - rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. - rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). - change Int.zwordsize with 32. - destruct (zlt i0 32). auto. apply Int.bits_above. auto. -Qed. - (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall -- cgit