diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-06-28 18:26:34 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-28 18:26:34 +0100 |
commit | d8464b57c4f56937b04e1caa37eea3b287dd415c (patch) | |
tree | 575755fa750a950b783a6795f57de3eab3a82aee /src | |
parent | e72ef9094c1d8239e56c4da126bb3f05341702a2 (diff) | |
parent | 56f1dd7a658dd21bb267dc41fc0301adbd620a6d (diff) | |
download | vericert-d8464b57c4f56937b04e1caa37eea3b287dd415c.tar.gz vericert-d8464b57c4f56937b04e1caa37eea3b287dd415c.zip |
Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Gible.v | 6 | ||||
-rw-r--r-- | src/hls/GiblePar.v | 6 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 6 | ||||
-rw-r--r-- | src/hls/GibleSeqgen.v | 10 | ||||
-rw-r--r-- | src/hls/GibleSeqgenproof.v | 6 | ||||
-rw-r--r-- | src/hls/IfConversionproof.v | 6 |
6 files changed, 22 insertions, 18 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 399935b..8971535 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -16,9 +16,9 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <https://www.gnu.org/licenses/>. -============= -RTLBlockInstr -============= +===== +Gible +===== These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have consistent instructions, which greatly simplifies the proofs, as they will by diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v index 9600d16..fcfb3d0 100644 --- a/src/hls/GiblePar.v +++ b/src/hls/GiblePar.v @@ -30,9 +30,9 @@ Require Import compcert.verilog.Op. Require Import vericert.hls.Gible. (*| -======== -RTLBlock -======== +========= +Gible Seq +========= |*) Module ParBB <: BlockType. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 3ccb765..778e0cd 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -40,9 +40,9 @@ Import NE.NonEmptyNotation. #[local] Open Scope pred_op. (*| -========= -RTLPargen -========= +==================== +Gible Par Generation +==================== Abstract Computations ===================== diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v index 31dabf8..127ee53 100644 --- a/src/hls/GibleSeqgen.v +++ b/src/hls/GibleSeqgen.v @@ -16,10 +16,6 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <https://www.gnu.org/licenses/>. -=========== -RTLBlockgen -=========== - .. coq:: none |*) @@ -36,6 +32,12 @@ Require Import vericert.hls.GibleSeq. #[local] Open Scope positive. +(*| +==================== +Gible Seq Generation +==================== +|*) + Definition check_valid_node (tc: code) (e: node) := match tc ! e with | Some _ => true diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v index fd336ed..7451510 100644 --- a/src/hls/GibleSeqgenproof.v +++ b/src/hls/GibleSeqgenproof.v @@ -16,9 +16,9 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <https://www.gnu.org/licenses/>. -================ -RTLBlockgenproof -================ +========================== +Gible Seq Generation Proof +========================== .. coq:: none |*) diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index addc223..12cb2bb 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -133,7 +133,7 @@ Section CORRECTNESS. Proof using. unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f. unfold transf_function. destruct_match; auto. auto. - Qed. + Admitted. Lemma functions_translated: forall (v: Values.val) (f: GibleSeq.fundef), @@ -163,7 +163,7 @@ Section CORRECTNESS. repeat ffts. Qed. - Lemma transf_initial_states : +(*) Lemma transf_initial_states : forall s1, initial_state prog s1 -> exists s2, initial_state tprog s2 /\ match_states None s1 s2. @@ -281,4 +281,6 @@ Section CORRECTNESS. - apply senv_preserved. Qed. + +*) End CORRECTNESS. |