Gentoo Packages

Search

Install

Install this package:

emerge -a sci-electronics/sby

Package Information

Description:

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.

Homepage:

https://github.com/YosysHQ/sby

License:

ISC

Versions

Metadata

Description

• 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。

Maintainers

• Huang Rui (vowstar@gmail.com) - Type: person

Upstream

• Bugs: https://github.com/YosysHQ/sby/issues
• Remote IDs:
  • github: YosysHQ/sby

<pkgmetadata>
	<maintainer type="person">
		<email>vowstar@gmail.com</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>
		<bugs-to>https://github.com/YosysHQ/sby/issues</bugs-to>
		<remote-id type="github">YosysHQ/sby</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Warning] Ebuild 0.68 has a line exceeding 80 positions on line 56.
• [Warning] Ebuild 0.67 has a line exceeding 80 positions on line 56.
• [Warning] USE flag 'test' in ebuild 0.68 is not documented in metadata.xml
• [Warning] USE flag 'test' in ebuild 0.67 is not documented in metadata.xml
• [Error] Manifest entry for unused DIST file 'sby-0.67.tar.gz'
• [Error] Manifest entry for unused DIST file 'sby-0.68.tar.gz'
• [Error] Repository is missing a repo-name in metadata/layout.conf or profiles/repo_name
• [Notice] Package has only unstable keywords for arch(es): [ amd64 ], all versions are unstable: [ 0.67, 0.68 ]

USE Flags

Manage flags for this package: euse -i <flag> -p sci-electronics/sby | euse -E <flag> -p sci-electronics/sby | euse -D <flag> -p sci-electronics/sby

Manifest