commit: 423f66557034c4bddcf311162390ea6253232e61 Author: Huang Rui <vowstar <AT> gmail <DOT> com> AuthorDate: Sat Dec 6 12:35:35 2025 +0000 Commit: Paul Zander <negril.nx+gentoo <AT> gmail <DOT> com> CommitDate: Sat Dec 6 12:35:35 2025 +0000 URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=423f6655
sci-electronics/sby: new package, add 0.60 Signed-off-by: Huang Rui <vowstar <AT> gmail.com> sci-electronics/sby/Manifest | 1 + sci-electronics/sby/metadata.xml | 29 +++++++++++++++++++++ sci-electronics/sby/sby-0.60.ebuild | 50 +++++++++++++++++++++++++++++++++++++ 3 files changed, 80 insertions(+) diff --git a/sci-electronics/sby/Manifest b/sci-electronics/sby/Manifest new file mode 100644 index 0000000000..66e322610f --- /dev/null +++ b/sci-electronics/sby/Manifest @@ -0,0 +1 @@ +DIST sby-0.60.tar.gz 173761 BLAKE2B f1da6db7f65c2bf251583fa77fffcfe224ace1a5d2d45d0cbc6884be9afcd178e1ea4f4dc8762988c709dd17c4751fffb90e4ec8aaaa893b57a4963cf17980a9 SHA512 985ccce14784d566af4d74da4415cc28815748d9df42ac24126b06b05978fe2284f8d4b9e63e248941a5fe96ca539162117b5d255eafb18987568888d94a415a diff --git a/sci-electronics/sby/metadata.xml b/sci-electronics/sby/metadata.xml new file mode 100644 index 0000000000..33a3784f13 --- /dev/null +++ b/sci-electronics/sby/metadata.xml @@ -0,0 +1,29 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd";> +<pkgmetadata> + <maintainer type="person"> + <email>[email protected]</email> + <name>Huang Rui</name> + </maintainer> + <longdescription lang="en"> + SymbiYosys (sby) is a front-end driver program for Yosys-based formal + hardware verification flows. It supports bounded model checking (BMC), + unbounded model checking, and cover property checking for hardware + designs written in Verilog, SystemVerilog, or VHDL. SymbiYosys + integrates with various SMT solvers and model checkers including + Yices, Z3, Boolector, and ABC. + </longdescription> + <longdescription lang="zh"> + SymbiYosys (sby) 是基于 Yosys 的形式化硬件验证流程的前端驱动程序。 + 它支持有界模型检查 (BMC)、无界模型检查和覆盖属性检查，适用于使用 + Verilog、SystemVerilog 或 VHDL 编写的硬件设计。SymbiYosys 集成了 + 多种 SMT 求解器和模型检查器，包括 Yices、Z3、Boolector 和 ABC。 + </longdescription> + <use> + <flag name="yices2">Enable Yices2 SMT solver support</flag> + </use> + <upstream> + <remote-id type="github">YosysHQ/sby</remote-id> + <bugs-to>https://github.com/YosysHQ/sby/issues</bugs-to> + </upstream> +</pkgmetadata> diff --git a/sci-electronics/sby/sby-0.60.ebuild b/sci-electronics/sby/sby-0.60.ebuild new file mode 100644 index 0000000000..0fa84967a8 --- /dev/null +++ b/sci-electronics/sby/sby-0.60.ebuild @@ -0,0 +1,50 @@ +# Copyright 2025 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +PYTHON_COMPAT=( python3_{11..14} ) + +inherit python-single-r1 + +DESCRIPTION="Front-end for Yosys-based formal hardware verification flows" +HOMEPAGE="https://github.com/YosysHQ/sby"; +SRC_URI="https://github.com/YosysHQ/${PN}/archive/v${PV}.tar.gz -> ${P}.tar.gz" + +LICENSE="ISC" +SLOT="0" +KEYWORDS="~amd64" +IUSE="yices2" +REQUIRED_USE="${PYTHON_REQUIRED_USE}" + +RDEPEND=" + ${PYTHON_DEPS} + $(python_gen_cond_dep ' + dev-python/click[${PYTHON_USEDEP}] + ') + sci-electronics/yosys + sci-mathematics/z3 + yices2? ( sci-mathematics/yices2 ) +" +DEPEND="${RDEPEND}" + +src_install() { + # Install Python modules to yosys shared directory + insinto /usr/share/yosys/python3 + doins sbysrc/sby_*.py + + # Install sby_core.py with program prefix substitution + sed -e 's|##yosys-program-prefix##|""|' \ + sbysrc/sby_core.py > "${T}/sby_core.py" || die + doins "${T}/sby_core.py" + + # Create the sby launcher script with path and version substitutions + # Use absolute path with EPREFIX because python-exec wrapper changes script location + local syspath="sys.path += [\"${EPREFIX}/usr/share/yosys/python3\"]" + sed -e "s|##yosys-sys-path##|${syspath}|" \ + -e "s|##yosys-release-version##|release_version = 'SBY ${PV}'|" \ + sbysrc/sby.py > "${T}/sby" || die + python_newscript "${T}/sby" sby + + dodoc README.md +}
