diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 23:28:28 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 23:28:28 +0100 |
commit | bfb722caf2d46867779222b45615481e9020f0aa (patch) | |
tree | 09ed655d7473cec86b2d52fc70aa3ce6dbe1284b /src | |
parent | 128b5d3a20647db3d0b17cc918d17fe5cadc07ff (diff) | |
download | vericert-kvx-bfb722caf2d46867779222b45615481e9020f0aa.tar.gz vericert-kvx-bfb722caf2d46867779222b45615481e9020f0aa.zip |
Rename asm to verilog
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 05353f9..db3a810 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -222,18 +222,19 @@ Proof. Qed. Theorem separate_transf_c_program_correct: - forall c_units asm_units c_program, - nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units asm_units -> + forall c_units verilog_units c_program, + nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units -> link_list c_units = Some c_program -> - exists asm_program, - link_list asm_units = Some asm_program - /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics asm_program). + exists verilog_program, + link_list verilog_units = Some verilog_program + /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program). Proof. intros. - assert (nlist_forall2 match_prog c_units asm_units). + assert (nlist_forall2 match_prog c_units verilog_units). { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } - assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + assert (exists verilog_program, link_list verilog_units = Some verilog_program + /\ match_prog c_program verilog_program). { eapply link_list_compose_passes; eauto. } - destruct H2 as (asm_program & P & Q). - exists asm_program; split; auto. apply c_semantic_preservation; auto. + destruct H2 as (verilog_program & P & Q). + exists verilog_program; split; auto. apply c_semantic_preservation; auto. Qed. |