Source code for edalize.symbiyosys

# Copyright edalize contributors
# Licensed under the 2-Clause BSD License, see LICENSE for details.
# SPDX-License-Identifier: BSD-2-Clause

import os
import re
import jinja2

from edalize.edatool import Edatool

[docs] class Symbiyosys(Edatool): _description = """SymbiYosys backend SymbiYosys is a wrapper around yosys to make it easier to do formal verification. Example snippet in CAPI2 format: .. code:: yaml symbiyosys: tasknames: # A list of task names to pass to sby. Defaults to empty (in which case # sby will run each task in the .sby file) - my_proof The SymbiYosys tool expects a configuration file telling it what to do. This file includes a list of all the source files, together with various flags which we'd like to make customizable (we support vlogdefine and vlogparam). To use the Edalize wrapper, you should include exactly one source file with file type 'sbyConfigTemplate'. This template file is a Jinja2 template and is expanded to yield a ``test.sby`` in the build directory. The sby file format expects a list of input files (twice: each file needs to appear in a read line at the start of the ``[script]`` section, then again in the ``[files]`` section). To make this a bit easier, the Edalize backend supplies several variables and a custom filter. If you don't need to do anything particularly complicated, start your script section with something like this: .. code:: [script] {{"-sv"|gen_reads}} This will expand to something like: .. code:: [script] read -sv -Ddefine1=1 -Ddefine2=2 -Isome/include/dir read -sv -Ddefine1=1 -Ddefine2=2 -Isome/include/dir chparam -set foo 'bar' -set baz 'qux' my_toplevel Here, the list of files is the list of files given to Edalize in the first place. The include directories also come from the file list (calculated by Edalize's internal fileset tracking). The defines come from ``vlogdefine`` parameters and the chparam command comes from ``vlogparam`` parameters. Similarly, write a files section like this: .. code:: [files] {{files}} which will expand to .. code:: [files] ../path/to/some/ ../path/to/ If you need more control over the read commands at the start of the script section, there are some variables that can help you. - ``{{chparam}}`` expands to the chparam command at the end of gen_reads as shown above. - ``{{flags}}`` expands to the flags (defines and includes) used for each read line. - ``{{src_files}}`` expands to a list with the basename of each source file. - ``{{top_level}}`` exands to the name of the top-level module. You can reproduce the example above with something like .. code:: [script] {% for name in src_files %} read -sv {{flags}} {{name}} {% endfor %} {{chparam}} """ argtypes = ["vlogdefine", "vlogparam"] tool_options = { "lists": { # A list of tasks to run from the .sby file. Passed on the sby # command line. "tasknames": "String" } } def __init__(self, edam=None, work_root=None, eda_api=None, verbose=True): super(Symbiyosys, self).__init__(edam, work_root, eda_api, verbose) # Register Jinja filters self.jinja_env.filters["gen_reads"] = self._gen_reads # The list of RTL paths in the fileset (populated at configure time by # _get_file_names) self.rtl_paths = None # The list of include directories in the fileset (populated at # configure time by _get_file_names) self.incdirs = None # The name of the interpolated .sby file that we create in the work # root self.sby_name = "test.sby"
[docs] @staticmethod def get_doc(api_ver): if api_ver == 0: return { "description": "SymbiYosys formal verification wrapper for Yosys", "lists": [ { "name": "tasknames", "type": "String", "desc": ( "A list of the .sby file's tasks to run. " "Passed on the sby command line." ), } ], }
def _get_file_names(self): """Read the fileset to get our file names""" assert self.rtl_paths is None src_files, self.incdirs = self._get_fileset_files() self.rtl_paths = [] bn_to_path = {} sby_names = [] # RTL files have types verilogSource or systemVerilogSource*. We # presumably want some of them. The .sby file has type sbyConfig: we # want exactly one of them. ft_re = re.compile(r"(:?systemV|v)erilogSource") for file_obj in src_files: if ft_re.match(file_obj.file_type): self.rtl_paths.append( # Check that basenames are unique (otherwise sby's behaviour of # copying everything into the same directory isn't going to # work). basename = os.path.basename( if basename in bn_to_path: raise RuntimeError( "More than one RTL file with the same" "basename: {!r} and {!r}.".format( bn_to_path[basename], ) ) bn_to_path[basename] = continue if file_obj.file_type == "sbyConfigTemplate": sby_names.append( continue # Ignore anything else if len(sby_names) != 1: raise RuntimeError( "SymbiYosys expects exactly one file with type " "sbyConfigTemplate (the one called " "something.sby.j2). We have {}.".format(sby_names or "none") ) return sby_names[0] def _get_read_flags(self): """ Return a string with the flags that should be passed for each read. These are exposed as the {{flags}} variable in Jinja templates. """ return " ".join( [ "-D{}={}".format(key, self._param_value_str(value)) for key, value in self.vlogdefine.items() ] + ["-I{}".format(inc) for inc in self.incdirs] ) def _get_chparam(self): """ Return a string for the {{chparam}} variable. """ if not self.vlogparam: return "" chparam_lst = ["chparam"] for key, value in self.vlogparam.items(): chparam_lst += [ "-set", key, self._param_value_str(param_value=value, str_quote_style='"'), ] chparam_lst.append(self.toplevel) return " ".join(chparam_lst) def _gen_reads(self, value): """ Custom jinja filter that generates read lines for each source file. We expect it to be used like this: {{"-sv"|gen_reads}} See the class documentation for more details. """ base_cmd = "read {} {} ".format(value, self._get_read_flags()) lines = [] for path in self.rtl_paths: lines.append(base_cmd + os.path.basename(path)) chparam = self._get_chparam() if chparam: lines.append(chparam) return "\n".join(lines) def _interpolate_sby(self, src): """ Patch a .sby template to read the right paths. The input file should be a Jinja template. We expect it not to have much templating, but the user will probably want to use templating for the list of source files (that has to appear twice). See the class documentation for details of the templating variables. """ # This should have been set by _get_file_names by now assert self.rtl_paths is not None src_path = os.path.join(self.work_root, src) dst_path = os.path.join(self.work_root, self.sby_name) # Load the source sby file as a Jinja2 template. We load it directly # (rather than through self.jinja_env) because it's user-supplied, # rather than living somewhere in the Edalize tree. with open(src_path) as sf: try: template = self.jinja_env.from_string( except jinja2.TemplateError as err: raise RuntimeError( "Failed to load {!r} " "as a Jinja2 template: {}.".format(src_path, err) ) files = "\n".join(self.rtl_paths) template_ctxt = { "chparam": self._get_chparam(), "files": files, "flags": self._get_read_flags(), "src_files": [os.path.basename(p) for p in self.rtl_paths], "top_level": self.toplevel, } with open(dst_path, "w") as df: df.write(template.render(template_ctxt)) def _dump_file_lists(self): """ Dump the list of RTL files and incdirs in work_root. This is useful if you need to run some sort of hook that consumes the list of files (to run sv2v in place on them, for example). The list of RTL files goes to files.txt and the list of include directories goes to incdirs.txt. """ with open(os.path.join(self.work_root, "files.txt"), "w") as handle: handle.write("\n".join(self.rtl_paths) + "\n") with open(os.path.join(self.work_root, "incdirs.txt"), "w") as handle: handle.write("\n".join(self.incdirs) + "\n")
[docs] def configure_main(self): clean_sby_name = self._get_file_names() self._interpolate_sby(clean_sby_name) self._dump_file_lists()
[docs] def build_main(self): pass
[docs] def run_main(self): tasknames = self.tool_options.get("tasknames", []) if not isinstance(tasknames, list): raise RuntimeError( '"tasknames" tool option should be ' "a list of strings. Got {!r}.".format(tasknames) ) self._run_tool("sby", ["-d", "build", self.sby_name] + tasknames)