diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..0301b8f
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+bazel-*
+*.swp
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..cb8000d
--- /dev/null
+++ b/README.md
@@ -0,0 +1,33 @@
+# rules_symbiyosys
+
+Provides [Bazel](https://bazel.build/) rules for
+[Symbiyosys](https://symbiyosys.readthedocs.io/en/latest/).
+
+Currently the only supported engine is `smtbmc` with the `yices` solver.
+
+`symbiyosys_test` is provided as a Bazel test rule.  `symbiyosys_trace` utilizes `gtkwave_wrapper`
+from [rules_verilog](https://github.com/agoessling/rules_verilog) to view traces produced by
+Symbiyosys.
+
+## Usage
+
+See [examples/BUILD](examples/BUILD) for example usage.
+
+### WORKSPACE
+
+To incorporate `rules_symbiyosys` into your project copy the following into your `WORKSPACE` file.
+
+```Starlark
+load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
+
+http_archive(
+    name = "rules_symbiyosys",
+    # See release page for latest version url and sha.
+)
+
+load("@rules_symbiyosys//symbiyosys:direct_repositories.bzl", "rules_symbiyosys_direct_deps")
+rules_symbiyosys_direct_deps()
+
+load("@rules_symbiyosys//symbiyosys:indirect_repositories.bzl", "rules_symbiyosys_indirect_deps")
+rules_symbiyosys_indirect_deps()
+```
diff --git a/WORKSPACE b/WORKSPACE
new file mode 100644
index 0000000..57b9b7d
--- /dev/null
+++ b/WORKSPACE
@@ -0,0 +1,7 @@
+workspace(name = "rules_symbiyosys")
+
+load("@rules_symbiyosys//symbiyosys:direct_repositories.bzl", "rules_symbiyosys_direct_deps")
+rules_symbiyosys_direct_deps()
+
+load("@rules_symbiyosys//symbiyosys:indirect_repositories.bzl", "rules_symbiyosys_indirect_deps")
+rules_symbiyosys_indirect_deps()
diff --git a/examples/BUILD b/examples/BUILD
new file mode 100644
index 0000000..0aa837a
--- /dev/null
+++ b/examples/BUILD
@@ -0,0 +1,61 @@
+load(
+    "@rules_symbiyosys//symbiyosys:defs.bzl",
+    "symbiyosys_test",
+    "symbiyosys_trace",
+)
+load("@rules_verilog//verilog:defs.bzl", "verilog_module")
+
+verilog_module(
+    name = "counter_top",
+    top = "counter_top",
+    srcs = [
+        "counter_top.sv",
+    ],
+    deps = [":counter"],
+)
+
+verilog_module(
+    name = "counter",
+    top = "counter",
+    srcs = ["counter.sv"],
+)
+
+symbiyosys_test(
+    name = "counter_pass",
+    module = ":counter_top",
+    params = {
+        "MAX_VAL": "3",
+    },
+    modes = [
+        "bmc",
+        "prove",
+    ],
+    depth = 20,
+    engine = "smtbmc",
+)
+
+symbiyosys_test(
+    name = "counter_fail",
+    module = ":counter_top",
+    params = {
+        "MAX_VAL": "15",
+    },
+    modes = [
+        "bmc",
+        "prove",
+    ],
+    depth = 20,
+    engine = "smtbmc",
+)
+
+symbiyosys_trace(
+    name = "counter_pass_trace",
+    test = ":counter_pass",
+    testonly = True,
+)
+
+symbiyosys_trace(
+    name = "counter_fail_trace",
+    test = ":counter_fail",
+    testonly = True,
+)
diff --git a/examples/counter.sv b/examples/counter.sv
new file mode 100644
index 0000000..94ce506
--- /dev/null
+++ b/examples/counter.sv
@@ -0,0 +1,24 @@
+module counter #(
+    parameter MAX_VAL = 3
+) (
+    input logic i_clk,
+    output logic [5:0] o_count
+);
+
+  initial o_count = 0;
+
+  always_ff @(posedge i_clk) begin
+    if (o_count == MAX_VAL) begin
+      o_count <= 0;
+    end else begin
+      o_count <= o_count + 1;
+    end
+  end
+
+`ifdef FORMAL
+  always_ff @(posedge i_clk) begin
+    assert(o_count < 10);
+  end
+`endif
+
+endmodule
diff --git a/examples/counter_top.sv b/examples/counter_top.sv
new file mode 100644
index 0000000..18a81da
--- /dev/null
+++ b/examples/counter_top.sv
@@ -0,0 +1,19 @@
+module counter_top #(
+    parameter MAX_VAL = 15
+) (
+    input logic i_clk
+);
+
+  logic [5:0] count;
+  counter #(.MAX_VAL(MAX_VAL)) counter (
+      .i_clk,
+      .o_count(count)
+  );
+
+`ifdef FORMAL
+  always_comb begin
+    assert(!(count & (1 << 5)));
+  end
+`endif
+
+endmodule
diff --git a/symbiyosys/BUILD b/symbiyosys/BUILD
new file mode 100644
index 0000000..e69de29
diff --git a/symbiyosys/defs.bzl b/symbiyosys/defs.bzl
new file mode 100644
index 0000000..507ce9c
--- /dev/null
+++ b/symbiyosys/defs.bzl
@@ -0,0 +1,166 @@
+load("@rules_verilog//verilog:defs.bzl", "VerilogModuleInfo")
+
+def _short_dir(f):
+  """Return the directory of the short_path."""
+  return f.short_path[:-len(f.basename)]
+
+
+def _get_binary(target, name):
+    """Return the file associated with name in target."""
+    # rules_foreign_cc creates one binary per output group.
+    return getattr(target[OutputGroupInfo], name).to_list()[0]
+
+
+def _symbiyosys_test_impl(ctx):
+    top = ctx.attr.module[VerilogModuleInfo].top
+    files = ctx.attr.module[VerilogModuleInfo].files.to_list()
+
+    # Need to explicitly add runfiles prefix so paths are correct both when run directly and when
+    # run from another rule.
+    prefix = "${{RUNFILES_DIR}}/{}/".format(ctx.workspace_name)
+
+    shell_cmd = [
+        prefix + ctx.executable._symbiyosys_wrapper.short_path,
+        "--sby_path",
+        prefix + ctx.executable._symbiyosys_toolchain.short_path,
+        "--yosys_path",
+        prefix + _get_binary(ctx.attr._yosys_toolchain, "yosys").short_path,
+        "--abc_path",
+        prefix + _get_binary(ctx.attr._yosys_toolchain, "yosys-abc").short_path,
+        "--smtbmc_path",
+        prefix + _get_binary(ctx.attr._yosys_toolchain, "yosys-smtbmc").short_path,
+        "--solver_paths",
+        prefix + _short_dir(_get_binary(ctx.attr._yices_toolchain, "yices")),
+        "--modes",
+        " ".join(ctx.attr.modes),
+        "--engine",
+        ctx.attr.engine,
+        "--top",
+        top,
+        "--params",
+        " ".join([k + "=" + v for k, v in ctx.attr.params.items()]),
+        "--depth",
+        str(ctx.attr.depth),
+        " ".join([prefix + f.short_path for f in files]),
+        "$@",
+    ]
+
+    script = ctx.actions.declare_file("{}.sh".format(ctx.label.name))
+    ctx.actions.write(script, " ".join(shell_cmd), is_executable = True)
+
+    runfiles = ctx.runfiles(
+        files = files,
+        transitive_files = depset(transitive = [
+            ctx.attr._symbiyosys_wrapper[DefaultInfo].default_runfiles.files,
+            ctx.attr._symbiyosys_toolchain[DefaultInfo].default_runfiles.files,
+            ctx.attr._yosys_toolchain[DefaultInfo].files,
+            ctx.attr._yices_toolchain[DefaultInfo].files,
+        ]),
+    )
+    return [DefaultInfo(executable = script, runfiles = runfiles)]
+
+
+symbiyosys_test = rule(
+    implementation = _symbiyosys_test_impl,
+    doc = "Formal verification of (System) Verilog.",
+    attrs = {
+        "module": attr.label(
+            doc = "Module to test.",
+            mandatory = True,
+            providers = [VerilogModuleInfo],
+        ),
+        "params": attr.string_dict(
+            doc = "Verilog parameters for top module.",
+        ),
+        "modes": attr.string_list(
+            doc = "Modes of verification.",
+            mandatory = True,
+            allow_empty = False,
+        ),
+        "depth": attr.int(
+            doc = "Solver depth.",
+            default = 20,
+        ),
+        "engine": attr.string(
+            doc = "Verification engine.",
+            default = "smtbmc",
+        ),
+        "_symbiyosys_wrapper": attr.label(
+            doc = "Symbiyosys wrapper script.",
+            default = Label("@rules_symbiyosys//symbiyosys/tools:symbiyosys_wrapper"),
+            executable = True,
+            cfg = "target",
+        ),
+        "_symbiyosys_toolchain": attr.label(
+            doc = "Symbiyosys toolchain.",
+            default = Label("@symbiyosys_archive//:sby"),
+            executable = True,
+            cfg = "target",
+        ),
+        "_yosys_toolchain": attr.label(
+            doc = "Yosys toolchain.",
+            default = Label("@rules_symbiyosys//symbiyosys/tools:yosys"),
+        ),
+        "_yices_toolchain": attr.label(
+            doc = "Yices toolchain.",
+            default = Label("@rules_symbiyosys//symbiyosys/tools:yices"),
+        ),
+    },
+    test = True,
+)
+
+
+def _symbiyosys_trace_impl(ctx):
+    # Run test to generate VCD directory / files.
+    vcd_dir = ctx.actions.declare_directory("{}_vcd".format(ctx.label.name))
+
+    args = ctx.actions.args()
+    args.add("--vcd_dir")
+    args.add(vcd_dir.path)
+    args.add("--ignore_failure")
+
+    ctx.actions.run(outputs = [vcd_dir], executable = ctx.executable.test, arguments = [args],
+                    env = {
+                        "RUNFILES_DIR": ctx.executable.test.path + ".runfiles",
+                        "PATH": "/usr/local/bin:/usr/bin:/bin"
+                    })
+
+    # Wrap gtk_wrapper in order to bake in arguments.
+    shell_cmd = [
+        ctx.executable._gtkwave_wrapper.short_path,
+        "--vcd_dir",
+        vcd_dir.short_path,
+        "--open_level",
+        "1",
+        "$@",
+    ]
+    shell_script = ctx.actions.declare_file(ctx.label.name + ".sh")
+    ctx.actions.write(shell_script, " ".join(shell_cmd), is_executable = True)
+
+    runfiles = ctx.runfiles(files = [vcd_dir])
+
+    for attr in [ctx.attr._gtkwave_wrapper, ctx.attr.test]:
+      runfiles = runfiles.merge(attr[DefaultInfo].default_runfiles)
+
+    return [DefaultInfo(executable = shell_script, runfiles = runfiles)]
+
+
+symbiyosys_trace = rule(
+    implementation = _symbiyosys_trace_impl,
+    doc = "View VCD trace from Symbiyosys.",
+    attrs = {
+        "test": attr.label(
+            doc = "Symbiyosys test target to produce VCD file.",
+            mandatory = True,
+            executable = True,
+            cfg = "target",
+        ),
+        "_gtkwave_wrapper": attr.label(
+            doc = "GTKwave wrapper script.",
+            default = Label("@rules_verilog//gtkwave:gtkwave_wrapper"),
+            executable = True,
+            cfg = "target",
+        ),
+    },
+    executable = True,
+)
diff --git a/symbiyosys/direct_repositories.bzl b/symbiyosys/direct_repositories.bzl
new file mode 100644
index 0000000..fafbcfd
--- /dev/null
+++ b/symbiyosys/direct_repositories.bzl
@@ -0,0 +1,47 @@
+load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
+
+def rules_symbiyosys_direct_deps():
+    http_archive(
+        name = "rules_verilog",
+        strip_prefix = "rules_verilog-0.1.0",
+        sha256 = "401b3f591f296f6fd2f6656f01afc1f93111e10b81b9a9d291f9c04b3e4a3e8b",
+        url = "https://github.com/agoessling/rules_verilog/archive/v0.1.0.zip",
+    )
+
+    http_archive(
+        name = "rules_foreign_cc",
+        strip_prefix = "rules_foreign_cc-ed95b95affecaa3ea3bf7bab3e0ab6aa847dfb06",
+        sha256 = "21177439c27c994fd9b6e04d4ed6cec79d7dbcf174649f8d70e396dd582d1c82",
+        url = "https://github.com/bazelbuild/rules_foreign_cc/archive/ed95b95affecaa3ea3bf7bab3e0ab6aa847dfb06.zip",
+    )
+
+    all_content = """
+filegroup(
+    name = "all",
+    srcs = glob(["**"]),
+    visibility = ["//visibility:public"],
+)"""
+
+    http_archive(
+        name = "yosys_archive",
+        build_file_content = all_content,
+        strip_prefix = "yosys-06347b119b08257eff37cdd10ed802e794c1a3cf",
+        sha256 = "33108d1ccf9ad4277071ad151994e428e8f39cafde30a0db9c910ac08056b7c3",
+        url = "https://github.com/YosysHQ/yosys/archive/06347b119b08257eff37cdd10ed802e794c1a3cf.zip",
+    )
+
+    http_archive(
+        name = "symbiyosys_archive",
+        build_file = "@rules_symbiyosys//symbiyosys/tools:symbiyosys.BUILD",
+        strip_prefix = "SymbiYosys-37a1fec1206c70c33565c0a1f3e6605d03ce47ac",
+        sha256 = "1719bdbf5d29a9d3038e2c57ddd9b2fcfcbc36bf8db4e875e7fce98d65daae60",
+        url = "https://github.com/YosysHQ/symbiyosys/archive/37a1fec1206c70c33565c0a1f3e6605d03ce47ac.zip",
+    )
+
+    http_archive(
+        name = "yices_archive",
+        build_file_content = all_content,
+        strip_prefix = "yices2-426cdc6037ee0e34309edbe4e10bcda9a7211a41",
+        sha256 = "8d29b11f2b05af1cb64ea5c5c01e46061e750b5724ff9595d477625a6f70edc6",
+        url = "https://github.com/SRI-CSL/yices2/archive/426cdc6037ee0e34309edbe4e10bcda9a7211a41.zip",
+    )
diff --git a/symbiyosys/indirect_repositories.bzl b/symbiyosys/indirect_repositories.bzl
new file mode 100644
index 0000000..61a2c03
--- /dev/null
+++ b/symbiyosys/indirect_repositories.bzl
@@ -0,0 +1,4 @@
+load("@rules_foreign_cc//:workspace_definitions.bzl", "rules_foreign_cc_dependencies")
+
+def rules_symbiyosys_indirect_deps():
+    rules_foreign_cc_dependencies()
diff --git a/symbiyosys/tools/BUILD b/symbiyosys/tools/BUILD
new file mode 100644
index 0000000..eeb44cd
--- /dev/null
+++ b/symbiyosys/tools/BUILD
@@ -0,0 +1,46 @@
+load("@rules_foreign_cc//tools/build_defs:make.bzl", "make")
+load("@rules_foreign_cc//tools/build_defs:configure.bzl", "configure_make")
+
+make(
+    name = "yosys",
+    lib_source = "@yosys_archive//:all",
+    binaries = [
+        "yosys",
+        "yosys-abc",
+        "yosys-filterlib",
+        "yosys-smtbmc",
+    ],
+    out_include_dir = "share",
+    make_commands = [
+        "make -j8",
+        "make install PREFIX=$$INSTALLDIR$$",
+    ],
+    tags = [
+        "requires-network",
+    ],
+    visibility = ["//visibility:public"],
+)
+
+configure_make(
+    name = "yices",
+    lib_source = "@yices_archive//:all",
+    binaries = [
+        "yices",
+        "yices-sat",
+        "yices-smt",
+        "yices-smt2",
+    ],
+    make_commands = [
+        "make -j8",
+        "make install PREFIX=$$INSTALLDIR$$",
+    ],
+    configure_in_place = True,
+    autoreconf = True,
+    visibility = ["//visibility:public"],
+)
+
+py_binary(
+    name = "symbiyosys_wrapper",
+    srcs = ["symbiyosys_wrapper.py"],
+    visibility = ["//visibility:public"],
+)
diff --git a/symbiyosys/tools/symbiyosys.BUILD b/symbiyosys/tools/symbiyosys.BUILD
new file mode 100644
index 0000000..05acdab
--- /dev/null
+++ b/symbiyosys/tools/symbiyosys.BUILD
@@ -0,0 +1,11 @@
+py_binary(
+    name = "sby",
+    srcs = ["sbysrc/sby.py"],
+    deps = [":sby_deps"],
+    visibility = ["//visibility:public"],
+)
+
+py_library(
+    name = "sby_deps",
+    srcs = glob(["sbysrc/sby_*.py"]),
+)
diff --git a/symbiyosys/tools/symbiyosys_wrapper.py b/symbiyosys/tools/symbiyosys_wrapper.py
new file mode 100644
index 0000000..10725b1
--- /dev/null
+++ b/symbiyosys/tools/symbiyosys_wrapper.py
@@ -0,0 +1,130 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import os
+import os.path
+import re
+import shutil
+import subprocess
+import sys
+import tempfile
+
+
+def get_config(modes, engine, top, srcs, depth, params):
+  config_str = ''
+  config_str = '[tasks]\n'
+  tasks = ['task_{:s}'.format(m) for m in modes]
+  config_str += '\n'.join(tasks)
+  config_str += '\n\n'
+
+  config_str += '[options]\n'
+  options = ['task_{:s}: mode {:s}'.format(m, m) for m in modes]
+  config_str += '\n'.join(options)
+  config_str += '\n'
+  options = ['task_{:s}: depth {:d}'.format(m, depth) for m in modes]
+  config_str += '\n'.join(options)
+  config_str += '\n\n'
+
+  config_str += '[engines]\n'
+  config_str += '{:s}\n'.format(engine)
+  config_str += '\n'
+
+  config_str += '[script]\n'
+  for f in srcs:
+    _, extension = os.path.splitext(f)
+    sv_flag = ' -sv' if extension == '.sv' else ''
+    config_str += 'read -formal{:s} -D{:s} {:s}\n'.format(sv_flag, top.upper(), os.path.basename(f))
+
+  for k, v in params.items():
+    config_str += 'chparam -set {:s} {} {:s}\n'.format(k, v, top)
+
+  config_str += 'prep -top {:s}\n'.format(top)
+  config_str += '\n'
+
+  config_str += '[files]\n'
+  config_str += '\n'.join(srcs)
+
+  return config_str
+
+
+class ParamAction(argparse.Action):
+  def __call__(self, parser, namespace, values, option_string=None):
+    setattr(namespace, self.dest, dict())
+    for value in values:
+      parts = value.split('=')
+
+      if len(parts) == 1:
+        parser.error('Argument "{}" contains no "=".'.format(value))
+      if len(parts) > 2:
+        parser.error('Argument "{}" contains multiple "=".'.format(value))
+
+      getattr(namespace, self.dest)[parts[0]] = parts[1]
+
+
+def main():
+  parser = argparse.ArgumentParser(description='Configure and run symbiyosys.')
+  parser.add_argument('--sby_path', required=True, help='Path to sby executable.')
+  parser.add_argument('--yosys_path', required=True, help='Path to yosys executable.')
+  parser.add_argument('--abc_path', required=True, help='Path to yosys-abc executable.')
+  parser.add_argument('--smtbmc_path', required=True, help='Path to yosys-smtbmc executable.')
+  parser.add_argument('--solver_paths', nargs='*', help='Solver paths to make available to Yosys.')
+  parser.add_argument('--modes', nargs='+', required=True, help='Task modes.')
+  parser.add_argument('--engine', default='smtbmc', help='Proof engine.')
+  parser.add_argument('--top', required=True, help='Top module name.')
+  parser.add_argument('--params', nargs='*', action=ParamAction, default={},
+      help='Params for top module. e.g. key=value')
+  parser.add_argument('--depth', type=int, default=20, help='Solver depth.')
+  parser.add_argument('--vcd_dir', help='Directory for output trace files.')
+  parser.add_argument('--ignore_failure', action='store_true',
+      help='Do not report error code from Symbiyosys.')
+  parser.add_argument('srcs', nargs='+', help='(System) verilog sources.')
+
+  args = parser.parse_args()
+
+  with tempfile.TemporaryDirectory() as directory:
+    with open(os.path.join(directory, 'config.sby'), 'w') as f:
+      config = get_config(args.modes, args.engine, args.top, args.srcs, args.depth, args.params)
+      f.write(config)
+
+    sby_args = [
+        os.path.abspath(args.sby_path),
+        '--yosys',
+        os.path.abspath(args.yosys_path),
+        '--abc',
+        os.path.abspath(args.abc_path),
+        '--smtbmc',
+        os.path.abspath(args.smtbmc_path),
+        os.path.join(directory, 'config.sby'),
+    ]
+
+    env = os.environ.copy()
+    paths = ':'.join([os.path.abspath(path) for path in args.solver_paths])
+    if paths:
+      env['PATH'] = paths + ':' + env['PATH']
+
+    completed = subprocess.run(sby_args, env=env)
+
+    if args.vcd_dir:
+      try:
+        os.mkdir(args.vcd_dir)
+      except FileExistsError:
+        pass
+
+      traces = glob.glob(os.path.join(directory, 'config_task_*/engine_0/*.vcd'))
+
+      for trace in traces:
+        match = re.search(r'config_task_(\w+)', trace)
+        if not match:
+          raise RuntimeError('Malformed trace file: {:s}'.format(trace))
+
+        mode = match.group(1)
+        name = '{:s}_{:s}'.format(mode, os.path.basename(trace))
+        shutil.copyfile(trace, os.path.join(args.vcd_dir, name))
+
+    if not args.ignore_failure:
+      sys.exit(completed.returncode)
+
+
+if __name__ == '__main__':
+  main()