diff options
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 4 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 19 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 4 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 4 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 6 |
5 files changed, 18 insertions, 19 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 1cc30c7..8245a06 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * 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 @@ -19,7 +19,7 @@ From compcert Require Import Maps. From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. -From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. 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 <yann@yannherklotz.com> * * 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 diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 71fb618..93d5612 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * 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 @@ -18,7 +18,7 @@ From compcert Require RTL Op Maps Errors. From compcert Require Import Maps Integers. -From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. +From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f5d5fa7..a0be0fa 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * 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 @@ -19,7 +19,7 @@ From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST. -From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. Definition transl_list_fun (a : node * Verilog.stmnt) := let (n, stmnt) := a in diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 5b467a7..9abbd4b 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * 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 @@ -17,8 +17,8 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. -From coqup Require HTL. -From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap. +From vericert Require HTL. +From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. Local Open Scope assocmap. |