From 97f0021e748179770a38b89d1aecc1cbeeab617f Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:34:34 +0200
Subject: [PATCH] correct_store_buffer: add comments in luFree and suFree

This adds comment to clarify a specificity of the Sn stage, which
follows the Su and Lu stages.

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

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 587d63b..d337d3d 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -14,14 +14,14 @@ Definition ready isSuUsed sbState (elt : instr_kind) :=
 Definition luFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Lu in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | None => true
   end.
 
 Definition suFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Su in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | None => true
   end.
 
-- 
GitLab