From 2df5dc835efa3ac7552363e81ef9af5d3145cc7e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 00:19:27 +0100 Subject: Finish manual simulation --- src/verilog/Test.v | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) (limited to 'src/verilog/Test.v') diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 5c22ef2..5fd6d07 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -1,9 +1,30 @@ +(* + * 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 . + *) + From coqup Require Import Verilog Veriloggen Coquplib Value. From compcert Require Import AST Errors Maps Op Integers. From compcert Require RTL. From Coq Require Import FSets.FMapPositive. +From bbv Require Import Word. Import ListNotations. Import HexNotationValue. +Import WordScope. + Local Open Scope word_scope. Definition test_module : module := @@ -60,6 +81,8 @@ Definition test_output_module : module := (Some Vskip)); Vdecl 1%positive 32; Vdecl 7%positive 32] |}. +Search (_ <> _ -> _ = _). + Lemma valid_test_output : transf_program test_input_program = OK test_output_module. Proof. trivial. Qed. @@ -95,4 +118,23 @@ Proof. apply get_state_fext_assoc. apply erun_Vvar_empty. auto. apply erun_Vlit. - unfold ZToValue. instantiate (1 := 32%nat). simpl. + unfold ZToValue. instantiate (1 := 32%nat). simpl. apply nevalue. simpl. + apply weqb_false. simpl. trivial. + eapply stmnt_runp_Vcase_nomatch. + apply get_state_fext_assoc. + apply erun_Vvar_empty. auto. + apply erun_Vlit. + unfold ZToValue. instantiate (1 := 32%nat). simpl. apply nevalue. simpl. + apply weqb_false. simpl. trivial. + eapply stmnt_runp_Vcase_default. + apply get_state_fext_assoc. + apply erun_Vvar_empty. auto. + apply stmnt_run_Vskip. + eapply mis_stepp_Cons. + apply mi_stepp_Vdecl. + eapply mis_stepp_Cons. + apply mi_stepp_Vdecl. + apply mis_stepp_Nil. + Unshelve. + exact 0%nat. +Qed. -- cgit