Verification research for general RTL/system-level designs (take 0.0)

git clone https://github.com/ric2k1/gv0-socv
cd gv0-socv/
# General Users
sudo ./SETUP.sh 
./INSTALL.sh

• For using GV tool interface, type after installation:

./gv

• Please notice that, if the shell script has no permission, type:

chmod +x <shell_script_filename>

• parser --> yosys, berkeley-abc
• file format converter --> yosys
• formal verification engine --> berkeley-abc
• simulator --> yosys

• Please check the document above to get detailed tutorials in "gv0-socv/doc/"

• Below are current supporting APIs, please type "help " for detailed usage

  • Common commands

  GV Help
  GV History 
  GV Usage
  GV Dofile
  GV Quit
  

  • Verify commands

  GV Formal Verify
  

  • Simulate commands

  GV Random Simulate
  GV SEt SAfe
  GV SHow
  

  • Network commands

  GV BLAst Ntk
  GV File2 Aig
  GV File2 Blif
  GV PRInt Aig
  GV PRint Info
  GV REad Design
  GV SEt Engine
  GV WRite aig
  GV YosysCMD
  

  • Abc commands

  GV ABCCMD
  GV ABCPrint
  GV ABCRead
  

  • Mode commands

  GV RESET SYStem
  GV SEt System
  GV WIZard
  

  • Bdd Commands

  GV BAND
  GV BCOFactor 
  GV BCOMpare 
  GV BConstruct 
  GV BDRAW 
  GV BEXist 
  GV BINV 
  GV BNAND 
  GV BNOR 
  GV BOR 
  GV BREPort 
  GV BRESET 
  GV BSETOrder 
  GV BSETVar 
  GV BSIMulate 
  GV BXNOR 
  GV BXOR 
  

  • Prove Commands

  GV PCHECKProperty
  GV PIMAGe 
  GV PINITialstate 
  GV PTRansrelation