From 658b618b6a72d76682e37e21480ab73348538429 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:38:07 +0200
Subject: [PATCH] correct_store_buffer: specify how the store buffer can evolve

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 src/correct_store_buffer.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 921df5c..08afe78 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -107,6 +107,28 @@ Section can_advance.
   Qed.
 End can_advance.
 
+Definition legal_sb_transitions st sbState sbState' :=
+  match st, sbState with
+  | Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+  | Su, Empty => sbState' = Empty
+  | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
+  end.
+
+Definition legal_sb_transitions_P suE suE' sbState sbState' :=
+  match suE, suE', sbState with
+  | true, true, Full => sbState' = Full
+  | true, true, _ => sbState' = NotEmpty \/ sbState' = Full
+  | true, false, Full => True
+  | true, false, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+  | true, false, Empty => sbState' = Empty
+  | false, true, Empty => sbState' = Empty
+  | false, true, Full => sbState' = Full
+  | false, true, _ => sbState' = NotEmpty \/ sbState' = Full
+  | false, false, Full => True
+  | false, false, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+  | false, false, Empty => sbState' = Empty
+  end.
+
 Section constrained.
   Variable opc : opcode.
   Variable e d : instr_kind.
-- 
GitLab