Skip to content

Latest commit

 

History

History
40 lines (28 loc) · 1.54 KB

README.md

File metadata and controls

40 lines (28 loc) · 1.54 KB
Raw

Sylvia - A Software-Style Symbolic Execution Engine for Verilog

Setup

Requirements

  • Python3: 3.8 or later
  • z3: run python3 -m pip install z3-solver
  • Icarus Verilog: 10.1 or later: run sudo apt install iverilog
  • Jinja 2.10 or later: run python3 -m pip install jinja2
  • PLY 3.4 or later: run python3 -m pip install ply
  • Graphviz 2.38.0 or later: run sudo apt install graphviz
  • Pygraphviz 1.3.1 or later: run python3 - m pip install pygraphviz. If you have trouble with this step with errors related to building wheel for pygraphviz, try running sudo apt install graphviz-dev and then rerunning the python3 - m pip install pygraphviz command.
  • PyVerilog: run python3 -m pip install pyverilog
  • networkx: run python3 -m pip install networkx
  • matplotlib: run python3 -m pip install matplotlib

Download

git clone https://github.com/kakiryan/Sylvia

cd Sylvia

Running Sylvia

The following command should get you started with a basic run of symbolic execution:

python3 -m main 1 designs/test-designs/updowncounter.v > out.txt

The expected usage of Sylvia is:

python3 -m main {num_cycles} {list of verilog files}

python3 -m main 1 designs/test-designs/test.v designs/test-designs/test_2.v > out.txt for example is a command with two example verilog files.

You can run:

python3 -m main --help for information about the different flags you can run Sylvia with. -B will display the initial & final symbolic store and path condition for each clock cycle during the run.