correct_store_buffer: fix ready and free functions

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

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.