From 89ed843ff1862b740edc812b6b1d245dbccf0721 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 22 Feb 2022 16:16:37 +0100 Subject: [PATCH] validate junit files (with extra attributes added to schema) --- sbysrc/sby_core.py | 6 ++++- tests/JUnit.xsd | 20 ++++++++++++++++ tests/Makefile | 10 ++++++-- tests/cover_fail.sby | 2 +- tests/junit_assert.sby | 38 +++++++++++++++++++++++++++++++ tests/junit_cover.sby | 43 +++++++++++++++++++++++++++++++++++ tests/junit_timeout_error.sby | 42 ++++++++++++++++++++++++++++++++++ 7 files changed, 157 insertions(+), 4 deletions(-) create mode 100644 tests/junit_assert.sby create mode 100644 tests/junit_cover.sby create mode 100644 tests/junit_timeout_error.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ede1a8d..b50ca3e 100644 --- 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'', file=f) print(f'', file=f) print(f'', file=f) + print(f'', file=f) + print(f'', file=f) print(f'', file=f) if self.precise_prop_status: for check in checks: diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd index 84b0f15..7a5f184 100644 --- 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 Time taken (in seconds) to execute the test + + + Cell ID of the property + + + + + Kind of property (assert, cover, live) + + + + + Source location of the property + + + + + Tracefile for the property + + diff --git a/tests/Makefile b/tests/Makefile index 58971e6..4b8ac35 100644 --- 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 8031e20..391e0a8 100644 --- 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 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 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 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 -- 2.30.2