diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-01-25 13:50:10 +0200 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-01-25 13:50:10 +0200 |
| commit | 2181eac18441168f773e3391c4671619f4339ee6 (patch) | |
| tree | 87fbb4c83af5199325027a69ad983f3a9f9f3890 /src/translation/Veriloggenproof.v | |
| parent | 9404debd87728ab9b78f8bfed68a758ee03520e3 (diff) | |
| download | vericert-2181eac18441168f773e3391c4671619f4339ee6.tar.gz vericert-2181eac18441168f773e3391c4671619f4339ee6.zip | |
Implement renumbering (wrong)
Diffstat (limited to 'src/translation/Veriloggenproof.v')
| -rw-r--r-- | src/translation/Veriloggenproof.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index c83a3b1..59267f7 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,14 +17,18 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. +From compcert Require Errors. From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. + Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := - match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. + +(* Lemma transf_program_match: forall prog, match_prog prog (transl_program prog). @@ -404,3 +408,4 @@ Section CORRECTNESS. Qed. End CORRECTNESS. +*) |