Materials

02_proof/Makefile

+
+all:
+	make -C abstract_00/
+	make -C abstract_01/
+	#make -C abstract_02/
+	#make -C abstract_03/
+	#make -C abstract_04/
+	#make -C abstract_05/
+	#make -C abstract_06/
+	make -C proof_01/
+	make -C proof_02/
+	make -C proof_final/
+
+one_step:
+	make -C proof_one_step/
+
+full:
+	make -C abstract_00/
+	make -C abstract_01/
+	make -C abstract_02/
+	make -C abstract_03/
+	make -C abstract_04/
+	make -C abstract_05/
+	make -C abstract_06/
+	make -C proof_01/
+	make -C proof_02/
+	make -C proof_final/
+
+clean:
+	make -C abstract_00/    clean
+	make -C abstract_01/    clean
+	make -C abstract_02/    clean
+	make -C abstract_03/    clean
+	make -C abstract_04/    clean
+	make -C abstract_05/    clean
+	make -C abstract_06/    clean
+	make -C proof_01/       clean
+	make -C proof_02/       clean
+	make -C proof_final/    clean
+	make -C proof_one_step/ clean
+

02_proof/README

+
+Here we illustrate our approach through the verification of an ARM CoreSight
+flow trace decompresser using symbolic model-checking of temporal logic and
+automatic theorem proving.
+
+Details are provided in paper "An Automated Framework Towards Widespread Formal
+Verification of Complex Hardware Designs", ERTS 2022: Embedded Real Time
+Systems, 30-31 March 2022, Toulouse, France
+
+--------------------------------------------------------------------------------
+
+The goal is to prove that, for all "i" in range 0 to (1 << 7*8)-1, having input
+"in" set to "i" by sets of 8 bits (when "enable" is set) implies that output
+"data" is set to "i" when "ready" rises.
+
+We prove this specification from 7 local properties (to be verified with
+model-checking) available in files "abstract_*/property.smv".
+
+
+The proof is separated in 3 steps:
+
+- first step is to use uninterpreted functions abstraction to relieve the
+  automatic theorem prover in solving the satisfiability problem: all functions
+  "next_event_a()[j:j]()" and "next_event()()" are abstracted to booleans.
+  This task is performed in folders "abstract_*".
+  This step is unnecessary since abstraction is proven correct with coq: see
+  folder "coq".
+
+- second step is to prove the implication of 2 intermediate properties, by sets
+  of 3 or 4 bytes, where we merge uninterpreted functions into one boolean.
+  This task is performed twice (to cover all 7 bytes) in folders "proof_01" and
+  "proof_02".
+
+- third step is to finally prove the specification from 2 intermediate
+  properties.
+  This task is performed in folder "proof_final".
+
+
+To run the proof, several possibilities:
+
+- we can verify uninterpreted functions abstraction for all the 7 properties.
+  This is long and unnecessary. But it can be done by running "make full".
+
+- we can only verify uninterpreted functions abstraction for the 2 first
+  properties, then rely on the proof written in coq for all other 5 properties.
+  This is quicker and can be done by running "make".
+
+- once we verified uninterpreted functions abstraction. We can also try to run
+  the proof in only one step. This is longer and can be done by running
+  "make one_step".
+
+
+Makefiles assume that Spot is installed in folder
+"/usr/local/lib/python3.7/site-packages/". Path to access Spot can be changed in
+file "Rules.mk".
+

02_proof/Rules.mk

+
+# location where spot is installed:
+SPOT="/usr/local/lib/python3.7/site-packages/"
+
+#===============================================================================
+
+all : proof.log
+	grep tautology $<
+
+
+##
+# 3) running the proof:
+#
+proof.log : proof.py
+	chmod +x ./$^
+	./$^ > $@
+
+
+##
+# 2) translation from SMV to Spot and creation of an implication of the overall
+# specifications by the conjunction of the filtered left side properties:
+#
+proof.py : left_side.spec.smv ${SPEC}
+	../../scripts/psl2spot.py  \
+	  --properties $<          \
+	  --specifications ${SPEC} \
+	  --filter ${FILTER}       \
+	  --to $@
+	# location where spot is installed:
+	sed -i '2a import sys' $@
+	sed -i '3a sys.path.append(${SPOT})' $@
+	sed -i '4G' $@
+
+
+##
+# 1) on the left side of the implication, we have the axioms and the properties
+# verified through model-checking:
+#
+left_side.spec.smv : ${AXIOMS} ${PROP}
+	cat $^ > $@
+
+#===============================================================================
+
+clean :
+	$(RM) left_side.spec.smv proof.py proof.log

02_proof/abstract_00/Makefile

+
+PROP   = property.smv
+AXIOMS = axioms.smv
+SPEC   = intermediate.smv
+FILTER = ""
+
+#===============================================================================
+
+include ../Rules.mk

02_proof/abstract_00/axioms.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event_a()[1:1]()." :=
+  always(
+     ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] ("in" == uwconst(i_0, 8)) ))
+  <->
+    ( next("in_eq_i_0_when_1st_enable") )
+  );
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event()()." :=
+  always(
+    ( next( next_event(  "clk" && "ready") ("data__0" == uwconst(i_0, 8)) ))
+  <->
+    ( next("data__0_eq_i_0_when_1st_ready") )
+  );
+
+PSLSPEC
+  NAME "Data is 15 bytes long in the specifications." :=
+  always( ("data_size" >= 0ud4_7) -> ("data_size" >= 0ud4_1) );
+
+PSLSPEC
+  NAME "A 1-bit vector equals to 0ub1_1 is a true boolean value." :=
+  always( ("ready" == 0ub1_1) <-> "ready" );
+

02_proof/abstract_00/intermediate.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_0 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && "ready") )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && "ready") ))
+     -- received byte (with index 1) is equal to i_0:
+  && ( next( next_event(  "clk" && "ready") ("data_size" >= 0ud4_7) ))
+  && ( next("in_eq_i_0_when_1st_enable") )
+  ->
+     ( next("data__0_eq_i_0_when_1st_ready") )
+  );
+

02_proof/abstract_00/property.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_0 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && ("ready" == 0ub1_1)) )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && ("ready" == 0ub1_1)) ))
+     -- received byte (with index 1) is equal to i_0:
+  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_1) ))
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] ("in" == uwconst(i_0, 8)) ))
+  ->
+     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__0" == uwconst(i_0, 8)) ))
+  );
+

02_proof/abstract_01/Makefile

+
+PROP   = property.smv
+AXIOMS = axioms.smv
+SPEC   = intermediate.smv
+FILTER = ""
+
+#===============================================================================
+
+include ../Rules.mk

02_proof/abstract_01/axioms.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event_a()[2:2]()." :=
+  always(
+     ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 1
+  && ( next( next_event_a("clk" && "enable")[2:2] ("in" == uwconst(i_1, 8)) ))
+  <->
+    ( next("in_eq_i_1_when_2nd_enable") )
+  );
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event()()." :=
+  always(
+    ( next( next_event(  "clk" && "ready") ("data__1" == uwconst(i_1, 8)) ))
+  <->
+    ( next("data__1_eq_i_1_when_1st_ready") )
+  );
+
+PSLSPEC
+  NAME "Data is 15 bytes long in the specifications." :=
+  always( ("data_size" >= 0ud4_7) -> ("data_size" >= 0ud4_2) );
+
+PSLSPEC
+  NAME "A 1-bit vector equals to 0ub1_1 is a true boolean value." :=
+  always( ("ready" == 0ub1_1) <-> "ready" );

02_proof/abstract_01/intermediate.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_1 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && "ready") )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && "ready") ))
+     -- received byte (with index 2) is equal to i_1:
+  && ( next( next_event(  "clk" && "ready") ("data_size" >= 0ud4_7) ))
+  && ( next("in_eq_i_1_when_2nd_enable") )
+  ->
+     ( next("data__1_eq_i_1_when_1st_ready") )
+  );
+

02_proof/abstract_01/property.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_1." :=
+forall i_1 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && ("ready" == 0ub1_1)) )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && ("ready" == 0ub1_1)) ))
+     -- received byte (with index 2) is equal to i_1:
+  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_2) ))
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 1
+  && ( next( next_event_a("clk" && "enable")[2:2] ("in" == uwconst(i_1, 8)) ))
+  ->
+     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__1" == uwconst(i_1, 8)) ))
+  );
+

02_proof/abstract_02/Makefile

+
+PROP   = property.smv
+AXIOMS = axioms.smv
+SPEC   = intermediate.smv
+FILTER = ""
+
+#===============================================================================
+
+include ../Rules.mk

02_proof/abstract_02/axioms.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event_a()[3:3]()." :=
+  always(
+     ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 1
+  && ( next( next_event_a("clk" && "enable")[2:2] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 2
+  && ( next( next_event_a("clk" && "enable")[3:3] ("in" == uwconst(i_2, 8)) ))
+  <->
+    ( next("in_eq_i_2_when_3rd_enable") )
+  );
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event()()." :=
+  always(
+    ( next( next_event(  "clk" && "ready") ("data__2" == uwconst(i_2, 8)) ))
+  <->
+    ( next("data__2_eq_i_2_when_1st_ready") )
+  );
+
+PSLSPEC
+  NAME "Data is 15 bytes long in the specifications." :=
+  always( ("data_size" >= 0ud4_7) -> ("data_size" >= 0ud4_3) );
+
+PSLSPEC
+  NAME "A 1-bit vector equals to 0ub1_1 is a true boolean value." :=
+  always( ("ready" == 0ub1_1) <-> "ready" );

02_proof/abstract_02/intermediate.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_2 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && "ready") )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && "ready") ))
+     -- received byte (with index 3) is equal to i_2:
+  && ( next( next_event(  "clk" && "ready") ("data_size" >= 0ud4_7) ))
+  && ( next("in_eq_i_2_when_3rd_enable") )
+  ->
+     ( next("data__2_eq_i_2_when_1st_ready") )
+  );
+

02_proof/abstract_02/property.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_2 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && ("ready" == 0ub1_1)) )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && ("ready" == 0ub1_1)) ))
+     -- received byte (with index 3) is equal to i_2:
+  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_3) ))
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 1
+  && ( next( next_event_a("clk" && "enable")[2:2] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 2
+  && ( next( next_event_a("clk" && "enable")[3:3] ("in" == uwconst(i_2, 8)) ))
+  ->
+     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__2" == uwconst(i_2, 8)) ))
+  );
+

02_proof/abstract_03/Makefile

+
+PROP   = property.smv
+AXIOMS = axioms.smv
+SPEC   = intermediate.smv
+FILTER = ""
+
+#===============================================================================
+
+include ../Rules.mk

02_proof/abstract_03/axioms.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event_a()[4:4]()." :=
+  always(
+     ( next( next_event_a("clk" && "enable")[1:1] ("in" == 0ub8_00001000)   )) -- isync packet
+  && ( next( next_event_a("clk" && "enable")[4:4] ("in" == uwconst(i_3, 8)) ))
+  <->
+    ( next("in_eq_i_3_when_4th_enable") )
+  );
+
+PSLSPEC
+  NAME "Uninterpreted functions abstraction for next_event()()." :=
+  always(
+    ( next( next_event(  "clk" && "ready") ("data__3" == uwconst(i_3, 8)) ))
+  <->
+    ( next("data__3_eq_i_3_when_1st_ready") )
+  );
+
+PSLSPEC
+  NAME "Data is 15 bytes long in the specifications." :=
+  always( ("data_size" >= 0ud4_7) -> ("data_size" >= 0ud4_4) );
+
+PSLSPEC
+  NAME "A 1-bit vector equals to 0ub1_1 is a true boolean value." :=
+  always( ("ready" == 0ub1_1) <-> "ready" );

02_proof/abstract_03/intermediate.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_0." :=
+forall i_3 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && "ready") )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && "ready") ))
+     -- received byte (with index 4) is equal to i_3:
+  && ( next( next_event(  "clk" && "ready") ("data_size" >= 0ud4_7) ))
+  && ( next("in_eq_i_3_when_4th_enable") )
+  ->
+     ( next("data__3_eq_i_3_when_1st_ready") )
+  );
+

02_proof/abstract_03/property.smv

+
+MODULE main
+
+PSLSPEC
+  NAME "When ready, received bytes are copied in order on output vectors. Case
+        of data_3." :=
+forall i_3 in {0:255} :
+  always(
+     -- starting from a reset or the end of a packet:
+     ( ("clk" && "reset") || ("clk" && ("ready" == 0ub1_1)) )
+     -- no reset until a new packet is decompressed:
+  && ( next( !"reset" until ("clk" && ("ready" == 0ub1_1)) ))
+     -- received byte (with index 4) is equal to i_3:
+  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_4) ))
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_00000001) == 0ub8_00000001) )) -- branch packet
+  && ( next( next_event_a("clk" && "enable")[1:1] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 1
+  && ( next( next_event_a("clk" && "enable")[2:2] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 2
+  && ( next( next_event_a("clk" && "enable")[3:3] (("in" & 0ub8_10000000) == 0ub8_10000000) )) -- presence of Byte 3
+  && ( next( next_event_a("clk" && "enable")[4:4] ("in" == uwconst(i_3, 8)) ))
+  ->
+     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__3" == uwconst(i_3, 8)) ))
+  );
+

02_proof/abstract_04/Makefile

+
+PROP   = property.smv
+AXIOMS = axioms.smv
+SPEC   = intermediate.smv
+FILTER = ""
+
+#===============================================================================
+
+include ../Rules.mk