diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index 74f7ddf5..9cc2a62d 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -84,7 +84,7 @@ jobs: pull: >- ghdl/yosys pkg/z3 - pkg/symbiyosys + pkg/sby pkg/yices2 pkg/boolector pkg/cvc diff --git a/.github/workflows/symbiyosys.yml b/.github/workflows/sby.yml similarity index 93% rename from .github/workflows/symbiyosys.yml rename to .github/workflows/sby.yml index 3e537bb6..a7a36daa 100644 --- a/.github/workflows/symbiyosys.yml +++ b/.github/workflows/sby.yml @@ -20,7 +20,7 @@ # # SPDX-License-Identifier: Apache-2.0 -name: 'symbiyosys' +name: 'sby' on: pull_request: @@ -29,16 +29,16 @@ on: - cron: '0 0 * * 5' workflow_dispatch: repository_dispatch: - types: [ symbiyosys ] + types: [ sby ] env: DOCKER_BUILDKIT: 1 jobs: - symbiyosys: + sby: uses: ./.github/workflows/common.yml with: - key: symbiyosys + key: sby skip-release: ${{ github.event_name == 'pull_request' }} secrets: gcr_token: '${{ secrets.GCR_JSON_KEY }}' diff --git a/.todo/tasks.py b/.todo/tasks.py index f6f20eeb..f1b148e3 100644 --- a/.todo/tasks.py +++ b/.todo/tasks.py @@ -20,7 +20,7 @@ # "synth:beta", # "synth:formal", # -# "synth:symbiyosys", +# "synth:sby", # # "build:base", # "build:build", @@ -42,7 +42,7 @@ def task(name, args, dry_run=False): "formal": ("cache", "formal"), - "symbiyosys": ("synth", "symbiyosys"), + "sby": ("synth", "sby"), "vunit": map( lambda backend: map( lambda tag: ("vunit", tag), [backend, "%s-master" % backend] ), ["mcode", "llvm", "gcc"] @@ -82,7 +82,7 @@ def b_s(tag): return ("synth", tag, "yosys", { "target": "yosys" }) - if tag == "symbiyosys": + if tag == "sby": return ("synth", tag, "synth_formal", { "args": [ 'IMAGE=ghdl/synth:yosys' diff --git a/debian-bookworm/symbiyosys.dockerfile b/debian-bookworm/sby.dockerfile similarity index 82% rename from debian-bookworm/symbiyosys.dockerfile rename to debian-bookworm/sby.dockerfile index 48ae912b..989d8cd0 100644 --- a/debian-bookworm/symbiyosys.dockerfile +++ b/debian-bookworm/sby.dockerfile @@ -36,11 +36,11 @@ RUN apt-get update -qq \ && update-ca-certificates \ && rm -rf /var/lib/apt/lists/* -RUN mkdir /tmp/symbiyosys && cd /tmp/symbiyosys \ - && curl -fsSL https://codeload.github.com/YosysHQ/SymbiYosys/tar.gz/main | tar xzf - --strip-components=1 \ - && make DESTDIR=/opt/symbiyosys install +RUN mkdir /tmp/sby && cd /tmp/sby \ + && curl -fsSL https://codeload.github.com/YosysHQ/sby/tar.gz/main | tar xzf - --strip-components=1 \ + && make DESTDIR=/opt/sby install #--- FROM scratch -COPY --from=build /opt/symbiyosys /symbiyosys +COPY --from=build /opt/sby /sby diff --git a/debian-bullseye/formal.dockerfile b/debian-bullseye/formal.dockerfile index 32496b94..046817e3 100644 --- a/debian-bullseye/formal.dockerfile +++ b/debian-bullseye/formal.dockerfile @@ -26,12 +26,12 @@ ARG REGISTRY='gcr.io/hdl-containers/debian/bullseye' # WORKAROUND: this is required because 'COPY --from' does not support ARGs FROM $REGISTRY/pkg/z3 AS pkg-z3 -FROM $REGISTRY/pkg/symbiyosys AS pkg-symbiyosys +FROM $REGISTRY/pkg/sby AS pkg-sby FROM $REGISTRY/ghdl/yosys AS min COPY --from=pkg-z3 /z3 / -COPY --from=pkg-symbiyosys /symbiyosys / +COPY --from=pkg-sby /sby / RUN apt-get update -qq \ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ diff --git a/debian-bullseye/symbiyosys.dockerfile b/debian-bullseye/sby.dockerfile similarity index 82% rename from debian-bullseye/symbiyosys.dockerfile rename to debian-bullseye/sby.dockerfile index 52b47561..399c12ec 100644 --- a/debian-bullseye/symbiyosys.dockerfile +++ b/debian-bullseye/sby.dockerfile @@ -36,11 +36,11 @@ RUN apt-get update -qq \ && update-ca-certificates \ && rm -rf /var/lib/apt/lists/* -RUN mkdir /tmp/symbiyosys && cd /tmp/symbiyosys \ - && curl -fsSL https://codeload.github.com/YosysHQ/SymbiYosys/tar.gz/main | tar xzf - --strip-components=1 \ - && make DESTDIR=/opt/symbiyosys install +RUN mkdir /tmp/sby && cd /tmp/sby \ + && curl -fsSL https://codeload.github.com/YosysHQ/sby/tar.gz/main | tar xzf - --strip-components=1 \ + && make DESTDIR=/opt/sby install #--- FROM scratch -COPY --from=build /opt/symbiyosys /symbiyosys +COPY --from=build /opt/sby /sby diff --git a/doc/conf.py b/doc/conf.py index d6829fd5..8be97626 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -193,7 +193,7 @@ def OCIImageShield(image): "cvc", "pono", "superprove", - "symbiyosys", + "sby", "yices2", "z3", ], diff --git a/doc/graph/formal.dot b/doc/graph/formal.dot index 09441a94..80e252f8 100644 --- a/doc/graph/formal.dot +++ b/doc/graph/formal.dot @@ -29,10 +29,10 @@ digraph G { { node [shape=note, color=dodgerblue, fontcolor=dodgerblue] d_boolector [label="boolector"]; d_pono [label="pono"]; - d_cvc [label="cvc"]; + d_cvc [label="cvc"]; d_formal [label="formal"]; d_superprove [label="superprove"]; - d_symbiyosys [label="symbiyosys"]; + d_sby [label="sby"]; d_yices2 [label="yices2"]; d_z3 [label="z3"]; } @@ -50,7 +50,7 @@ digraph G { "pkg/cvc" "pkg/pono" "pkg/superprove" - "pkg/symbiyosys" + "pkg/sby" "pkg/yices2" "pkg/z3" } @@ -132,18 +132,18 @@ digraph G { "pkg/superprove" -> "t_pkg/superprove"; } - subgraph cluster_symbiyosys { + subgraph cluster_sby { { rank=same node [shape=cylinder, color=grey, fontcolor=grey] - "p_symbiyosys_scratch" [label="scratch"] - "p_symbiyosys_build/base" [label="build/base"] + "p_sby_scratch" [label="scratch"] + "p_sby_build/base" [label="build/base"] } - d_symbiyosys -> "pkg/symbiyosys" [style=dotted]; + d_sby -> "pkg/sby" [style=dotted]; - "t_pkg/symbiyosys" [shape=folder, color=red, fontcolor=red, label="symbiyosys.pkg"]; + "t_pkg/sby" [shape=folder, color=red, fontcolor=red, label="sby.pkg"]; - "pkg/symbiyosys" -> "t_pkg/symbiyosys"; + "pkg/sby" -> "t_pkg/sby"; } subgraph cluster_yices2 { @@ -181,7 +181,7 @@ digraph G { "p_formal_cvc" [label="pkg/cvc"] "p_formal_ghdl" [label="ghdl/yosys"] "p_formal_pono" [label="pkg/pono"] - "p_formal_symbiyosys" [label="pkg/symbiyosys"] + "p_formal_sby" [label="pkg/sby"] "p_formal_superprove" [label="pkg/superprove"] "p_formal_z3" [label="pkg/z3"] "p_formal_yices2" [label="pkg/yices2"] @@ -210,7 +210,7 @@ digraph G { d_cvc d_pono d_superprove - d_symbiyosys + d_sby d_yices2 d_z3 } @@ -224,7 +224,7 @@ digraph G { "scratch" -> "p_cvc_scratch" -> d_cvc; "ghdl/yosys" -> "p_formal_ghdl" -> d_formal; - "pkg/symbiyosys" -> "p_formal_symbiyosys" -> d_formal; + "pkg/sby" -> "p_formal_sby" -> d_formal; "pkg/boolector" -> "p_formal_boolector" -> d_formal; "pkg/cvc" -> "p_formal_cvc" -> d_formal; "pkg/pono" -> "p_formal_pono" -> d_formal; @@ -235,8 +235,8 @@ digraph G { "build/build" -> "p_pono_build/build" -> d_pono; "scratch" -> "p_pono_scratch" -> d_pono; - "build/base" -> "p_symbiyosys_build/base" -> d_symbiyosys; - "scratch" -> "p_symbiyosys_scratch" -> d_symbiyosys; + "build/base" -> "p_sby_build/base" -> d_sby; + "scratch" -> "p_sby_scratch" -> d_sby; "build/build" -> "p_superprove_build/build" -> d_superprove; "scratch" -> "p_superprove_scratch" -> d_superprove; @@ -255,14 +255,14 @@ digraph G { "p_formal_ghdl" -> "formal/min" -> "formal" -> "formal/all"; "p_pono_scratch" -> "pkg/pono"; "p_superprove_scratch" -> "pkg/superprove"; - "p_symbiyosys_scratch" -> "pkg/symbiyosys"; + "p_sby_scratch" -> "pkg/sby"; "p_yices2_scratch" -> "pkg/yices2"; "p_z3_scratch" -> "pkg/z3"; } { edge [style=dashed, color=grey] { - "p_formal_symbiyosys", + "p_formal_sby", "p_formal_z3" } -> "formal/min"; diff --git a/doc/graph/graph.dot b/doc/graph/graph.dot index e27a4124..6463ce05 100644 --- a/doc/graph/graph.dot +++ b/doc/graph/graph.dot @@ -100,7 +100,7 @@ digraph G { "pkg/prjoxide" "pkg/prjtrellis" "pkg/superprove" - "pkg/symbiyosys" + "pkg/sby" "pkg/yices2" "pkg/yosys" "pkg/verible" @@ -298,7 +298,7 @@ digraph G { subgraph cluster_formal { label = "Formal"; m_formal -> { - "pkg/symbiyosys" + "pkg/sby" "pkg/boolector" "pkg/cvc" "pkg/pono" diff --git a/doc/tools.yml b/doc/tools.yml index 7fcb723b..ccf19c70 100644 --- a/doc/tools.yml +++ b/doc/tools.yml @@ -316,10 +316,10 @@ superprove: #--- -symbiyosys: +sby: src: true pkg: - - 'symbiyosys' + - 'sby' in: - 'formal/min' - 'formal' diff --git a/test/symbiyosys.pkg.sh b/test/sby.pkg.sh similarity index 100% rename from test/symbiyosys.pkg.sh rename to test/sby.pkg.sh diff --git a/utils/pyHDLC/config.yml b/utils/pyHDLC/config.yml index 17875db7..c8dea6be 100644 --- a/utils/pyHDLC/config.yml +++ b/utils/pyHDLC/config.yml @@ -73,7 +73,7 @@ defaults: pkg/cvc: *EmptyTarget pkg/pono: *EmptyTarget pkg/superprove: *EmptyTarget - pkg/symbiyosys: *EmptyTarget + pkg/sby: *EmptyTarget pkg/yices2: *EmptyTarget pkg/z3: *EmptyTarget formal/min: { <<: *FormalDockerfile, target: min } @@ -178,7 +178,7 @@ jobs: cvc: *SysDebianAmd64 pono: *SysDebianBullseyeAmd64 superprove: *SysDebianBullseyeAmd64 - symbiyosys: *SysDebianAmd64 + sby: *SysDebianAmd64 yices2: *SysDebianAmd64 z3: *SysDebianAmd64