From cb51a550c4bd3645369cdfabf2719750acc8f3d8 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:34:19 +0200
Subject: [PATCH] correct_store_buffer: fix ready and free functions

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

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 993249c..587d63b 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -5,10 +5,10 @@ Import ListNotations.
 (* free and cycle functions. *)
 Definition ready isSuUsed sbState (elt : instr_kind) :=
   match elt with
-  | (Load, (Lsu, 0)) => busFree isSuUsed sbState
-  | (_, (Su, 0)) => negb (sbStateT_beq sbState Full)
-  | (_, (_, 0)) => true
-  | _ => false
+  | (Load, (Lsu, _)) => busFree isSuUsed sbState
+  | (_, (Su, _)) => negb (sbStateT_beq sbState Full)
+  | (_, (Lu, S _)) => false
+  | _ => true
   end.
 
 Definition luFree isSuUsed sbState trace :=
@@ -28,7 +28,11 @@ Definition suFree isSuUsed sbState trace :=
 Definition lsuFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Lsu in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some (opcode, (stg, lat)) => ready isSuUsed sbState (opcode, (stg, lat)) &&
+                                  if stage_beq (nstg stg opcode) Lu then
+                                    luFree isSuUsed sbState trace
+                                  else
+                                    suFree isSuUsed sbState trace
   | None => true
   end.
 
-- 
GitLab