validate junit files (with extra attributes added to schema)

sbysrc/sby_core.py

@@ -407,7 +407,9 @@ class SbyTask:
             proc.checkretcode = True
 
             def instance_hierarchy_callback(retcode):
-                assert retcode == 0
+                if retcode != 0:
+                    self.precise_prop_status = False
+                    return
                 if self.design_hierarchy == None:
                     with open(f"{self.workdir}/model/design.json") as f:
                         self.design_hierarchy = design_hierarchy(f)
@@ -776,6 +778,8 @@ class SbyTask:
         print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="0" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
         print(f'<properties>', file=f)
         print(f'<property name="os" value="{platform.system()}"/>', file=f)
+        print(f'<property name="expect" value="{", ".join(self.expect)}"/>', file=f)
+        print(f'<property name="status" value="{self.status}"/>', file=f)
         print(f'</properties>', file=f)
         if self.precise_prop_status:
             for check in checks:

tests/JUnit.xsd

@@ -130,6 +130,26 @@ Permission to waive conditions of this license may be requested from Windy Road
 							<xs:documentation xml:lang="en">Time taken (in seconds) to execute the test</xs:documentation>
 						</xs:annotation>
 					</xs:attribute>
+					<xs:attribute name="id" type="xs:string" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Cell ID of the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="type" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Kind of property (assert, cover, live)</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="location" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Source location of the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="tracefile" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Tracefile for the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
 				</xs:complexType>
 			</xs:element>
 			<xs:element name="system-out">

tests/Makefile

@@ -1,11 +1,17 @@
 SBY_FILES=$(wildcard *.sby)
 SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=))
+JUNIT_TESTS=junit_assert_pass junit_assert_fail junit_assert_preunsat \
+junit_cover_pass junit_cover_uncovered junit_cover_assert junit_cover_preunsat \
+junit_timeout_error_timeout junit_timeout_error_syntax junit_timeout_error_solver
 
-.PHONY: test
+.PHONY: test validate_junit
 
 FORCE:
 
-test: $(SBY_TESTS)
+test: $(JUNIT_TESTS)
 
 test_%: %.sby FORCE
 	python3 ../sbysrc/sby.py -f $<
+
+$(JUNIT_TESTS): $(SBY_TESTS)
+	python validate_junit.py $@/$@.xml

tests/cover_fail.sby

@@ -1,7 +1,7 @@
 [options]
 mode cover
 depth 5
-expect fail
+expect pass,fail
 
 [engines]
 smtbmc boolector

tests/junit_assert.sby

@@ -0,0 +1,38 @@
+[tasks]
+pass
+fail
+preunsat
+
+[options]
+mode bmc
+depth 1
+
+pass: expect pass
+fail: expect fail
+preunsat: expect error
+
+[engines]
+smtbmc boolector
+
+[script]
+fail: read -define FAIL
+preunsat: read -define PREUNSAT
+read -sv test.sv
+prep -top top
+
+[file test.sv]
+module test(input foo);
+always @* assert(foo);
+`ifdef FAIL
+always @* assert(!foo);
+`endif
+`ifdef PREUNSAT
+always @* assume(!foo);
+`endif
+endmodule
+
+module top();
+test test_i (
+.foo(1'b1)
+);
+endmodule

tests/junit_cover.sby

@@ -0,0 +1,43 @@
+[tasks]
+pass
+uncovered fail
+assert fail
+preunsat
+
+[options]
+mode cover
+depth 1
+
+pass: expect pass
+fail: expect fail
+preunsat: expect fail
+
+[engines]
+smtbmc boolector
+
+[script]
+uncovered: read -define FAIL
+assert: read -define FAIL_ASSERT
+preunsat: read -define PREUNSAT
+read -sv test.sv
+prep -top top
+
+[file test.sv]
+module test(input foo);
+`ifdef PREUNSAT
+always @* assume(!foo);
+`endif
+always @* cover(foo);
+`ifdef FAIL
+always @* cover(!foo);
+`endif
+`ifdef FAIL_ASSERT
+always @* assert(!foo);
+`endif
+endmodule
+
+module top();
+test test_i (
+.foo(1'b1)
+);
+endmodule

tests/junit_timeout_error.sby

@@ -0,0 +1,42 @@
+[tasks]
+syntax error
+solver error
+timeout
+
+[options]
+mode cover
+depth 1
+timeout: timeout 1
+error: expect error
+timeout: expect timeout
+
+[engines]
+~solver: smtbmc --dumpsmt2 --progress --stbv z3
+solver: smtbmc foo
+
+[script]
+read -noverific
+syntax: read -define SYNTAX_ERROR
+read -sv primes.sv
+prep -top primes
+
+[file primes.sv]
+module primes;
+	parameter [8:0] offset = 7;
+	(* anyconst *) reg [8:0] prime1;
+	wire [9:0] prime2 = prime1 + offset;
+	(* allconst *) reg [4:0] factor;
+
+`ifdef SYNTAX_ERROR
+	foo
+`endif
+
+	always @* begin
+		if (1 < factor && factor < prime1)
+			assume ((prime1 % factor) != 0);
+		if (1 < factor && factor < prime2)
+			assume ((prime2 % factor) != 0);
+		assume (1 < prime1);
+		cover (1);
+	end
+endmodule