From 34e0f092551fcd7e1eef4a8a3c863fa940dcbf2f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 28 Mar 2022 01:25:37 +0100
Subject: Work on specification of RTLBlock generation

---
 src/hls/RTLBlockInstr.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'src/hls/RTLBlockInstr.v')

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index d308366..cd23da3 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -46,6 +46,9 @@ Require Import Vericertlib.
 Definition node := positive.
 
 (*|
+.. index::
+   triple: definition; RTLBlockInstr; instruction
+
 Instruction Definition
 ======================
 
@@ -67,6 +70,9 @@ Inductive instr : Type :=
   option pred_op -> condition -> list reg -> predicate -> instr.
 
 (*|
+.. index::
+   triple: definition; RTLBlockInstr; control-flow instruction
+
 Control-Flow Instruction Definition
 ===================================
 
@@ -312,6 +318,14 @@ Section RELSEM.
   | eval_pred_none:
       forall i i', eval_pred None i i' i.
 
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; instruction
+
+Step Instruction
+=============================
+|*)
+
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
       forall sp ist,
@@ -346,6 +360,14 @@ Section RELSEM.
       step_instr sp (mk_instr_state rs pr m)
                     (RBsetpred p' c args p) ist.
 
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; control-flow instruction
+
+Step Control-Flow Instruction
+=============================
+|*)
+
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
     forall s f sp rs m res fd ros sig args pc pc' pr,
-- 
cgit