From c59de73d5041effdddbae588420f9f8d0972fd44 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 5 Jul 2022 19:48:53 +0200
Subject: [PATCH] rc: move sbStateT to definitions
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 10 ----------
src/definitions.v | 12 +++++++++++-
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index c000ebf..7dd8dbc 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -2,17 +2,7 @@ Require Import Bool Lia List Nat PeanoNat.
From StoreBuffer Require Import definitions utils.
Import ListNotations.
-Variant sbStateT :=
- | Empty
- | NotEmpty
- | Full.
-
-Scheme Equality for sbStateT.
-
(* free and cycle functions. *)
-Definition busFree isSuUsed sbState :=
- (sbStateT_beq sbState Empty) && (negb isSuUsed).
-
Definition ready isSuUsed sbState (elt : instr_kind) :=
match elt with
| (Load, (Lsu, 0)) => busFree isSuUsed sbState
diff --git a/src/definitions.v b/src/definitions.v
index 3096c87..6f1ef36 100644
--- a/src/definitions.v
+++ b/src/definitions.v
@@ -5,7 +5,7 @@
Require Import Bool List Nat.
Import ListNotations.
-(* Basic definitions: opcodes and stages. *)
+(* Basic definitions: opcodes, stages, store buffer state. *)
Variant opcode :=
| Load
| Store.
@@ -97,6 +97,16 @@ Proof.
reflexivity.
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. *)
Definition state := (stage * nat)%type.
--
GitLab