Skip to content

Commit

Permalink
Implement basic verifier cli
Browse files Browse the repository at this point in the history
  • Loading branch information
gtarawneh committed Dec 17, 2017
1 parent d60f274 commit 2126ae4
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 3 deletions.
1 change: 1 addition & 0 deletions requirements.txt
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
jinja2
docopt
18 changes: 15 additions & 3 deletions verifier.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#!/usr/bin/env python

from docopt import docopt
from sg_parser import load_sg
from lib_parser import load_lib
from lib_parser import merge_libs
Expand All @@ -8,6 +9,15 @@

import json

usage = """verifier.py
Usage:
verifier.py [options] <circuit.v> <spec.sg>
Options:
-q --quiet Suppress printing state exploration details.
"""


def get_next_state(encoding, state, transition):
"""Compute the next after a transition."""
Expand Down Expand Up @@ -220,11 +230,13 @@ def main():

# Load library, circuit and spec

spec = load_sg("examples/buffers/spec-n50.sg")
circuit = load_verilog("examples/buffers/buffers-n50.v")
args = docopt(usage, version="verifier.py v0.1")

spec = load_sg(args["<spec.sg>"])
circuit = load_verilog(args["<circuit.v>"])
lib = load_lib("libraries/*.lib")

result, msg = verify_circuit(lib, circuit, spec, quiet=True)
result, msg = verify_circuit(lib, circuit, spec, quiet=args["--quiet"])

print("Result: " + ("PASS" if result else "FAIL"))

Expand Down

0 comments on commit 2126ae4

Please sign in to comment.