From: Jannis Harder Date: Mon, 11 Apr 2022 15:39:05 +0000 (+0200) Subject: Refactor tests X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8da6f07cb3c11375ac59b625aee4f75b40ca8464;p=SymbiYosys.git Refactor tests Organize tests into subdirectories and use a new makefile that scans .sby files and allows selecting tests by mode, engine, solver and/or subdirectory. Automatically skips tests that use engines/solvers that are not found in the PATH. See `cd tests; make help` for a description of supported make targets. --- diff --git a/tests/.gitignore b/tests/.gitignore index f91f05a..9737325 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,16 +1,2 @@ -/both_ex*/ -/cover*/ -/demo*/ -/memory*/ -/mixed*/ -/preunsat*/ -/prv32fmcmp*/ -/redxor*/ -/stopfirst*/ -/junit_*/ -/keepgoing_*/ -/submod_props*/ -/multi_assert*/ -/aim_vs_smt2_nonzero_start_offset*/ -/invalid_ff_dcinit_merge*/ -/2props1trace*/ +/make/rules +__pycache__ diff --git a/tests/2props1trace.sby b/tests/2props1trace.sby deleted file mode 100644 index 8f51fde..0000000 --- a/tests/2props1trace.sby +++ /dev/null @@ -1,22 +0,0 @@ -[options] -mode bmc -depth 1 -expect fail - -[engines] -smtbmc - -[script] -read -sv top.sv -prep -top top - -[file top.sv] -module top( -input foo, -input bar -); -always @(*) begin - assert (foo); - assert (bar); -end -endmodule diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd deleted file mode 100644 index 7a5f184..0000000 --- a/tests/JUnit.xsd +++ /dev/null @@ -1,232 +0,0 @@ - - - - JUnit test result schema for the Apache Ant JUnit and JUnitReport tasks -Copyright © 2011, Windy Road Technology Pty. Limited -The Apache Ant JUnit XML Schema is distributed under the terms of the Apache License Version 2.0 http://www.apache.org/licenses/ -Permission to waive conditions of this license may be requested from Windy Road Support (http://windyroad.org/support). - - - - - - - - - - Contains an aggregation of testsuite results - - - - - - - - - - Derived from testsuite/@name in the non-aggregated documents - - - - - Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite - - - - - - - - - - - - Contains the results of exexuting a testsuite - - - - - Properties (e.g., environment settings) set during test execution - - - - - - - - - - - - - - - - - - - - - - - - - Indicates that the test errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. Contains as a text node relevant data for the error, e.g., a stack trace - - - - - - - The error message. e.g., if a java exception is thrown, the return value of getMessage() - - - - - The type of error that occured. e.g., if a java execption is thrown the full class name of the exception. - - - - - - - - - Indicates that the test failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals. Contains as a text node relevant data for the failure, e.g., a stack trace - - - - - - - The message specified in the assert - - - - - The type of the assert. - - - - - - - - - - Name of the test method - - - - - Full class name for the class the test method is in. - - - - - 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 - - - - - - - Data that was written to standard out while the test was executed - - - - - - - - - - Data that was written to standard error while the test was executed - - - - - - - - - - - Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents - - - - - - - - - - when the test was executed. Timezone may not be specified. - - - - - Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined. - - - - - - - - - - The total number of tests in the suite - - - - - The total number of tests in the suite that failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals - - - - - The total number of tests in the suite that errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. - - - - - The total number of ignored or skipped tests in the suite. - - - - - Time taken (in seconds) to execute the tests in the suite - - - - - - - - - diff --git a/tests/Makefile b/tests/Makefile index 177688c..eb941e2 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,25 +1,19 @@ -SBY_FILES=$(wildcard *.sby) -SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=)) -CHECK_PY_FILES=$(wildcard *.check.py) -CHECK_PY_TASKS=$(addprefix check_,$(CHECK_PY_FILES:.check.py=)) -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 +test: -.PHONY: test validate_junit scripted +.PHONY: test clean refresh help -test: $(JUNIT_TESTS) $(CHECK_PY_TASKS) +help: + @cat make/help.txt -test_%: %.sby FORCE - python3 ../sbysrc/sby.py -f $< +export SBY_WORKDIR_GITIGNORE=1 +export SBY_MAIN=$(realpath $(dir $(firstword $(MAKEFILE_LIST)))/../sbysrc/sby.py) -$(CHECK_PY_TASKS): check_%: %.check.py test_% - python3 $< +make/rules/collect.mk: make/collect_tests.py + python3 make/collect_tests.py -$(JUNIT_TESTS): $(SBY_TESTS) - python3 validate_junit.py $@/$@.xml +make/rules/test/%.mk: + python3 make/test_rules.py $< -scripted: - make -C scripted - -FORCE: +ifneq (help,$(MAKECMDGOALS)) +include make/rules/collect.mk +endif diff --git a/tests/aim_vs_smt2_nonzero_start_offset.sby b/tests/aim_vs_smt2_nonzero_start_offset.sby deleted file mode 100644 index 4309551..0000000 --- a/tests/aim_vs_smt2_nonzero_start_offset.sby +++ /dev/null @@ -1,33 +0,0 @@ -[tasks] -bmc -prove - -[options] -bmc: mode bmc -prove: mode prove -expect fail -wait on - -[engines] -bmc: abc bmc3 -bmc: abc sim3 -prove: aiger avy -prove: aiger suprove -prove: abc pdr - -[script] -read -sv test.sv -prep -top test - -[file test.sv] -module test ( - input clk, - input [8:1] nonzero_offset -); - reg [7:0] counter = 0; - - always @(posedge clk) begin - if (counter == 3) assert(nonzero_offset[1]); - counter <= counter + 1; - end -endmodule diff --git a/tests/both_ex.sby b/tests/both_ex.sby deleted file mode 100644 index 8177374..0000000 --- a/tests/both_ex.sby +++ /dev/null @@ -1,22 +0,0 @@ -[tasks] -btormc bmc -pono bmc -cover - -[options] -bmc: mode bmc -cover: mode cover -depth 5 -expect pass - -[engines] -btormc: btor btormc -pono: btor pono -cover: btor btormc - -[script] -read -sv both_ex.v -prep -top test - -[files] -both_ex.v diff --git a/tests/both_ex.v b/tests/both_ex.v deleted file mode 100644 index 00d1a52..0000000 --- a/tests/both_ex.v +++ /dev/null @@ -1,25 +0,0 @@ -module test( - input clk, - input [7:0] data - ); - -localparam MAX_COUNT = 8'd111; -reg [7:0] count = 8'd0; -reg [7:0] margin = MAX_COUNT; - -always @ (posedge clk) begin - if (data > margin) begin - count <= 8'd0; - margin <= MAX_COUNT; - end else begin - count <= count + data; - margin <= margin - data; - end - - assume (data < 8'd40); - assert (count <= MAX_COUNT); - cover (count == 8'd42); - cover (count == 8'd111); -end - -endmodule diff --git a/tests/check_output.py b/tests/check_output.py deleted file mode 100644 index ab531eb..0000000 --- a/tests/check_output.py +++ /dev/null @@ -1,17 +0,0 @@ -import re - - -def line_ref(dir, filename, pattern): - with open(dir + "/src/" + filename) as file: - if isinstance(pattern, str): - pattern_re = re.compile(re.escape(pattern)) - else: - pattern_re = pattern - pattern = pattern.pattern - - for number, line in enumerate(file, 1): - if pattern_re.search(line): - # Needs to match source locations for both verilog frontends - return fr"{filename}:(?:{number}|\d+.\d+-{number}.\d+)" - - raise RuntimeError("%s: pattern `%s` not found" % (filename, pattern)) diff --git a/tests/cover.sby b/tests/cover.sby deleted file mode 100644 index 894cfe1..0000000 --- a/tests/cover.sby +++ /dev/null @@ -1,13 +0,0 @@ -[options] -mode cover -expect pass - -[engines] -btor btormc - -[script] -read -formal cover.sv -prep -top top - -[files] -cover.sv diff --git a/tests/cover.sv b/tests/cover.sv deleted file mode 100644 index 478ce36..0000000 --- a/tests/cover.sv +++ /dev/null @@ -1,17 +0,0 @@ -module top ( - input clk, - input [7:0] din -); - reg [31:0] state = 0; - - always @(posedge clk) begin - state <= ((state << 5) + state) ^ din; - end - -`ifdef FORMAL - always @(posedge clk) begin - cover (state == 'd 12345678); - cover (state == 'h 12345678); - end -`endif -endmodule diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby deleted file mode 100644 index 391e0a8..0000000 --- a/tests/cover_fail.sby +++ /dev/null @@ -1,31 +0,0 @@ -[options] -mode cover -depth 5 -expect pass,fail - -[engines] -smtbmc boolector - -[script] -read -sv test.v -prep -top test - -[file test.v] -module test( -input clk, -input rst, -output reg [3:0] count -); - -initial assume (rst == 1'b1); - -always @(posedge clk) begin -if (rst) - count <= 4'b0; -else - count <= count + 1'b1; - -cover (count == 0 && !rst); -cover (count == 4'd11 && !rst); -end -endmodule diff --git a/tests/demo.sby b/tests/demo.sby deleted file mode 100644 index bc40cd6..0000000 --- a/tests/demo.sby +++ /dev/null @@ -1,19 +0,0 @@ -[tasks] -btormc -pono - -[options] -mode bmc -depth 100 -expect fail - -[engines] -btormc: btor btormc -pono: btor pono - -[script] -read -formal demo.sv -prep -top demo - -[files] -demo.sv diff --git a/tests/demo.sv b/tests/demo.sv deleted file mode 100644 index 240ea1d..0000000 --- a/tests/demo.sv +++ /dev/null @@ -1,19 +0,0 @@ -module demo ( - input clk, - output reg [5:0] counter -); - initial counter = 0; - - always @(posedge clk) begin - if (counter == 15) - counter <= 0; - else - counter <= counter + 1; - end - -`ifdef FORMAL - always @(posedge clk) begin - assert (counter < 7); - end -`endif -endmodule diff --git a/tests/invalid_ff_dcinit_merge.sby b/tests/invalid_ff_dcinit_merge.sby deleted file mode 100644 index a23d8f0..0000000 --- a/tests/invalid_ff_dcinit_merge.sby +++ /dev/null @@ -1,29 +0,0 @@ -[options] -mode bmc -depth 4 -expect fail - -[engines] -smtbmc - -[script] -read -formal top.sv -prep -top top - -[file top.sv] -module top( -input clk, d -); - -reg q1; -reg q2; - -always @(posedge clk) begin - q1 <= d; - q2 <= d; -end; - -// q1 and q2 are unconstrained in the initial state, so this should fail -always @(*) assert(q1 == q2); - -endmodule diff --git a/tests/junit/JUnit.xsd b/tests/junit/JUnit.xsd new file mode 100644 index 0000000..7a5f184 --- /dev/null +++ b/tests/junit/JUnit.xsd @@ -0,0 +1,232 @@ + + + + JUnit test result schema for the Apache Ant JUnit and JUnitReport tasks +Copyright © 2011, Windy Road Technology Pty. Limited +The Apache Ant JUnit XML Schema is distributed under the terms of the Apache License Version 2.0 http://www.apache.org/licenses/ +Permission to waive conditions of this license may be requested from Windy Road Support (http://windyroad.org/support). + + + + + + + + + + Contains an aggregation of testsuite results + + + + + + + + + + Derived from testsuite/@name in the non-aggregated documents + + + + + Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite + + + + + + + + + + + + Contains the results of exexuting a testsuite + + + + + Properties (e.g., environment settings) set during test execution + + + + + + + + + + + + + + + + + + + + + + + + + Indicates that the test errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. Contains as a text node relevant data for the error, e.g., a stack trace + + + + + + + The error message. e.g., if a java exception is thrown, the return value of getMessage() + + + + + The type of error that occured. e.g., if a java execption is thrown the full class name of the exception. + + + + + + + + + Indicates that the test failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals. Contains as a text node relevant data for the failure, e.g., a stack trace + + + + + + + The message specified in the assert + + + + + The type of the assert. + + + + + + + + + + Name of the test method + + + + + Full class name for the class the test method is in. + + + + + 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 + + + + + + + Data that was written to standard out while the test was executed + + + + + + + + + + Data that was written to standard error while the test was executed + + + + + + + + + + + Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents + + + + + + + + + + when the test was executed. Timezone may not be specified. + + + + + Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined. + + + + + + + + + + The total number of tests in the suite + + + + + The total number of tests in the suite that failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals + + + + + The total number of tests in the suite that errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. + + + + + The total number of ignored or skipped tests in the suite. + + + + + Time taken (in seconds) to execute the tests in the suite + + + + + + + + + diff --git a/tests/junit/Makefile b/tests/junit/Makefile new file mode 100644 index 0000000..dd89403 --- /dev/null +++ b/tests/junit/Makefile @@ -0,0 +1,2 @@ +SUBDIR=junit +include ../make/subdir.mk diff --git a/tests/junit/junit_assert.sby b/tests/junit/junit_assert.sby new file mode 100644 index 0000000..e13f375 --- /dev/null +++ b/tests/junit/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/junit_assert.sh b/tests/junit/junit_assert.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_assert.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit/junit_cover.sby b/tests/junit/junit_cover.sby new file mode 100644 index 0000000..53747ba --- /dev/null +++ b/tests/junit/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/junit_cover.sh b/tests/junit/junit_cover.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_cover.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit/junit_expect.sby b/tests/junit/junit_expect.sby new file mode 100644 index 0000000..63d65a6 --- /dev/null +++ b/tests/junit/junit_expect.sby @@ -0,0 +1,16 @@ +[options] +mode bmc +depth 1 +expect fail,timeout + +[engines] +smtbmc + +[script] +read -formal foo.v +prep -top foo + +[file foo.v] +module foo; +always_comb assert(1); +endmodule diff --git a/tests/junit/junit_expect.sh b/tests/junit/junit_expect.sh new file mode 100644 index 0000000..cb66b10 --- /dev/null +++ b/tests/junit/junit_expect.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +! python3 $SBY_MAIN -f $SBY_FILE $TASK +grep '' $WORKDIR/$WORKDIR.xml diff --git a/tests/junit/junit_nocodeloc.sby b/tests/junit/junit_nocodeloc.sby new file mode 100644 index 0000000..5d2afc8 --- /dev/null +++ b/tests/junit/junit_nocodeloc.sby @@ -0,0 +1,20 @@ +[options] +mode bmc + +expect fail + +[engines] +smtbmc boolector + +[script] +read -sv multi_assert.v +prep -top test +setattr -unset src + +[file multi_assert.v] +module test(); +always @* begin +assert (1); +assert (0); +end +endmodule diff --git a/tests/junit/junit_nocodeloc.sh b/tests/junit/junit_nocodeloc.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_nocodeloc.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit/junit_timeout_error.sby b/tests/junit/junit_timeout_error.sby new file mode 100644 index 0000000..551de49 --- /dev/null +++ b/tests/junit/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 diff --git a/tests/junit/junit_timeout_error.sh b/tests/junit/junit_timeout_error.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_timeout_error.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit/validate_junit.py b/tests/junit/validate_junit.py new file mode 100644 index 0000000..c1c0573 --- /dev/null +++ b/tests/junit/validate_junit.py @@ -0,0 +1,19 @@ +from xmlschema import XMLSchema, XMLSchemaValidationError +import argparse + +def main(): + parser = argparse.ArgumentParser(description="Validate JUnit output") + parser.add_argument('xml') + parser.add_argument('--xsd', default="JUnit.xsd") + + args = parser.parse_args() + + schema = XMLSchema(args.xsd) + try: + schema.validate(args.xml) + except XMLSchemaValidationError as e: + print(e) + exit(1) + +if __name__ == '__main__': + main() diff --git a/tests/junit_assert.sby b/tests/junit_assert.sby deleted file mode 100644 index e13f375..0000000 --- a/tests/junit_assert.sby +++ /dev/null @@ -1,38 +0,0 @@ -[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 deleted file mode 100644 index 53747ba..0000000 --- a/tests/junit_cover.sby +++ /dev/null @@ -1,43 +0,0 @@ -[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_nocodeloc.sby b/tests/junit_nocodeloc.sby deleted file mode 100644 index 5d2afc8..0000000 --- a/tests/junit_nocodeloc.sby +++ /dev/null @@ -1,20 +0,0 @@ -[options] -mode bmc - -expect fail - -[engines] -smtbmc boolector - -[script] -read -sv multi_assert.v -prep -top test -setattr -unset src - -[file multi_assert.v] -module test(); -always @* begin -assert (1); -assert (0); -end -endmodule diff --git a/tests/junit_timeout_error.sby b/tests/junit_timeout_error.sby deleted file mode 100644 index 551de49..0000000 --- a/tests/junit_timeout_error.sby +++ /dev/null @@ -1,42 +0,0 @@ -[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 diff --git a/tests/keepgoing/Makefile b/tests/keepgoing/Makefile new file mode 100644 index 0000000..0727e8b --- /dev/null +++ b/tests/keepgoing/Makefile @@ -0,0 +1,2 @@ +SUBDIR=keepgoing +include ../make/subdir.mk diff --git a/tests/keepgoing/check_output.py b/tests/keepgoing/check_output.py new file mode 100644 index 0000000..ab531eb --- /dev/null +++ b/tests/keepgoing/check_output.py @@ -0,0 +1,17 @@ +import re + + +def line_ref(dir, filename, pattern): + with open(dir + "/src/" + filename) as file: + if isinstance(pattern, str): + pattern_re = re.compile(re.escape(pattern)) + else: + pattern_re = pattern + pattern = pattern.pattern + + for number, line in enumerate(file, 1): + if pattern_re.search(line): + # Needs to match source locations for both verilog frontends + return fr"{filename}:(?:{number}|\d+.\d+-{number}.\d+)" + + raise RuntimeError("%s: pattern `%s` not found" % (filename, pattern)) diff --git a/tests/keepgoing/keepgoing_multi_step.py b/tests/keepgoing/keepgoing_multi_step.py new file mode 100644 index 0000000..c724c66 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.py @@ -0,0 +1,31 @@ +import sys +from check_output import * + +src = "keepgoing_multi_step.sv" + +workdir = sys.argv[1] + +assert_0 = line_ref(workdir, src, "assert(0)") +step_3_7 = line_ref(workdir, src, "step 3,7") +step_5 = line_ref(workdir, src, "step 5") +step_7 = line_ref(workdir, src, "step 7") + +log = open(workdir + "/logfile.txt").read() +log_per_trace = log.split("Writing trace to VCD file")[:-1] + +assert len(log_per_trace) == 4 + + +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) + +for i in range(1, 4): + assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) + + +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) +assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) + +pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd" +assert re.search(pattern, open(f"{workdir}/{workdir}.xml").read()) diff --git a/tests/keepgoing/keepgoing_multi_step.sby b/tests/keepgoing/keepgoing_multi_step.sby new file mode 100644 index 0000000..b9b0ba5 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.sby @@ -0,0 +1,18 @@ +[tasks] +bmc +prove + +[options] +bmc: mode bmc +prove: mode prove +expect fail + +[engines] +smtbmc --keep-going boolector + +[script] +read -sv keepgoing_multi_step.sv +prep -top test + +[files] +keepgoing_multi_step.sv diff --git a/tests/keepgoing/keepgoing_multi_step.sh b/tests/keepgoing/keepgoing_multi_step.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing/keepgoing_multi_step.sv b/tests/keepgoing/keepgoing_multi_step.sv new file mode 100644 index 0000000..8d5d8e3 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.sv @@ -0,0 +1,22 @@ +module test ( + input clk, a +); + reg [7:0] counter = 0; + + always @(posedge clk) begin + counter <= counter + 1; + end + + always @(posedge clk) begin + assert(0); + if (counter == 3 || counter == 7) begin + assert(a); // step 3,7 + end + if (counter == 5) begin + assert(a); // step 5 + end + if (counter == 7) begin + assert(a); // step 7 + end + end +endmodule diff --git a/tests/keepgoing/keepgoing_same_step.py b/tests/keepgoing/keepgoing_same_step.py new file mode 100644 index 0000000..e273916 --- /dev/null +++ b/tests/keepgoing/keepgoing_same_step.py @@ -0,0 +1,19 @@ +import sys +from check_output import * + +workdir = sys.argv[1] +src = "keepgoing_same_step.sv" + +assert_a = line_ref(workdir, src, "assert(a)") +assert_not_a = line_ref(workdir, src, "assert(!a)") +assert_0 = line_ref(workdir, src, "assert(0)") + +log = open(workdir + "/logfile.txt").read() +log_per_trace = log.split("Writing trace to VCD file")[:-1] + +assert len(log_per_trace) == 2 + +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) +assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[1], re.M) diff --git a/tests/keepgoing/keepgoing_same_step.sby b/tests/keepgoing/keepgoing_same_step.sby new file mode 100644 index 0000000..d344dcc --- /dev/null +++ b/tests/keepgoing/keepgoing_same_step.sby @@ -0,0 +1,13 @@ +[options] +mode bmc +expect fail + +[engines] +smtbmc --keep-going boolector + +[script] +read -sv keepgoing_same_step.sv +prep -top test + +[files] +keepgoing_same_step.sv diff --git a/tests/keepgoing/keepgoing_same_step.sh b/tests/keepgoing/keepgoing_same_step.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_same_step.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing/keepgoing_same_step.sv b/tests/keepgoing/keepgoing_same_step.sv new file mode 100644 index 0000000..98fe6d0 --- /dev/null +++ b/tests/keepgoing/keepgoing_same_step.sv @@ -0,0 +1,17 @@ +module test ( + input clk, a +); + reg [7:0] counter = 0; + + always @(posedge clk) begin + counter <= counter + 1; + end + + always @(posedge clk) begin + if (counter == 3) begin + assert(a); + assert(!a); + assert(0); + end + end +endmodule diff --git a/tests/keepgoing/keepgoing_smtc.py b/tests/keepgoing/keepgoing_smtc.py new file mode 100644 index 0000000..e0fd27d --- /dev/null +++ b/tests/keepgoing/keepgoing_smtc.py @@ -0,0 +1,25 @@ +import sys +from check_output import * + +workdir = sys.argv[1] +src = "keepgoing_same_step.sv" + +assert_a = line_ref(workdir, src, "assert(a)") +assert_not_a = line_ref(workdir, src, "assert(!a)") +assert_0 = line_ref(workdir, src, "assert(0)") + +assert_false = line_ref(workdir, "extra.smtc", "assert false") +assert_distinct = line_ref(workdir, "extra.smtc", "assert (distinct") + +log = open(workdir + "/logfile.txt").read() +log_per_trace = log.split("Writing trace to VCD file")[:-1] + +assert len(log_per_trace) == 4 + +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M) + +assert re.search(r"Assert src/%s failed: false" % assert_false, log_per_trace[0], re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[1], re.M) +assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[2], re.M) +assert re.search(r"Assert src/%s failed: \(distinct" % assert_distinct, log_per_trace[3], re.M) diff --git a/tests/keepgoing/keepgoing_smtc.sby b/tests/keepgoing/keepgoing_smtc.sby new file mode 100644 index 0000000..a4cc762 --- /dev/null +++ b/tests/keepgoing/keepgoing_smtc.sby @@ -0,0 +1,19 @@ +[options] +mode bmc +expect fail + +[engines] +smtbmc --keep-going boolector -- --smtc src/extra.smtc + +[script] +read -sv keepgoing_same_step.sv +prep -top test + +[files] +keepgoing_same_step.sv + +[file extra.smtc] +state 2 +assert false +always +assert (distinct [counter] #b00000111) diff --git a/tests/keepgoing/keepgoing_smtc.sh b/tests/keepgoing/keepgoing_smtc.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_smtc.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing_multi_step.check.py b/tests/keepgoing_multi_step.check.py deleted file mode 100644 index 78c713f..0000000 --- a/tests/keepgoing_multi_step.check.py +++ /dev/null @@ -1,29 +0,0 @@ -from check_output import * - -src = "keepgoing_multi_step.sv" - -for task in ["keepgoing_multi_step_bmc", "keepgoing_multi_step_prove"]: - assert_0 = line_ref(task, src, "assert(0)") - step_3_7 = line_ref(task, src, "step 3,7") - step_5 = line_ref(task, src, "step 5") - step_7 = line_ref(task, src, "step 7") - - log = open(task + "/logfile.txt").read() - log_per_trace = log.split("Writing trace to VCD file")[:-1] - - assert len(log_per_trace) == 4 - - - assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) - - for i in range(1, 4): - assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) - - - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) - assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) - - pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd" - assert re.search(pattern, open(f"{task}/{task}.xml").read()) diff --git a/tests/keepgoing_multi_step.sby b/tests/keepgoing_multi_step.sby deleted file mode 100644 index b9b0ba5..0000000 --- a/tests/keepgoing_multi_step.sby +++ /dev/null @@ -1,18 +0,0 @@ -[tasks] -bmc -prove - -[options] -bmc: mode bmc -prove: mode prove -expect fail - -[engines] -smtbmc --keep-going boolector - -[script] -read -sv keepgoing_multi_step.sv -prep -top test - -[files] -keepgoing_multi_step.sv diff --git a/tests/keepgoing_multi_step.sv b/tests/keepgoing_multi_step.sv deleted file mode 100644 index 8d5d8e3..0000000 --- a/tests/keepgoing_multi_step.sv +++ /dev/null @@ -1,22 +0,0 @@ -module test ( - input clk, a -); - reg [7:0] counter = 0; - - always @(posedge clk) begin - counter <= counter + 1; - end - - always @(posedge clk) begin - assert(0); - if (counter == 3 || counter == 7) begin - assert(a); // step 3,7 - end - if (counter == 5) begin - assert(a); // step 5 - end - if (counter == 7) begin - assert(a); // step 7 - end - end -endmodule diff --git a/tests/keepgoing_same_step.check.py b/tests/keepgoing_same_step.check.py deleted file mode 100644 index 35cd314..0000000 --- a/tests/keepgoing_same_step.check.py +++ /dev/null @@ -1,18 +0,0 @@ -from check_output import * - -task = "keepgoing_same_step" -src = "keepgoing_same_step.sv" - -assert_a = line_ref(task, src, "assert(a)") -assert_not_a = line_ref(task, src, "assert(!a)") -assert_0 = line_ref(task, src, "assert(0)") - -log = open(task + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to VCD file")[:-1] - -assert len(log_per_trace) == 2 - -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) -assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[1], re.M) diff --git a/tests/keepgoing_same_step.sby b/tests/keepgoing_same_step.sby deleted file mode 100644 index d344dcc..0000000 --- a/tests/keepgoing_same_step.sby +++ /dev/null @@ -1,13 +0,0 @@ -[options] -mode bmc -expect fail - -[engines] -smtbmc --keep-going boolector - -[script] -read -sv keepgoing_same_step.sv -prep -top test - -[files] -keepgoing_same_step.sv diff --git a/tests/keepgoing_same_step.sv b/tests/keepgoing_same_step.sv deleted file mode 100644 index 98fe6d0..0000000 --- a/tests/keepgoing_same_step.sv +++ /dev/null @@ -1,17 +0,0 @@ -module test ( - input clk, a -); - reg [7:0] counter = 0; - - always @(posedge clk) begin - counter <= counter + 1; - end - - always @(posedge clk) begin - if (counter == 3) begin - assert(a); - assert(!a); - assert(0); - end - end -endmodule diff --git a/tests/keepgoing_smtc.check.py b/tests/keepgoing_smtc.check.py deleted file mode 100644 index 5749e3f..0000000 --- a/tests/keepgoing_smtc.check.py +++ /dev/null @@ -1,24 +0,0 @@ -from check_output import * - -task = "keepgoing_smtc" -src = "keepgoing_same_step.sv" - -assert_a = line_ref(task, src, "assert(a)") -assert_not_a = line_ref(task, src, "assert(!a)") -assert_0 = line_ref(task, src, "assert(0)") - -assert_false = line_ref(task, "extra.smtc", "assert false") -assert_distinct = line_ref(task, "extra.smtc", "assert (distinct") - -log = open(task + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to VCD file")[:-1] - -assert len(log_per_trace) == 4 - -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M) - -assert re.search(r"Assert src/%s failed: false" % assert_false, log_per_trace[0], re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[1], re.M) -assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[2], re.M) -assert re.search(r"Assert src/%s failed: \(distinct" % assert_distinct, log_per_trace[3], re.M) diff --git a/tests/keepgoing_smtc.sby b/tests/keepgoing_smtc.sby deleted file mode 100644 index a4cc762..0000000 --- a/tests/keepgoing_smtc.sby +++ /dev/null @@ -1,19 +0,0 @@ -[options] -mode bmc -expect fail - -[engines] -smtbmc --keep-going boolector -- --smtc src/extra.smtc - -[script] -read -sv keepgoing_same_step.sv -prep -top test - -[files] -keepgoing_same_step.sv - -[file extra.smtc] -state 2 -assert false -always -assert (distinct [counter] #b00000111) diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py new file mode 100644 index 0000000..cf782b9 --- /dev/null +++ b/tests/make/collect_tests.py @@ -0,0 +1,47 @@ +from pathlib import Path +import re + +tests = [] +checked_dirs = [] + +SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./]*$") + +def collect(path): + # don't pick up any paths that need escaping nor any sby workdirs + if not SAFE_PATH.match(str(path)) or (path / "config.sby").exists(): + return + + checked_dirs.append(path) + for entry in path.glob("*.sby"): + filename = str(entry) + if not SAFE_PATH.match(filename): + continue + if not re.match(r"^[a-zA-Z0-9_./]*$", filename): + print(f"skipping {filename!r}, use only [a-zA-Z0-9_./] in filenames") + continue + tests.append(entry) + for entry in path.glob("*"): + if entry.is_dir(): + collect(entry) + + +collect(Path(".")) + +out_file = Path("make/rules/collect.mk") +out_file.parent.mkdir(exist_ok=True) + +with out_file.open("w") as output: + + + for checked_dir in checked_dirs: + print(f"{out_file}: {checked_dir}", file=output) + + for test in tests: + print(f"make/rules/test/{test}.mk: {test}", file=output) + for ext in [".sh", ".py"]: + script_file = test.parent / (test.stem + ext) + if script_file.exists(): + print(f"make/rules/test/{test}.mk: {script_file}", file=output) + print(f"make/rules/test/{test}.mk: make/test_rules.py", file=output) + for test in tests: + print(f"-include make/rules/test/{test}.mk", file=output) diff --git a/tests/make/help.txt b/tests/make/help.txt new file mode 100644 index 0000000..c840c4c --- /dev/null +++ b/tests/make/help.txt @@ -0,0 +1,20 @@ +make test: + run all tests (default) + +make clean: + remove all sby workdirs + +make test[_m_][_e_][_s_]: + run all tests that use a specific mode, engine and solver + +make : + run the test for .sby + +make refresh: + do nothing apart from refreshing generated make rules + +make help: + show this help + +running make in a subdirectory or prefixing the target with the subdirectory +limits the test selection to that directory diff --git a/tests/make/subdir.mk b/tests/make/subdir.mk new file mode 100644 index 0000000..b1f367a --- /dev/null +++ b/tests/make/subdir.mk @@ -0,0 +1,15 @@ +test: + @$(MAKE) -C .. $(SUBDIR)/$@ + +.PHONY: test refresh IMPLICIT_PHONY + +IMPLICIT_PHONY: + +refresh: + @$(MAKE) -C .. refresh + +help: + @$(MAKE) -C .. help + +%: IMPLICIT_PHONY + @$(MAKE) -C .. $(SUBDIR)/$@ diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py new file mode 100644 index 0000000..1ad49ba --- /dev/null +++ b/tests/make/test_rules.py @@ -0,0 +1,135 @@ +import shutil +import sys +import os +import subprocess +import json +from pathlib import Path + + +sby_file = Path(sys.argv[1]) +sby_dir = sby_file.parent + + +taskinfo = json.loads( + subprocess.check_output( + [sys.executable, os.getenv("SBY_MAIN"), "--dumptaskinfo", sby_file] + ) +) + + +def parse_engine(engine): + engine, *args = engine + default_solvers = {"smtbmc": "yices"} + for arg in args: + if not arg.startswith("-"): + return engine, arg + return engine, default_solvers.get(engine) + + +REQUIRED_TOOLS = { + ("smtbmc", "yices"): ["yices-smt2"], + ("smtbmc", "z3"): ["z3"], + ("smtbmc", "cvc4"): ["cvc4"], + ("smtbmc", "mathsat"): ["mathsat"], + ("smtbmc", "boolector"): ["boolector"], + ("smtbmc", "bitwuzla"): ["bitwuzla"], + ("smtbmc", "abc"): ["yosys-abc"], + ("aiger", "suprove"): ["suprove"], + ("aiger", "avy"): ["avy"], + ("aiger", "aigbmc"): ["aigbmc"], + ("btor", "btormc"): ["btormc"], + ("btor", "pono"): ["pono"], +} + +rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk") +rules_file.parent.mkdir(exist_ok=True, parents=True) + +with rules_file.open("w") as rules: + name = str(sby_dir / sby_file.stem) + + for task, info in taskinfo.items(): + target = name + workdirname = sby_file.stem + if task: + target += f"_{task}" + workdirname += f"_{task}" + + engines = set() + solvers = set() + engine_solvers = set() + + required_tools = set() + + for engine in info["engines"]: + engine, solver = parse_engine(engine) + engines.add(engine) + required_tools.update(REQUIRED_TOOLS.get((engine, solver), ())) + if solver: + solvers.add(solver) + engine_solvers.add((engine, solver)) + + print(f".PHONY: {target}", file=rules) + print(f"{target}:", file=rules) + + shell_script = sby_dir / f"{sby_file.stem}.sh" + + missing_tools = sorted( + f"`{tool}`" for tool in required_tools if shutil.which(tool) is None + ) + + if missing_tools: + print( + f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo", + file=rules, + ) + + elif shell_script.exists(): + print( + f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}", + file=rules, + ) + else: + print( + f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}", + file=rules, + ) + + print(f".PHONY: clean-{target}", file=rules) + print(f"clean-{target}:", file=rules) + print(f"\trm -rf {target}", file=rules) + + test_groups = [] + + mode = info["mode"] + + test_groups.append(f"test_m_{mode}") + + for engine in sorted(engines): + test_groups.append(f"test_e_{engine}") + test_groups.append(f"test_m_{mode}_e_{engine}") + + for solver in sorted(solvers): + test_groups.append(f"test_s_{solver}") + test_groups.append(f"test_m_{mode}_s_{solver}") + + for engine, solver in sorted(engine_solvers): + test_groups.append(f"test_e_{engine}_s_{solver}") + test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}") + + prefix = "" + + for part in [*sby_dir.parts, ""]: + print(f".PHONY: {prefix}clean {prefix}test", file=rules) + print(f"{prefix}clean: clean-{target}", file=rules) + print(f"{prefix}test: {target}", file=rules) + + for test_group in test_groups: + print(f".PHONY: {prefix}{test_group}", file=rules) + print(f"{prefix}{test_group}: {target}", file=rules) + prefix += f"{part}/" + + tasks = [task for task in taskinfo.keys() if task] + + if tasks: + print(f".PHONY: {name}", file=rules) + print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules) diff --git a/tests/memory.sby b/tests/memory.sby deleted file mode 100644 index fa3d1d6..0000000 --- a/tests/memory.sby +++ /dev/null @@ -1,19 +0,0 @@ -[tasks] -btormc -pono - -[options] -mode bmc -depth 10 -expect fail - -[engines] -btormc: btor btormc -pono: btor pono - -[script] -read -formal memory.sv -prep -top testbench - -[files] -memory.sv diff --git a/tests/memory.sv b/tests/memory.sv deleted file mode 100644 index fdb9ca4..0000000 --- a/tests/memory.sv +++ /dev/null @@ -1,60 +0,0 @@ -module testbench ( - input clk, wen, - input [9:0] addr, - input [7:0] wdata, - output [7:0] rdata -); - memory uut ( - .clk (clk ), - .wen (wen ), - .addr (addr ), - .wdata(wdata), - .rdata(rdata) - ); - - (* anyconst *) reg [9:0] test_addr; - reg test_data_valid = 0; - reg [7:0] test_data; - - always @(posedge clk) begin - if (addr == test_addr) begin - if (wen) begin - test_data <= wdata; - test_data_valid <= 1; - end - if (test_data_valid) begin - assert(test_data == rdata); - end - end - end -endmodule - -module memory ( - input clk, wen, - input [9:0] addr, - input [7:0] wdata, - output [7:0] rdata -); - reg [7:0] bank0 [0:255]; - reg [7:0] bank1 [0:255]; - reg [7:0] bank2 [0:255]; - reg [7:0] bank3 [0:255]; - - wire [1:0] mem_sel = addr[9:8]; - wire [7:0] mem_addr = addr[7:0]; - - always @(posedge clk) begin - case (mem_sel) - 0: if (wen) bank0[mem_addr] <= wdata; - 1: if (wen) bank1[mem_addr] <= wdata; - 2: if (wen) bank1[mem_addr] <= wdata; // BUG: Should assign to bank2 - 3: if (wen) bank3[mem_addr] <= wdata; - endcase - end - - assign rdata = - mem_sel == 0 ? bank0[mem_addr] : - mem_sel == 1 ? bank1[mem_addr] : - mem_sel == 2 ? bank2[mem_addr] : - mem_sel == 3 ? bank3[mem_addr] : 'bx; -endmodule diff --git a/tests/mixed.sby b/tests/mixed.sby deleted file mode 100644 index 2d9467e..0000000 --- a/tests/mixed.sby +++ /dev/null @@ -1,21 +0,0 @@ -[tasks] -cover -btormc bmc -pono bmc - -[options] -cover: mode cover -bmc: mode bmc -bmc: depth 1 - -[engines] -cover: btor btormc -btormc: btor btormc -pono: btor pono - -[script] -read -formal mixed.v -prep -top test - -[files] -mixed.v diff --git a/tests/mixed.v b/tests/mixed.v deleted file mode 100644 index fa3cf2c..0000000 --- a/tests/mixed.v +++ /dev/null @@ -1,17 +0,0 @@ -module test (input CP, CN, CX, input A, B, output reg XP, XN, YP, YN); - always @* begin - assume (A || B); - assume (!A || !B); - assert (A != B); - cover (A); - cover (B); - end - always @(posedge CP) - XP <= A; - always @(negedge CN) - XN <= B; - always @(posedge CX) - YP <= A; - always @(negedge CX) - YN <= B; -endmodule diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby deleted file mode 100644 index 883181a..0000000 --- a/tests/multi_assert.sby +++ /dev/null @@ -1,24 +0,0 @@ -[tasks] -btormc -pono - -[options] -mode bmc -depth 5 -expect fail - -[engines] -btormc: btor btormc -pono: btor pono - -[script] -read -sv multi_assert.v -prep -top test - -[file multi_assert.v] -module test(); -always @* begin -assert (1); -assert (0); -end -endmodule diff --git a/tests/preunsat.sby b/tests/preunsat.sby deleted file mode 100644 index 98255c6..0000000 --- a/tests/preunsat.sby +++ /dev/null @@ -1,22 +0,0 @@ -[tasks] -btormc -yices - -[options] -mode bmc -yices: expect error -btormc: expect pass - -[engines] -btormc: btor btormc -yices: smtbmc yices - -[script] -read -sv test.sv -prep -top test - -[file test.sv] -module test(input foo); -always @* assume(0); -always @* assert(foo); -endmodule diff --git a/tests/prv32fmcmp.sby b/tests/prv32fmcmp.sby deleted file mode 100644 index 2412eb8..0000000 --- a/tests/prv32fmcmp.sby +++ /dev/null @@ -1,21 +0,0 @@ -[tasks] -btormc -pono - -[options] -mode bmc -expect fail - -[engines] -btormc: btor btormc -pono: btor pono - -[script] -read -noverific -read -sv picorv32.v -read -sv prv32fmcmp.v -prep -top prv32fmcmp - -[files] -../extern/picorv32.v -prv32fmcmp.v diff --git a/tests/prv32fmcmp.v b/tests/prv32fmcmp.v deleted file mode 100644 index 5116375..0000000 --- a/tests/prv32fmcmp.v +++ /dev/null @@ -1,73 +0,0 @@ -module prv32fmcmp ( - input clock, - input resetn, - output mem_valid_a, mem_valid_b, - output mem_instr_a, mem_instr_b, - input mem_ready_a, mem_ready_b, - output [31:0] mem_addr_a, mem_addr_b, - output [31:0] mem_wdata_a, mem_wdata_b, - output [ 3:0] mem_wstrb_a, mem_wstrb_b, - input [31:0] mem_rdata_a, mem_rdata_b -); - picorv32 #( - .REGS_INIT_ZERO(1), - .COMPRESSED_ISA(1) - ) prv32_a ( - .clk (clock ), - .resetn (resetn ), - .mem_valid (mem_valid_a), - .mem_instr (mem_instr_a), - .mem_ready (mem_ready_a), - .mem_addr (mem_addr_a ), - .mem_wdata (mem_wdata_a), - .mem_wstrb (mem_wstrb_a), - .mem_rdata (mem_rdata_a) - ); - - picorv32 #( - .REGS_INIT_ZERO(1), - .COMPRESSED_ISA(1) - ) prv32_b ( - .clk (clock ), - .resetn (resetn ), - .mem_valid (mem_valid_b), - .mem_instr (mem_instr_b), - .mem_ready (mem_ready_b), - .mem_addr (mem_addr_b ), - .mem_wdata (mem_wdata_b), - .mem_wstrb (mem_wstrb_b), - .mem_rdata (mem_rdata_b) - ); - - reg [31:0] rom [0:255]; - - integer mem_access_cnt_a = 0; - integer mem_access_cnt_b = 0; - - always @* begin - assume(resetn == !$initstate); - - if (resetn) begin - // only consider programs without data memory read/write - if (mem_valid_a) assume(mem_instr_a); - if (mem_valid_b) assume(mem_instr_b); - - // when the access cnt matches, the addresses must match - if (mem_valid_a && mem_valid_b && mem_access_cnt_a == mem_access_cnt_b) begin - assert(mem_addr_a == mem_addr_b); - end - - // hook up to memory - assume(mem_rdata_a == rom[mem_addr_a[9:2]]); - assume(mem_rdata_b == rom[mem_addr_b[9:2]]); - end - - // it will pass when this is enabled - //assume(mem_ready_a == mem_ready_b); - end - - always @(posedge clock) begin - mem_access_cnt_a <= mem_access_cnt_a + (resetn && mem_valid_a && mem_ready_a); - mem_access_cnt_b <= mem_access_cnt_b + (resetn && mem_valid_b && mem_ready_b); - end -endmodule diff --git a/tests/redxor.sby b/tests/redxor.sby deleted file mode 100644 index 0746861..0000000 --- a/tests/redxor.sby +++ /dev/null @@ -1,13 +0,0 @@ -[options] -mode cover -expect pass - -[engines] -btor btormc - -[script] -read -formal redxor.v -prep -top test - -[files] -redxor.v diff --git a/tests/redxor.v b/tests/redxor.v deleted file mode 100644 index 3bab284..0000000 --- a/tests/redxor.v +++ /dev/null @@ -1,8 +0,0 @@ -module test(input [7:0] I, output O); -assign O = ^I; - -always @(*) begin -cover(O==1'b0); -cover(O==1'b1); -end -endmodule diff --git a/tests/regression/Makefile b/tests/regression/Makefile new file mode 100644 index 0000000..0d9b684 --- /dev/null +++ b/tests/regression/Makefile @@ -0,0 +1,2 @@ +SUBDIR=regression +include ../make/subdir.mk diff --git a/tests/regression/aim_vs_smt2_nonzero_start_offset.sby b/tests/regression/aim_vs_smt2_nonzero_start_offset.sby new file mode 100644 index 0000000..94591d7 --- /dev/null +++ b/tests/regression/aim_vs_smt2_nonzero_start_offset.sby @@ -0,0 +1,36 @@ +[tasks] +abc_bmc3 bmc +abc_sim3 bmc +aiger_avy prove +aiger_suprove prove +abc_pdr prove + +[options] +bmc: mode bmc +prove: mode prove +expect fail +wait on + +[engines] +abc_bmc3: abc bmc3 +abc_sim3: abc sim3 +aiger_avy: aiger avy +aiger_suprove: aiger suprove +abc_pdr: abc pdr + +[script] +read -sv test.sv +prep -top test + +[file test.sv] +module test ( + input clk, + input [8:1] nonzero_offset +); + reg [7:0] counter = 0; + + always @(posedge clk) begin + if (counter == 3) assert(nonzero_offset[1]); + counter <= counter + 1; + end +endmodule diff --git a/tests/regression/invalid_ff_dcinit_merge.sby b/tests/regression/invalid_ff_dcinit_merge.sby new file mode 100644 index 0000000..a23d8f0 --- /dev/null +++ b/tests/regression/invalid_ff_dcinit_merge.sby @@ -0,0 +1,29 @@ +[options] +mode bmc +depth 4 +expect fail + +[engines] +smtbmc + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top( +input clk, d +); + +reg q1; +reg q2; + +always @(posedge clk) begin + q1 <= d; + q2 <= d; +end; + +// q1 and q2 are unconstrained in the initial state, so this should fail +always @(*) assert(q1 == q2); + +endmodule diff --git a/tests/scripted/.gitignore b/tests/scripted/.gitignore deleted file mode 100644 index 6403b85..0000000 --- a/tests/scripted/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/junit_*/ diff --git a/tests/scripted/Makefile b/tests/scripted/Makefile deleted file mode 100644 index ca27199..0000000 --- a/tests/scripted/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -SH_FILES=$(wildcard *.sh) -SH_TESTS=$(addprefix test_,$(SH_FILES:.sh=)) - -test: $(SH_TESTS) - -test_%: %.sh FORCE - bash $< - -FORCE: - -.PHONY: test FORCE diff --git a/tests/scripted/junit_expect.sby b/tests/scripted/junit_expect.sby deleted file mode 100644 index 63d65a6..0000000 --- a/tests/scripted/junit_expect.sby +++ /dev/null @@ -1,16 +0,0 @@ -[options] -mode bmc -depth 1 -expect fail,timeout - -[engines] -smtbmc - -[script] -read -formal foo.v -prep -top foo - -[file foo.v] -module foo; -always_comb assert(1); -endmodule diff --git a/tests/scripted/junit_expect.sh b/tests/scripted/junit_expect.sh deleted file mode 100644 index 27b972d..0000000 --- a/tests/scripted/junit_expect.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/bash - -# this is expected to return 1 so don't use 'set -e' -python3 ../../sbysrc/sby.py -f junit_expect.sby -grep '' junit_expect/junit_expect.xml diff --git a/tests/stopfirst.sby b/tests/stopfirst.sby deleted file mode 100644 index 782f791..0000000 --- a/tests/stopfirst.sby +++ /dev/null @@ -1,16 +0,0 @@ -[options] -mode bmc -expect fail - -[engines] -btor btormc - -[script] -read -sv test.sv -prep -top test - -[file test.sv] -module test(input foo); -always @* assert(foo); -always @* assert(!foo); -endmodule diff --git a/tests/submod_props.sby b/tests/submod_props.sby deleted file mode 100644 index 9933676..0000000 --- a/tests/submod_props.sby +++ /dev/null @@ -1,33 +0,0 @@ -[tasks] -bmc -cover -flatten - -[options] -bmc: mode bmc -cover: mode cover -flatten: mode bmc - -expect fail - -[engines] -smtbmc boolector - -[script] -read -sv test.sv -prep -top top -flatten: flatten - -[file test.sv] -module test(input foo); -always @* assert(foo); -always @* assert(!foo); -always @* cover(foo); -always @* cover(!foo); -endmodule - -module top(); -test test_i ( -.foo(1'b1) -); -endmodule diff --git a/tests/unsorted/2props1trace.sby b/tests/unsorted/2props1trace.sby new file mode 100644 index 0000000..8f51fde --- /dev/null +++ b/tests/unsorted/2props1trace.sby @@ -0,0 +1,22 @@ +[options] +mode bmc +depth 1 +expect fail + +[engines] +smtbmc + +[script] +read -sv top.sv +prep -top top + +[file top.sv] +module top( +input foo, +input bar +); +always @(*) begin + assert (foo); + assert (bar); +end +endmodule diff --git a/tests/unsorted/Makefile b/tests/unsorted/Makefile new file mode 100644 index 0000000..61c3a6f --- /dev/null +++ b/tests/unsorted/Makefile @@ -0,0 +1,2 @@ +SUBDIR=unsorted +include ../make/subdir.mk diff --git a/tests/unsorted/both_ex.sby b/tests/unsorted/both_ex.sby new file mode 100644 index 0000000..8177374 --- /dev/null +++ b/tests/unsorted/both_ex.sby @@ -0,0 +1,22 @@ +[tasks] +btormc bmc +pono bmc +cover + +[options] +bmc: mode bmc +cover: mode cover +depth 5 +expect pass + +[engines] +btormc: btor btormc +pono: btor pono +cover: btor btormc + +[script] +read -sv both_ex.v +prep -top test + +[files] +both_ex.v diff --git a/tests/unsorted/both_ex.v b/tests/unsorted/both_ex.v new file mode 100644 index 0000000..00d1a52 --- /dev/null +++ b/tests/unsorted/both_ex.v @@ -0,0 +1,25 @@ +module test( + input clk, + input [7:0] data + ); + +localparam MAX_COUNT = 8'd111; +reg [7:0] count = 8'd0; +reg [7:0] margin = MAX_COUNT; + +always @ (posedge clk) begin + if (data > margin) begin + count <= 8'd0; + margin <= MAX_COUNT; + end else begin + count <= count + data; + margin <= margin - data; + end + + assume (data < 8'd40); + assert (count <= MAX_COUNT); + cover (count == 8'd42); + cover (count == 8'd111); +end + +endmodule diff --git a/tests/unsorted/cover.sby b/tests/unsorted/cover.sby new file mode 100644 index 0000000..894cfe1 --- /dev/null +++ b/tests/unsorted/cover.sby @@ -0,0 +1,13 @@ +[options] +mode cover +expect pass + +[engines] +btor btormc + +[script] +read -formal cover.sv +prep -top top + +[files] +cover.sv diff --git a/tests/unsorted/cover.sv b/tests/unsorted/cover.sv new file mode 100644 index 0000000..478ce36 --- /dev/null +++ b/tests/unsorted/cover.sv @@ -0,0 +1,17 @@ +module top ( + input clk, + input [7:0] din +); + reg [31:0] state = 0; + + always @(posedge clk) begin + state <= ((state << 5) + state) ^ din; + end + +`ifdef FORMAL + always @(posedge clk) begin + cover (state == 'd 12345678); + cover (state == 'h 12345678); + end +`endif +endmodule diff --git a/tests/unsorted/cover_fail.sby b/tests/unsorted/cover_fail.sby new file mode 100644 index 0000000..391e0a8 --- /dev/null +++ b/tests/unsorted/cover_fail.sby @@ -0,0 +1,31 @@ +[options] +mode cover +depth 5 +expect pass,fail + +[engines] +smtbmc boolector + +[script] +read -sv test.v +prep -top test + +[file test.v] +module test( +input clk, +input rst, +output reg [3:0] count +); + +initial assume (rst == 1'b1); + +always @(posedge clk) begin +if (rst) + count <= 4'b0; +else + count <= count + 1'b1; + +cover (count == 0 && !rst); +cover (count == 4'd11 && !rst); +end +endmodule diff --git a/tests/unsorted/demo.sby b/tests/unsorted/demo.sby new file mode 100644 index 0000000..bc40cd6 --- /dev/null +++ b/tests/unsorted/demo.sby @@ -0,0 +1,19 @@ +[tasks] +btormc +pono + +[options] +mode bmc +depth 100 +expect fail + +[engines] +btormc: btor btormc +pono: btor pono + +[script] +read -formal demo.sv +prep -top demo + +[files] +demo.sv diff --git a/tests/unsorted/demo.sv b/tests/unsorted/demo.sv new file mode 100644 index 0000000..240ea1d --- /dev/null +++ b/tests/unsorted/demo.sv @@ -0,0 +1,19 @@ +module demo ( + input clk, + output reg [5:0] counter +); + initial counter = 0; + + always @(posedge clk) begin + if (counter == 15) + counter <= 0; + else + counter <= counter + 1; + end + +`ifdef FORMAL + always @(posedge clk) begin + assert (counter < 7); + end +`endif +endmodule diff --git a/tests/unsorted/memory.sby b/tests/unsorted/memory.sby new file mode 100644 index 0000000..fa3d1d6 --- /dev/null +++ b/tests/unsorted/memory.sby @@ -0,0 +1,19 @@ +[tasks] +btormc +pono + +[options] +mode bmc +depth 10 +expect fail + +[engines] +btormc: btor btormc +pono: btor pono + +[script] +read -formal memory.sv +prep -top testbench + +[files] +memory.sv diff --git a/tests/unsorted/memory.sv b/tests/unsorted/memory.sv new file mode 100644 index 0000000..fdb9ca4 --- /dev/null +++ b/tests/unsorted/memory.sv @@ -0,0 +1,60 @@ +module testbench ( + input clk, wen, + input [9:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + memory uut ( + .clk (clk ), + .wen (wen ), + .addr (addr ), + .wdata(wdata), + .rdata(rdata) + ); + + (* anyconst *) reg [9:0] test_addr; + reg test_data_valid = 0; + reg [7:0] test_data; + + always @(posedge clk) begin + if (addr == test_addr) begin + if (wen) begin + test_data <= wdata; + test_data_valid <= 1; + end + if (test_data_valid) begin + assert(test_data == rdata); + end + end + end +endmodule + +module memory ( + input clk, wen, + input [9:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + reg [7:0] bank0 [0:255]; + reg [7:0] bank1 [0:255]; + reg [7:0] bank2 [0:255]; + reg [7:0] bank3 [0:255]; + + wire [1:0] mem_sel = addr[9:8]; + wire [7:0] mem_addr = addr[7:0]; + + always @(posedge clk) begin + case (mem_sel) + 0: if (wen) bank0[mem_addr] <= wdata; + 1: if (wen) bank1[mem_addr] <= wdata; + 2: if (wen) bank1[mem_addr] <= wdata; // BUG: Should assign to bank2 + 3: if (wen) bank3[mem_addr] <= wdata; + endcase + end + + assign rdata = + mem_sel == 0 ? bank0[mem_addr] : + mem_sel == 1 ? bank1[mem_addr] : + mem_sel == 2 ? bank2[mem_addr] : + mem_sel == 3 ? bank3[mem_addr] : 'bx; +endmodule diff --git a/tests/unsorted/mixed.sby b/tests/unsorted/mixed.sby new file mode 100644 index 0000000..2d9467e --- /dev/null +++ b/tests/unsorted/mixed.sby @@ -0,0 +1,21 @@ +[tasks] +cover +btormc bmc +pono bmc + +[options] +cover: mode cover +bmc: mode bmc +bmc: depth 1 + +[engines] +cover: btor btormc +btormc: btor btormc +pono: btor pono + +[script] +read -formal mixed.v +prep -top test + +[files] +mixed.v diff --git a/tests/unsorted/mixed.v b/tests/unsorted/mixed.v new file mode 100644 index 0000000..fa3cf2c --- /dev/null +++ b/tests/unsorted/mixed.v @@ -0,0 +1,17 @@ +module test (input CP, CN, CX, input A, B, output reg XP, XN, YP, YN); + always @* begin + assume (A || B); + assume (!A || !B); + assert (A != B); + cover (A); + cover (B); + end + always @(posedge CP) + XP <= A; + always @(negedge CN) + XN <= B; + always @(posedge CX) + YP <= A; + always @(negedge CX) + YN <= B; +endmodule diff --git a/tests/unsorted/multi_assert.sby b/tests/unsorted/multi_assert.sby new file mode 100644 index 0000000..883181a --- /dev/null +++ b/tests/unsorted/multi_assert.sby @@ -0,0 +1,24 @@ +[tasks] +btormc +pono + +[options] +mode bmc +depth 5 +expect fail + +[engines] +btormc: btor btormc +pono: btor pono + +[script] +read -sv multi_assert.v +prep -top test + +[file multi_assert.v] +module test(); +always @* begin +assert (1); +assert (0); +end +endmodule diff --git a/tests/unsorted/preunsat.sby b/tests/unsorted/preunsat.sby new file mode 100644 index 0000000..98255c6 --- /dev/null +++ b/tests/unsorted/preunsat.sby @@ -0,0 +1,22 @@ +[tasks] +btormc +yices + +[options] +mode bmc +yices: expect error +btormc: expect pass + +[engines] +btormc: btor btormc +yices: smtbmc yices + +[script] +read -sv test.sv +prep -top test + +[file test.sv] +module test(input foo); +always @* assume(0); +always @* assert(foo); +endmodule diff --git a/tests/unsorted/prv32fmcmp.sby b/tests/unsorted/prv32fmcmp.sby new file mode 100644 index 0000000..bd4e096 --- /dev/null +++ b/tests/unsorted/prv32fmcmp.sby @@ -0,0 +1,21 @@ +[tasks] +btormc +pono + +[options] +mode bmc +expect fail + +[engines] +btormc: btor btormc +pono: btor pono + +[script] +read -noverific +read -sv picorv32.v +read -sv prv32fmcmp.v +prep -top prv32fmcmp + +[files] +../../extern/picorv32.v +prv32fmcmp.v diff --git a/tests/unsorted/prv32fmcmp.v b/tests/unsorted/prv32fmcmp.v new file mode 100644 index 0000000..5116375 --- /dev/null +++ b/tests/unsorted/prv32fmcmp.v @@ -0,0 +1,73 @@ +module prv32fmcmp ( + input clock, + input resetn, + output mem_valid_a, mem_valid_b, + output mem_instr_a, mem_instr_b, + input mem_ready_a, mem_ready_b, + output [31:0] mem_addr_a, mem_addr_b, + output [31:0] mem_wdata_a, mem_wdata_b, + output [ 3:0] mem_wstrb_a, mem_wstrb_b, + input [31:0] mem_rdata_a, mem_rdata_b +); + picorv32 #( + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1) + ) prv32_a ( + .clk (clock ), + .resetn (resetn ), + .mem_valid (mem_valid_a), + .mem_instr (mem_instr_a), + .mem_ready (mem_ready_a), + .mem_addr (mem_addr_a ), + .mem_wdata (mem_wdata_a), + .mem_wstrb (mem_wstrb_a), + .mem_rdata (mem_rdata_a) + ); + + picorv32 #( + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1) + ) prv32_b ( + .clk (clock ), + .resetn (resetn ), + .mem_valid (mem_valid_b), + .mem_instr (mem_instr_b), + .mem_ready (mem_ready_b), + .mem_addr (mem_addr_b ), + .mem_wdata (mem_wdata_b), + .mem_wstrb (mem_wstrb_b), + .mem_rdata (mem_rdata_b) + ); + + reg [31:0] rom [0:255]; + + integer mem_access_cnt_a = 0; + integer mem_access_cnt_b = 0; + + always @* begin + assume(resetn == !$initstate); + + if (resetn) begin + // only consider programs without data memory read/write + if (mem_valid_a) assume(mem_instr_a); + if (mem_valid_b) assume(mem_instr_b); + + // when the access cnt matches, the addresses must match + if (mem_valid_a && mem_valid_b && mem_access_cnt_a == mem_access_cnt_b) begin + assert(mem_addr_a == mem_addr_b); + end + + // hook up to memory + assume(mem_rdata_a == rom[mem_addr_a[9:2]]); + assume(mem_rdata_b == rom[mem_addr_b[9:2]]); + end + + // it will pass when this is enabled + //assume(mem_ready_a == mem_ready_b); + end + + always @(posedge clock) begin + mem_access_cnt_a <= mem_access_cnt_a + (resetn && mem_valid_a && mem_ready_a); + mem_access_cnt_b <= mem_access_cnt_b + (resetn && mem_valid_b && mem_ready_b); + end +endmodule diff --git a/tests/unsorted/redxor.sby b/tests/unsorted/redxor.sby new file mode 100644 index 0000000..0746861 --- /dev/null +++ b/tests/unsorted/redxor.sby @@ -0,0 +1,13 @@ +[options] +mode cover +expect pass + +[engines] +btor btormc + +[script] +read -formal redxor.v +prep -top test + +[files] +redxor.v diff --git a/tests/unsorted/redxor.v b/tests/unsorted/redxor.v new file mode 100644 index 0000000..3bab284 --- /dev/null +++ b/tests/unsorted/redxor.v @@ -0,0 +1,8 @@ +module test(input [7:0] I, output O); +assign O = ^I; + +always @(*) begin +cover(O==1'b0); +cover(O==1'b1); +end +endmodule diff --git a/tests/unsorted/stopfirst.sby b/tests/unsorted/stopfirst.sby new file mode 100644 index 0000000..782f791 --- /dev/null +++ b/tests/unsorted/stopfirst.sby @@ -0,0 +1,16 @@ +[options] +mode bmc +expect fail + +[engines] +btor btormc + +[script] +read -sv test.sv +prep -top test + +[file test.sv] +module test(input foo); +always @* assert(foo); +always @* assert(!foo); +endmodule diff --git a/tests/unsorted/submod_props.sby b/tests/unsorted/submod_props.sby new file mode 100644 index 0000000..9933676 --- /dev/null +++ b/tests/unsorted/submod_props.sby @@ -0,0 +1,33 @@ +[tasks] +bmc +cover +flatten + +[options] +bmc: mode bmc +cover: mode cover +flatten: mode bmc + +expect fail + +[engines] +smtbmc boolector + +[script] +read -sv test.sv +prep -top top +flatten: flatten + +[file test.sv] +module test(input foo); +always @* assert(foo); +always @* assert(!foo); +always @* cover(foo); +always @* cover(!foo); +endmodule + +module top(); +test test_i ( +.foo(1'b1) +); +endmodule diff --git a/tests/validate_junit.py b/tests/validate_junit.py deleted file mode 100644 index c1c0573..0000000 --- a/tests/validate_junit.py +++ /dev/null @@ -1,19 +0,0 @@ -from xmlschema import XMLSchema, XMLSchemaValidationError -import argparse - -def main(): - parser = argparse.ArgumentParser(description="Validate JUnit output") - parser.add_argument('xml') - parser.add_argument('--xsd', default="JUnit.xsd") - - args = parser.parse_args() - - schema = XMLSchema(args.xsd) - try: - schema.validate(args.xml) - except XMLSchemaValidationError as e: - print(e) - exit(1) - -if __name__ == '__main__': - main()