Skip to content
Snippets Groups Projects
Commit c59de73d authored by Alban Gruin's avatar Alban Gruin
Browse files

rc: move sbStateT to definitions


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent c6795c42
No related branches found
No related tags found
No related merge requests found
...@@ -2,17 +2,7 @@ Require Import Bool Lia List Nat PeanoNat. ...@@ -2,17 +2,7 @@ Require Import Bool Lia List Nat PeanoNat.
From StoreBuffer Require Import definitions utils. From StoreBuffer Require Import definitions utils.
Import ListNotations. Import ListNotations.
Variant sbStateT :=
| Empty
| NotEmpty
| Full.
Scheme Equality for sbStateT.
(* free and cycle functions. *) (* free and cycle functions. *)
Definition busFree isSuUsed sbState :=
(sbStateT_beq sbState Empty) && (negb isSuUsed).
Definition ready isSuUsed sbState (elt : instr_kind) := Definition ready isSuUsed sbState (elt : instr_kind) :=
match elt with match elt with
| (Load, (Lsu, 0)) => busFree isSuUsed sbState | (Load, (Lsu, 0)) => busFree isSuUsed sbState
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
Require Import Bool List Nat. Require Import Bool List Nat.
Import ListNotations. Import ListNotations.
(* Basic definitions: opcodes and stages. *) (* Basic definitions: opcodes, stages, store buffer state. *)
Variant opcode := Variant opcode :=
| Load | Load
| Store. | Store.
...@@ -97,6 +97,16 @@ Proof. ...@@ -97,6 +97,16 @@ Proof.
reflexivity. reflexivity.
Qed. Qed.
Variant sbStateT :=
| Empty
| NotEmpty
| Full.
Scheme Equality for sbStateT.
Definition busFree isSuUsed sbState :=
(sbStateT_beq sbState Empty) && (negb isSuUsed).
(* State of an instruction in the pipeline. *) (* State of an instruction in the pipeline. *)
Definition state := (stage * nat)%type. Definition state := (stage * nat)%type.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment