diff options
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r-- | src/hls/RTLBlockInstr.v | 22 |
1 files changed, 22 insertions, 0 deletions
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, |