frontends/verific/README

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