Configuration File ParsingΒΆ

The configuration file parsing API is split into the following parts:

Example

The following example uses the declarative API to define a small subset of the SBY config syntax:

import yosys_mau.config_parser as cfg
from yosys_mau import source_str
from yosys_mau.source_str import report

class Options(cfg.ConfigOptions):
    mode = cfg.Option(cfg.EnumValue("bmc", "prove"))
    depth = cfg.Option(cfg.IntValue(min=0), default=20)
    multiclock = cfg.Option(cfg.BoolValue(), default=False)

class Engines(cfg.ConfigCommands):
    def setup(self):
        self.smtbmc_args: list[str] = []
        self.abc_args: list[str] = []

    @cfg.command(cfg.StrValue())
    def smtbmc(self, arguments: str):
        self.smtbmc_args.append(arguments)

    @cfg.command(cfg.StrValue())
    def abc(self, arguments: str):
        self.abc_args.append(arguments)

    def unrecognized_command(self, command: cfg.ConfigCommand):
        raise report.InputError(
            command.name,
            f"unrecognized engine `{command.name}`",
        )

class ExampleConfig(cfg.ConfigParser):
    file = cfg.StrSection().with_arguments()

    @cfg.postprocess_section(cfg.StrSection())
    def files(self, section: str) -> list[str]:
        return section.splitlines()

    script = cfg.StrSection()
    options = cfg.OptionsSection(Options)
    engines = cfg.CommandsSection(Engines, required=True)

It can parse a config file like this:

[options]
mode bmc
depth 200
multiclock on

[engines]
smtbmc yices
smtbmc bitwuzla
abc bmc3

[script]
read -formal top.sv

[file top.sv]
module top(...);
...
endmodule

[file defines.sv]
`define SOME_DEFINE

[files]
more.sv
source.sv
files.sv

When the contents of the file are read into a string example_input using read_file, the parsed configuration can be accessed as follows:

config = ExampleConfig(example_input)

assert config.options.mode == "bmc"
assert config.options.depth == 200
assert config.options.multiclock

assert config.engines.smtbmc_args == ["yices", "bitwuzla"]
assert config.engines.abc_args == ["bmc3"]

assert config.script == "read -formal top.sv\n\n"

assert config.file["top.sv"] == "module top(...);\n...\nendmodule\n\n"
assert config.file["defines.sv"] == "`define SOME_DEFINE\n\n"

assert config.files == ["more.sv", "source.sv", "files.sv"]