frontends/verific/README

   1
   2 This directory contains Verific bindings for Yosys.
   3
   4 Use Tabby CAD Suite from YosysHQ if you need Yosys+Verifc.
   5 https://www.yosyshq.com/
   6
   7 Contact YosysHQ at contact@yosyshq.com for free evaluation
   8 binaries of Tabby CAD Suite.
   9
  10
  11 Verific Features that should be enabled in your Verific library
  12 ===============================================================
  13
  14 database/DBCompileFlags.h:
  15         DB_PRESERVE_INITIAL_VALUE
  16
  17
  18 Testing Verific+Yosys+SymbiYosys for formal verification
  19 ========================================================
  20
  21 Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions:
  22 http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing
  23
  24 Then run in the following command in this directory:
  25
  26         sby -f example.sby
  27
  28 This will generate approximately one page of text output. The last lines
  29 should be something like this:
  30
  31         SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
  32         SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
  33         SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase
  34         SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction
  35         SBY [example] summary: successful proof by k-induction.
  36         SBY [example] DONE (PASS, rc=0)
  37