yosys

History

Ethan Mahintorabi 82a4a87c97 Fixes error with vector indicies of the form [2:7] [-12:7] Make sure that we correctly adjust the value to align it to a zero indexed list with lsb = 0 Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>		2024-05-08 20:29:47 +00:00
..
Makefile.inc	Verific support for VHDL 2019	2024-03-28 13:21:55 +01:00
README	Update README	2022-07-28 12:32:19 +02:00
example.sby	Improve docs for verific bindings, add simply sby example	2017-07-22 11:58:51 +02:00
example.sv	Improve docs for verific bindings, add simply sby example	2017-07-22 11:58:51 +02:00
verific.cc	Fixes error with vector indicies of the form [2:7] [-12:7]	2024-05-08 20:29:47 +00:00
verific.h	verific: Fixes incorrect aldff inference in verific importer	2024-02-05 07:10:25 +00:00
verificsva.cc	verific: Handle non-seq properties with VerificClocking conditions	2023-04-21 17:19:42 +02:00

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)