validate junit files (with extra attributes added to schema)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ede1a8d968fb309d7d747531a0ec980b62ffe043..b50ca3e8d7f1c371c67568488a2ed68705844843 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/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:

diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd
index 84b0f157b19eaf5933ace3159e559b9ca749cefa..7a5f1846f73dae0ed210b09179f402d89d524827 100644 (file)
--- a/tests/JUnit.xsd
+++ b/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">

diff --git a/tests/Makefile b/tests/Makefile
index 58971e69c8866d38a876352ee8c7f9ba011e45ba..4b8ac3589ad4cd95eccfd8108bebb6e296f7261d 100644 (file)
--- a/tests/Makefile
+++ b/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

diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby
index 8031e207ee3b12fc77580e649961569ec5c384a8..391e0a830261fefff14ea9802ec2b6481797a3cf 100644 (file)
--- a/tests/cover_fail.sby
+++ b/tests/cover_fail.sby
@@ -1,7 +1,7 @@
 [options]
 mode cover
 depth 5
-expect fail
+expect pass,fail
 
 [engines]
 smtbmc boolector

diff --git a/tests/junit_assert.sby b/tests/junit_assert.sby
new file mode 100644 (file)
index 0000000..e13f375
--- /dev/null
+++ b/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

diff --git a/tests/junit_cover.sby b/tests/junit_cover.sby
new file mode 100644 (file)
index 0000000..53747ba
--- /dev/null
+++ b/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

diff --git a/tests/junit_timeout_error.sby b/tests/junit_timeout_error.sby
new file mode 100644 (file)
index 0000000..551de49
--- /dev/null
+++ b/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