[pull] master from YosysHQ:master

.github/workflows/ci.yml

@@ -0,0 +1,14 @@
+name: ci
+on: [push, pull_request]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: YosysHQ/setup-oss-cad-suite@v3
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+      - name: Run checks
+        run: pip install xmlschema && make ci

.github/workflows/codeql.yml

@@ -0,0 +1,28 @@
+name: "CodeQL"
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 2 * * *'
+
+jobs:
+  analyze:
+    name: Analyze
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: read
+      security-events: write
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v4
+
+    - name: Initialize CodeQL
+      uses: github/codeql-action/init@v3
+      with:
+        languages: python
+        queries: security-extended,security-and-quality
+
+    - name: Perform CodeQL Analysis
+      uses: github/codeql-action/analyze@v3

.readthedocs.yaml

@@ -3,6 +3,11 @@
 
 version: 2
 
+build:
+    os: ubuntu-22.04
+    tools:
+        python: '3.11'
+
 formats:
   - pdf
 

Makefile

@@ -1,6 +1,6 @@
 
 DESTDIR =
-PREFIX = /usr/local
+PREFIX ?= /usr/local
 PROGRAM_PREFIX =
 
 # On Windows, manually setting absolute path to Python binary may be required
@@ -10,6 +10,8 @@ ifeq ($(OS), Windows_NT)
 PYTHON = $(shell cygpath -w -m $(PREFIX)/bin/python3)
 endif
 
+.PHONY: help install ci test html clean
+
 help:
 	@echo ""
 	@echo "sudo make install"
@@ -19,7 +21,11 @@ help:
 	@echo "    build documentation in docs/build/html/"
 	@echo ""
 	@echo "make test"
-	@echo "    run examples"
+	@echo "    run tests, skipping tests with missing dependencies"
+	@echo ""
+	@echo "make ci"
+	@echo "    run all tests, failing tests with missing dependencies"
+	@echo "    note: this requires a full Tabby CAD Suite or OSS CAD Suite install"
 	@echo ""
 	@echo "make clean"
 	@echo "    cleanup"
@@ -39,17 +45,22 @@ else
 	chmod +x $(DESTDIR)$(PREFIX)/bin/sby
 endif
 
-ci: \
-  test_demo1 test_demo2 test_demo3 \
-  test_abstract_abstr test_abstract_props \
-  test_demos_fib_cover test_demos_fib_prove test_demos_fib_live \
-  test_multiclk_dpmem \
-  test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
-  test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
-  test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \
-  run_tests
+.PHONY: check_cad_suite run_ci
+
+ci: check_cad_suite
+	@$(MAKE) run_ci
+
+run_ci:
+	$(MAKE) test NOSKIP=1
 	if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		YOSYS_NOVERIFIC=1 $(MAKE) ci; \
+		YOSYS_NOVERIFIC=1 $(MAKE) run_ci; \
+	fi
+
+check_cad_suite:
+	@if ! which tabbypip >/dev/null 2>&1; then \
+		echo "'make ci' requries the Tabby CAD Suite or the OSS CAD Suite"; \
+		echo "try 'make test' instead or run 'make run_ci' to proceed anyway."; \
+		exit 1; \
 	fi
 
 test_demo1:
@@ -61,59 +72,7 @@ test_demo2:
 test_demo3:
 	cd sbysrc && python3 sby.py -f demo3.sby
 
-test_abstract_abstr:
-	@if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f abstr.sby; \
-	else echo "skipping $@"; fi
-
-test_abstract_props:
-	if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f props.sby; \
-	else echo "skipping $@"; fi
-
-test_demos_fib_cover:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby cover
-
-test_demos_fib_prove:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby prove
-
-test_demos_fib_live:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby live
-
-test_multiclk_dpmem:
-	cd docs/examples/multiclk && python3 ../../../sbysrc/sby.py -f dpmem.sby
-
-test_puzzles_djb2hash:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f djb2hash.sby
-
-test_puzzles_pour853to4:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f pour_853_to_4.sby
-
-test_puzzles_wolfgoatcabbage:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f wolf_goat_cabbage.sby
-
-test_puzzles_primegen_primegen:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primegen
-
-test_puzzles_primegen_primes_pass:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_pass
-
-test_puzzles_primegen_primes_fail:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_fail
-
-test_quickstart_demo:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f demo.sby
-
-test_quickstart_cover:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f cover.sby
-
-test_quickstart_prove:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f prove.sby
-
-test_quickstart_memory:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
-
-run_tests:
+test:
 	$(MAKE) -C tests test
 
 html:

docs/examples/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples
+TESTDIR=../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/abstract/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/abstract
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/autotune/README.md

@@ -0,0 +1,30 @@
+# Autotune demo
+
+This directory contains a simple sequential integer divider circuit. The
+verilog implementation in [divider.sv](divider.sv) comes with assertions that
+this circuit will always produce the correct result and will always finish
+within a fixed number of cycles. The circuit has the divider bit-width as
+parameter.
+
+Increasing the WIDTH parameter quickly turns proving those assertions into a
+very difficult proof for fully autmated solvers. This makes it a good example
+for the `--autotune` option which tries different backend engines to find the
+best performing engine configuration for a given verification task.
+
+The [divider.sby](divider.sby) file defines 3 tasks named `small`, `medium` and
+`large` which configure the divider with different bit-widths. To verify the
+`small` divider using the default engine run:
+
+    sby -f divider.sby small
+
+To automatically try different backend engines using autotune, run
+
+    sby --autotune -f divider.sby small
+
+The `small` task should finish quickly using both the default engine and using
+autotune. The `medium` and `large` tasks take significantly longer and show
+greater differences between engine configurations. Note that the `large` tasks
+can take many minutes to hours, depending on the machine you are using.
+
+You can learn more about Sby's autotune feature from [Sby's
+documentation](https://symbiyosys.readthedocs.io/en/latest/autotune.html).

docs/examples/autotune/divider.sby

@@ -0,0 +1,24 @@
+[tasks]
+small default
+medium
+large
+
+[options]
+mode prove
+small: depth 11
+medium: depth 15
+large: depth 19
+
+[engines]
+smtbmc
+
+[script]
+small: read -define WIDTH=8
+medium: read -define WIDTH=12
+large: read -define WIDTH=16
+
+read -formal divider.sv
+prep -top divider
+
+[files]
+divider.sv

docs/examples/autotune/divider.sv

@@ -0,0 +1,85 @@
+`ifndef WIDTH
+`define WIDTH 4
+`endif
+
+module divider #(
+    parameter WIDTH=`WIDTH
+) (
+    input wire clk,
+    input wire start,
+    input wire [WIDTH-1:0] dividend,
+    input wire [WIDTH-1:0] divisor,
+
+    output reg done,
+    output reg [WIDTH-1:0] quotient,
+    output wire [WIDTH-1:0] remainder
+);
+
+    reg [WIDTH-1:0] acc;
+
+    reg [WIDTH*2-1:0] sub;
+    reg [WIDTH-1:0] pos;
+
+    assign remainder = acc;
+
+    always @(posedge clk) begin
+        if (start) begin
+            acc <= dividend;
+            quotient <= 0;
+            sub <= divisor << (WIDTH - 1);
+            pos <= 1 << (WIDTH - 1);
+            done <= 0;
+        end else if (!done) begin
+            if (acc >= sub) begin
+                acc <= acc - sub[WIDTH-1:0];
+                quotient <= quotient + pos;
+            end
+
+            sub <= sub >> 1;
+            {pos, done} <= pos;
+        end
+    end
+
+
+`ifdef FORMAL
+    reg [WIDTH-1:0] start_dividend = 0;
+    reg [WIDTH-1:0] start_divisor = 0;
+
+    reg started = 0;
+    reg finished = 0;
+    reg [$clog2(WIDTH + 1):0] counter = 0;
+
+    always @(posedge clk) begin
+        // Bound the number of cycles until the result is ready
+        assert (counter <= WIDTH);
+
+        if (started) begin
+            if (finished || done) begin
+                finished <= 1;
+                // Make sure result stays until we start a new division
+                assert (done);
+
+                // Check the result
+                if (start_divisor == 0) begin
+                    assert (&quotient);
+                    assert (remainder == start_dividend);
+                end else begin
+                    assert (quotient == start_dividend / start_divisor);
+                    assert (remainder == start_dividend % start_divisor);
+                end
+            end else begin
+                counter <= counter + 1'b1;
+            end
+        end
+
+        // Track the requested inputs
+        if (start) begin
+            start_divisor <= divisor;
+            start_dividend <= dividend;
+            started <= 1;
+            counter <= 0;
+            finished <= 0;
+        end
+    end
+`endif
+endmodule

docs/examples/demos/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/demos
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/demos/picorv32_axicheck.sby

@@ -0,0 +1,25 @@
+[tasks]
+yices
+boolector
+z3
+abc
+
+[options]
+mode bmc
+depth 10
+
+[engines]
+yices: smtbmc yices
+boolector: smtbmc boolector -ack
+z3: smtbmc --nomem z3
+abc: abc bmc3
+
+[script]
+read_verilog -formal -norestrict -assume-asserts picorv32.v
+read_verilog -formal axicheck.v
+prep -top testbench
+
+[files]
+picorv32.v ../../../extern/picorv32.v
+axicheck.v ../../../extern/axicheck.v
+

sbysrc/demo2.sby → docs/examples/demos/up_down_counter.sby

@@ -1,10 +1,13 @@
+[tasks]
+suprove
+avy
+
 [options]
 mode prove
-wait on
 
 [engines]
-aiger suprove
-aiger avy
+suprove: aiger suprove
+avy: aiger avy
 
 [script]
 read_verilog -formal demo.v