From 0f223a52dc59646ce2731ebd9b2141ce1ad82ba1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 22 Mar 2022 18:04:18 +0000 Subject: Add first descriptions to org file --- src/hls/RTLBlockInstr.v | 49 ++++++++++++++----------------------------------- src/hls/RTLBlockgen.v | 26 ++++++++++++++++---------- 2 files changed, 30 insertions(+), 45 deletions(-) (limited to 'src') diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 7391f97..770f377 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -(* [[file:../../lit/scheduling.org::rtlblockinstr-main][rtlblockinstr-main]] *) +(* [[file:../../lit/scheduling.org::rtlblockinstr-imports][rtlblockinstr-imports]] *) Require Import Coq.micromega.Lia. Require Import compcert.backend.Registers. @@ -31,20 +31,9 @@ Require Import compcert.verilog.Op. Require Import Predicate. Require Import Vericertlib. +(* rtlblockinstr-imports ends here *) -(** * RTLBlock Instructions - -These instructions are used for [RTLBlock] and [RTLPar], so that they have consistent -instructions, which greatly simplifies the proofs, as they will by default have the same instruction -syntax and semantics. The only changes are therefore at the top-level of the instructions. - - ** Instruction Definition - -First, we define the instructions that can be placed into a basic block, meaning they won't branch. -The main changes to how instructions are defined in [RTL], is that these instructions don't have a -next node, as they will be in a basic block, and they also have an optional predicate ([pred_op]). -*) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *) Definition node := positive. Inductive instr : Type := @@ -53,12 +42,9 @@ Inductive instr : Type := | RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr. +(* rtlblockinstr-instr-def ends here *) -(** ** Control-Flow Instruction Definition - -These are the instructions that count as control-flow, and will be placed at the end of the basic -blocks. *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *) Inductive cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr | RBtailcall : signature -> reg + ident -> list reg -> cf_instr @@ -69,9 +55,9 @@ Inductive cf_instr : Type := | RBreturn : option reg -> cf_instr | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +(* rtlblockinstr-cf-instr-def ends here *) -(** ** Helper functions *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *) Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil @@ -160,24 +146,17 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) | _, _ => Regmap.init Vundef end. +(* rtlblockinstr-helpers ends here *) -(** *** Instruction State - -Definition of the instruction state, which contains the following: - -- [is_rs] This is the current state of the registers. -- [is_ps] This is the current state of the predicate registers, which is in a separate namespace and - area compared to the standard registers in [is_rs]. -- [is_mem] The current state of the memory. *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-instr-state][rtlblockinstr-instr-state]] *) Record instr_state := mk_instr_state { is_rs: regset; is_ps: predset; is_mem: mem; }. +(* rtlblockinstr-instr-state ends here *) -(** ** Top-Level Type Definitions *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *) Section DEFINITION. Context {bblock_body: Type}. @@ -240,9 +219,9 @@ Section DEFINITION. state. End DEFINITION. +(* rtlblockinstr-type-def ends here *) -(** ** Semantics *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *) Section RELSEM. Context {bblock_body : Type}. @@ -347,4 +326,4 @@ Section RELSEM. step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. End RELSEM. -(* rtlblockinstr-main ends here *) +(* rtlblockinstr-semantics ends here *) diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index f45151d..706cb09 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) +(* [[file:../../lit/scheduling.org::rtlblockgen-imports][rtlblockgen-imports]] *) Require compcert.backend.RTL. Require Import compcert.common.AST. Require Import compcert.lib.Maps. @@ -28,16 +28,10 @@ Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. #[local] Open Scope positive. +(* rtlblockgen-imports ends here *) -Parameter partition : RTL.function -> Errors.res function. - -(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold - function to find the desired element. *) -Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive := - List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes). - -(*Compute find_block (2::94::28::40::19::nil) 40.*) - +(* [[file:../../lit/scheduling.org::rtlblockgen-equalities-insert][rtlblockgen-equalities-insert]] *) +(* [[[[file:~/projects/vericert/lit/scheduling.org::rtlblockgen-equalities][rtlblockgen-equalities]]][rtlblockgen-equalities]] *) Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. Proof. decide equality. @@ -155,6 +149,18 @@ Defined. Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := if eqd a b then true else false. +(* rtlblockgen-equalities ends here *) +(* rtlblockgen-equalities-insert ends here *) + +(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) +Parameter partition : RTL.function -> Errors.res function. + +(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold + function to find the desired element. *) +Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive := + List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes). + +(*Compute find_block (2::94::28::40::19::nil) 40.*) Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) := match istr, istr' with -- cgit