diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-28 01:25:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-28 01:25:37 +0100 |
| commit | 34e0f092551fcd7e1eef4a8a3c863fa940dcbf2f (patch) | |
| tree | 2445041018f6ad9667f9ab5be5c24910b2575dbf /src/hls/RTLBlockInstr.v | |
| parent | 6959b38a343d4575efc442ea02422dc64cf59d00 (diff) | |
| download | vericert-34e0f092551fcd7e1eef4a8a3c863fa940dcbf2f.tar.gz vericert-34e0f092551fcd7e1eef4a8a3c863fa940dcbf2f.zip | |
Work on specification of RTLBlock generation
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, |