From 1c22af68f8d6fd13220922fbbe3bd7e43353c864 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:27:24 +0200
Subject: [PATCH] definitions: add a function to compare the whole pipeline

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

diff --git a/src/definitions.v b/src/definitions.v
index 788c278..77197b7 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.
-- 
GitLab