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 @@ + + + + + vowstar@gmail.com + Huang Rui + + + 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. + + + SymbiYosys (sby) 是基于 Yosys 的形式化硬件验证流程的前端驱动程序。 + 它支持有界模型检查 (BMC)、无界模型检查和覆盖属性检查,适用于使用 + Verilog、SystemVerilog 或 VHDL 编写的硬件设计。SymbiYosys 集成了 + 多种 SMT 求解器和模型检查器,包括 Yices、Z3、Boolector 和 ABC。 + + + Enable Yices2 SMT solver support + + + YosysHQ/sby + https://github.com/YosysHQ/sby/issues + + 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 +}