From 2d647ce5fdf5343a7d9961a63d66b5191706aeaf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 22 Mar 2022 16:43:39 +0000 Subject: Add comments to allow for literate detangling --- src/hls/RTLPar.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/hls/RTLPar.v') diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 4986cff..bcb51c6 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz + * Copyright (C) 2020-2022 Yann Herklotz * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -16,6 +16,7 @@ * along with this program. If not, see . *) +(* [[file:../../lit/scheduling.org::rtlpar-main][rtlpar-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Events. @@ -138,3 +139,4 @@ Definition max_pc_function (f: function) : positive := (pc + match Zlength i.(bb_body) with Z.pos p => p | _ => 1 end))%positive) f.(fn_code) 1%positive. +(* rtlpar-main ends here *) -- cgit