diff --git a/src/definitions.v b/src/definitions.v index 788c278cc6c7a926727067dcf64389ce5d56eba7..77197b7084ea4f33dec67ee9966f9572d0bf2e3a 100644 --- a/src/definitions.v +++ b/src/definitions.v @@ -229,6 +229,15 @@ Proof. + contradiction. Qed. +(* Pipeline comparison. *) +Definition pipeline_leb p1 p2 := + let comb := List.combine p1 p2 in + Nat.eqb (List.length p1) (List.length p2) + && List.forallb (fun instrs => + match instrs with + | ((o1, st1), (o2, st2)) => opcode_beq o1 o2 && state_leb st1 st2 + end) comb. + (* Pipeline validity. *) Definition single_in_stage trace st := List.count_occ stage_eq_dec (get_stg trace) st <=? 1.