Initial commit.

.gitignore

@@ -0,0 +1,2 @@
+bazel-*
+*.swp

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()
+```

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()

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,
+)

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

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

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,
+)

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",
+    )

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()