-/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__
+++ /dev/null
-[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
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<xs:schema
- xmlns:xs="http://www.w3.org/2001/XMLSchema"
- elementFormDefault="qualified"
- attributeFormDefault="unqualified">
- <xs:annotation>
- <xs:documentation xml:lang="en">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).</xs:documentation>
- </xs:annotation>
- <xs:element name="testsuite" type="testsuite"/>
- <xs:simpleType name="ISO8601_DATETIME_PATTERN">
- <xs:restriction base="xs:dateTime">
- <xs:pattern value="[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}"/>
- </xs:restriction>
- </xs:simpleType>
- <xs:element name="testsuites">
- <xs:annotation>
- <xs:documentation xml:lang="en">Contains an aggregation of testsuite results</xs:documentation>
- </xs:annotation>
- <xs:complexType>
- <xs:sequence>
- <xs:element name="testsuite" minOccurs="0" maxOccurs="unbounded">
- <xs:complexType>
- <xs:complexContent>
- <xs:extension base="testsuite">
- <xs:attribute name="package" type="xs:token" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Derived from testsuite/@name in the non-aggregated documents</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="id" type="xs:int" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- </xs:extension>
- </xs:complexContent>
- </xs:complexType>
- </xs:element>
- </xs:sequence>
- </xs:complexType>
- </xs:element>
- <xs:complexType name="testsuite">
- <xs:annotation>
- <xs:documentation xml:lang="en">Contains the results of exexuting a testsuite</xs:documentation>
- </xs:annotation>
- <xs:sequence>
- <xs:element name="properties">
- <xs:annotation>
- <xs:documentation xml:lang="en">Properties (e.g., environment settings) set during test execution</xs:documentation>
- </xs:annotation>
- <xs:complexType>
- <xs:sequence>
- <xs:element name="property" minOccurs="0" maxOccurs="unbounded">
- <xs:complexType>
- <xs:attribute name="name" use="required">
- <xs:simpleType>
- <xs:restriction base="xs:token">
- <xs:minLength value="1"/>
- </xs:restriction>
- </xs:simpleType>
- </xs:attribute>
- <xs:attribute name="value" type="xs:string" use="required"/>
- </xs:complexType>
- </xs:element>
- </xs:sequence>
- </xs:complexType>
- </xs:element>
- <xs:element name="testcase" minOccurs="0" maxOccurs="unbounded">
- <xs:complexType>
- <xs:choice minOccurs="0">
- <xs:element name="skipped" />
- <xs:element name="error" minOccurs="0" maxOccurs="1">
- <xs:annotation>
- <xs:documentation xml:lang="en">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</xs:documentation>
- </xs:annotation>
- <xs:complexType>
- <xs:simpleContent>
- <xs:extension base="pre-string">
- <xs:attribute name="message" type="xs:string">
- <xs:annotation>
- <xs:documentation xml:lang="en">The error message. e.g., if a java exception is thrown, the return value of getMessage()</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="type" type="xs:string" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">The type of error that occured. e.g., if a java execption is thrown the full class name of the exception.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- </xs:extension>
- </xs:simpleContent>
- </xs:complexType>
- </xs:element>
- <xs:element name="failure">
- <xs:annotation>
- <xs:documentation xml:lang="en">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</xs:documentation>
- </xs:annotation>
- <xs:complexType>
- <xs:simpleContent>
- <xs:extension base="pre-string">
- <xs:attribute name="message" type="xs:string">
- <xs:annotation>
- <xs:documentation xml:lang="en">The message specified in the assert</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="type" type="xs:string" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">The type of the assert.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- </xs:extension>
- </xs:simpleContent>
- </xs:complexType>
- </xs:element>
- </xs:choice>
- <xs:attribute name="name" type="xs:token" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Name of the test method</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="classname" type="xs:token" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Full class name for the class the test method is in.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="time" type="xs:decimal" use="required">
- <xs:annotation>
- <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">
- <xs:annotation>
- <xs:documentation xml:lang="en">Data that was written to standard out while the test was executed</xs:documentation>
- </xs:annotation>
- <xs:simpleType>
- <xs:restriction base="pre-string">
- <xs:whiteSpace value="preserve"/>
- </xs:restriction>
- </xs:simpleType>
- </xs:element>
- <xs:element name="system-err">
- <xs:annotation>
- <xs:documentation xml:lang="en">Data that was written to standard error while the test was executed</xs:documentation>
- </xs:annotation>
- <xs:simpleType>
- <xs:restriction base="pre-string">
- <xs:whiteSpace value="preserve"/>
- </xs:restriction>
- </xs:simpleType>
- </xs:element>
- </xs:sequence>
- <xs:attribute name="name" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents</xs:documentation>
- </xs:annotation>
- <xs:simpleType>
- <xs:restriction base="xs:token">
- <xs:minLength value="1"/>
- </xs:restriction>
- </xs:simpleType>
- </xs:attribute>
- <xs:attribute name="timestamp" type="ISO8601_DATETIME_PATTERN" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">when the test was executed. Timezone may not be specified.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="hostname" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined.</xs:documentation>
- </xs:annotation>
- <xs:simpleType>
- <xs:restriction base="xs:token">
- <xs:minLength value="1"/>
- </xs:restriction>
- </xs:simpleType>
- </xs:attribute>
- <xs:attribute name="tests" type="xs:int" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">The total number of tests in the suite</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="failures" type="xs:int" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">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</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="errors" type="xs:int" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">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.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="skipped" type="xs:int" use="optional">
- <xs:annotation>
- <xs:documentation xml:lang="en">The total number of ignored or skipped tests in the suite.</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- <xs:attribute name="time" type="xs:decimal" use="required">
- <xs:annotation>
- <xs:documentation xml:lang="en">Time taken (in seconds) to execute the tests in the suite</xs:documentation>
- </xs:annotation>
- </xs:attribute>
- </xs:complexType>
- <xs:simpleType name="pre-string">
- <xs:restriction base="xs:string">
- <xs:whiteSpace value="preserve"/>
- </xs:restriction>
- </xs:simpleType>
-</xs:schema>
-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
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-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))
+++ /dev/null
-[options]
-mode cover
-expect pass
-
-[engines]
-btor btormc
-
-[script]
-read -formal cover.sv
-prep -top top
-
-[files]
-cover.sv
+++ /dev/null
-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
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-[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
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<xs:schema
+ xmlns:xs="http://www.w3.org/2001/XMLSchema"
+ elementFormDefault="qualified"
+ attributeFormDefault="unqualified">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">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).</xs:documentation>
+ </xs:annotation>
+ <xs:element name="testsuite" type="testsuite"/>
+ <xs:simpleType name="ISO8601_DATETIME_PATTERN">
+ <xs:restriction base="xs:dateTime">
+ <xs:pattern value="[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}"/>
+ </xs:restriction>
+ </xs:simpleType>
+ <xs:element name="testsuites">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Contains an aggregation of testsuite results</xs:documentation>
+ </xs:annotation>
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element name="testsuite" minOccurs="0" maxOccurs="unbounded">
+ <xs:complexType>
+ <xs:complexContent>
+ <xs:extension base="testsuite">
+ <xs:attribute name="package" type="xs:token" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Derived from testsuite/@name in the non-aggregated documents</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="id" type="xs:int" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ </xs:extension>
+ </xs:complexContent>
+ </xs:complexType>
+ </xs:element>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
+ <xs:complexType name="testsuite">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Contains the results of exexuting a testsuite</xs:documentation>
+ </xs:annotation>
+ <xs:sequence>
+ <xs:element name="properties">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Properties (e.g., environment settings) set during test execution</xs:documentation>
+ </xs:annotation>
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element name="property" minOccurs="0" maxOccurs="unbounded">
+ <xs:complexType>
+ <xs:attribute name="name" use="required">
+ <xs:simpleType>
+ <xs:restriction base="xs:token">
+ <xs:minLength value="1"/>
+ </xs:restriction>
+ </xs:simpleType>
+ </xs:attribute>
+ <xs:attribute name="value" type="xs:string" use="required"/>
+ </xs:complexType>
+ </xs:element>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
+ <xs:element name="testcase" minOccurs="0" maxOccurs="unbounded">
+ <xs:complexType>
+ <xs:choice minOccurs="0">
+ <xs:element name="skipped" />
+ <xs:element name="error" minOccurs="0" maxOccurs="1">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">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</xs:documentation>
+ </xs:annotation>
+ <xs:complexType>
+ <xs:simpleContent>
+ <xs:extension base="pre-string">
+ <xs:attribute name="message" type="xs:string">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The error message. e.g., if a java exception is thrown, the return value of getMessage()</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="type" type="xs:string" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The type of error that occured. e.g., if a java execption is thrown the full class name of the exception.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ </xs:extension>
+ </xs:simpleContent>
+ </xs:complexType>
+ </xs:element>
+ <xs:element name="failure">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">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</xs:documentation>
+ </xs:annotation>
+ <xs:complexType>
+ <xs:simpleContent>
+ <xs:extension base="pre-string">
+ <xs:attribute name="message" type="xs:string">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The message specified in the assert</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="type" type="xs:string" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The type of the assert.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ </xs:extension>
+ </xs:simpleContent>
+ </xs:complexType>
+ </xs:element>
+ </xs:choice>
+ <xs:attribute name="name" type="xs:token" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Name of the test method</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="classname" type="xs:token" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Full class name for the class the test method is in.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="time" type="xs:decimal" use="required">
+ <xs:annotation>
+ <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">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Data that was written to standard out while the test was executed</xs:documentation>
+ </xs:annotation>
+ <xs:simpleType>
+ <xs:restriction base="pre-string">
+ <xs:whiteSpace value="preserve"/>
+ </xs:restriction>
+ </xs:simpleType>
+ </xs:element>
+ <xs:element name="system-err">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Data that was written to standard error while the test was executed</xs:documentation>
+ </xs:annotation>
+ <xs:simpleType>
+ <xs:restriction base="pre-string">
+ <xs:whiteSpace value="preserve"/>
+ </xs:restriction>
+ </xs:simpleType>
+ </xs:element>
+ </xs:sequence>
+ <xs:attribute name="name" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents</xs:documentation>
+ </xs:annotation>
+ <xs:simpleType>
+ <xs:restriction base="xs:token">
+ <xs:minLength value="1"/>
+ </xs:restriction>
+ </xs:simpleType>
+ </xs:attribute>
+ <xs:attribute name="timestamp" type="ISO8601_DATETIME_PATTERN" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">when the test was executed. Timezone may not be specified.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="hostname" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined.</xs:documentation>
+ </xs:annotation>
+ <xs:simpleType>
+ <xs:restriction base="xs:token">
+ <xs:minLength value="1"/>
+ </xs:restriction>
+ </xs:simpleType>
+ </xs:attribute>
+ <xs:attribute name="tests" type="xs:int" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The total number of tests in the suite</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="failures" type="xs:int" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">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</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="errors" type="xs:int" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">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.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="skipped" type="xs:int" use="optional">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">The total number of ignored or skipped tests in the suite.</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ <xs:attribute name="time" type="xs:decimal" use="required">
+ <xs:annotation>
+ <xs:documentation xml:lang="en">Time taken (in seconds) to execute the tests in the suite</xs:documentation>
+ </xs:annotation>
+ </xs:attribute>
+ </xs:complexType>
+ <xs:simpleType name="pre-string">
+ <xs:restriction base="xs:string">
+ <xs:whiteSpace value="preserve"/>
+ </xs:restriction>
+ </xs:simpleType>
+</xs:schema>
--- /dev/null
+SUBDIR=junit
+include ../make/subdir.mk
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 validate_junit.py $WORKDIR/$WORKDIR.xml
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 validate_junit.py $WORKDIR/$WORKDIR.xml
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+! python3 $SBY_MAIN -f $SBY_FILE $TASK
+grep '<failure type="EXPECT" message="Task returned status PASS. Expected values were: FAIL TIMEOUT" />' $WORKDIR/$WORKDIR.xml
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 validate_junit.py $WORKDIR/$WORKDIR.xml
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 validate_junit.py $WORKDIR/$WORKDIR.xml
--- /dev/null
+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()
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-[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
--- /dev/null
+SUBDIR=keepgoing
+include ../make/subdir.mk
--- /dev/null
+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))
--- /dev/null
+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())
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 ${SBY_FILE%.sby}.py $WORKDIR
--- /dev/null
+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
--- /dev/null
+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)
--- /dev/null
+[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
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 ${SBY_FILE%.sby}.py $WORKDIR
--- /dev/null
+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
--- /dev/null
+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)
--- /dev/null
+[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)
--- /dev/null
+#!/bin/bash
+set -e
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+python3 ${SBY_FILE%.sby}.py $WORKDIR
+++ /dev/null
-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())
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-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)
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-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)
+++ /dev/null
-[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)
--- /dev/null
+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)
--- /dev/null
+make test:
+ run all tests (default)
+
+make clean:
+ remove all sby workdirs
+
+make test[_m_<mode>][_e_<engine>][_s_<solver>]:
+ run all tests that use a specific mode, engine and solver
+
+make <name>:
+ run the test for <name>.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
--- /dev/null
+test:
+ @$(MAKE) -C .. $(SUBDIR)/$@
+
+.PHONY: test refresh IMPLICIT_PHONY
+
+IMPLICIT_PHONY:
+
+refresh:
+ @$(MAKE) -C .. refresh
+
+help:
+ @$(MAKE) -C .. help
+
+%: IMPLICIT_PHONY
+ @$(MAKE) -C .. $(SUBDIR)/$@
--- /dev/null
+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)
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-[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
+++ /dev/null
-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
+++ /dev/null
-[options]
-mode cover
-expect pass
-
-[engines]
-btor btormc
-
-[script]
-read -formal redxor.v
-prep -top test
-
-[files]
-redxor.v
+++ /dev/null
-module test(input [7:0] I, output O);
-assign O = ^I;
-
-always @(*) begin
-cover(O==1'b0);
-cover(O==1'b1);
-end
-endmodule
--- /dev/null
+SUBDIR=regression
+include ../make/subdir.mk
--- /dev/null
+[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
--- /dev/null
+[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
+++ /dev/null
-SH_FILES=$(wildcard *.sh)
-SH_TESTS=$(addprefix test_,$(SH_FILES:.sh=))
-
-test: $(SH_TESTS)
-
-test_%: %.sh FORCE
- bash $<
-
-FORCE:
-
-.PHONY: test FORCE
+++ /dev/null
-[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
+++ /dev/null
-#!/bin/bash
-
-# this is expected to return 1 so don't use 'set -e'
-python3 ../../sbysrc/sby.py -f junit_expect.sby
-grep '<failure type="EXPECT" message="Task returned status PASS. Expected values were: FAIL TIMEOUT" />' junit_expect/junit_expect.xml
+++ /dev/null
-[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
+++ /dev/null
-[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
--- /dev/null
+[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
--- /dev/null
+SUBDIR=unsorted
+include ../make/subdir.mk
--- /dev/null
+[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
--- /dev/null
+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
--- /dev/null
+[options]
+mode cover
+expect pass
+
+[engines]
+btor btormc
+
+[script]
+read -formal cover.sv
+prep -top top
+
+[files]
+cover.sv
--- /dev/null
+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
--- /dev/null
+[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
--- /dev/null
+[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
--- /dev/null
+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
--- /dev/null
+[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
--- /dev/null
+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
--- /dev/null
+[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
--- /dev/null
+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
--- /dev/null
+[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
--- /dev/null
+[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
--- /dev/null
+[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
--- /dev/null
+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
--- /dev/null
+[options]
+mode cover
+expect pass
+
+[engines]
+btor btormc
+
+[script]
+read -formal redxor.v
+prep -top test
+
+[files]
+redxor.v
--- /dev/null
+module test(input [7:0] I, output O);
+assign O = ^I;
+
+always @(*) begin
+cover(O==1'b0);
+cover(O==1'b1);
+end
+endmodule
--- /dev/null
+[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
--- /dev/null
+[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
+++ /dev/null
-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()
projects / SymbiYosys.git / commitdiff