yosys

mirror of https://github.com/YosysHQ/yosys synced 2026-07-15 11:45:41 +00:00

Akash Levy 2f8c9327b3 Verific: guard large-mem RAM width/word-count against int overflow Address review feedback on the large-memory fix: - comment explaining the 64-bit promotion and the remaining int limits - log_error if the per-word width or word count would overflow RTLIL's int memory->width / memory->size fields, instead of silently truncating Co-authored-by: Cursor <cursoragent@cursor.com>		2026-06-24 23:33:55 -07:00
..
CMakeLists.txt	CMake: integrate silimate additions and extensions	2026-06-10 20:27:52 +03:00
example.sby
example.sv
README
verific.cc	Verific: guard large-mem RAM width/word-count against int overflow	2026-06-24 23:33:55 -07:00
verific.h
verificsva.cc

README

This directory contains Verific bindings for Yosys.

Use Tabby CAD Suite from YosysHQ if you need Yosys+Verific.
https://www.yosyshq.com/

Contact YosysHQ at contact@yosyshq.com for free evaluation
binaries of Tabby CAD Suite.


Verific Features that should be enabled in your Verific library
===============================================================

database/DBCompileFlags.h:
	DB_PRESERVE_INITIAL_VALUE


Testing Verific+Yosys+SymbiYosys for formal verification
========================================================

Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions:
http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing

Then run in the following command in this directory:

	sby -f example.sby

This will generate approximately one page of text output. The last lines
should be something like this:

	SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
	SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase
	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction
	SBY [example] summary: successful proof by k-induction.
	SBY [example] DONE (PASS, rc=0)