diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index c000ebf945f11846adac85e35f203dd4cb56e57b..7dd8dbc47c4714553166652323650b772b469793 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 3096c8746c0e85b777589b8b20162edb68c007a2..6f1ef36601cc7ae04fc6cdb351a175ce82b2154c 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.