From 450bda69837b02c20d2fb391bbe7827d1becaac4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 14 Jul 2020 16:08:58 +0100 Subject: Change name to Vericert --- src/translation/HTLgenproof.v | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index dd1d967..ddf8c3a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz * * This program is free software: you can redistribute it and/or modify @@ -18,8 +18,8 @@ From compcert Require RTL Registers AST. From compcert Require Import Integers Globalenvs Memory Linking. -From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. -From coqup Require HTL Verilog. +From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. +From vericert Require HTL Verilog. Require Import Lia. @@ -708,13 +708,12 @@ Section CORRECTNESS. Admitted. Lemma eval_cond_correct : - forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, - translate_condition cond args s1 = OK c s' i -> - Op.eval_condition - cond - (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) - m = Some b -> - Verilog.expr_runp f asr asa c (boolToValue b). + exists v' : value, + Verilog.expr_runp f' asr asa e v' /\ + val_value_lessdef + (Values.Val.of_optbool + (Op.eval_condition cond + (map (fun r : positive => Registers.Regmap.get r rs) args) m)) v' Admitted. (** The proof of semantic preservation for the translation of instructions -- cgit