search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
387 stars 73 forks source link

Autotune: Automatic engine selection #158

Closed jix closed 2 years ago

jix commented 2 years ago

First usable version of an automatic engine selection. Running with sby -f --autotune some_config.sby ignores the engine configured in the sby file and tries several different engines/engine configs in parallel. This required refactoring the core taskloop a bit, to isolate different engine runs from each other (giving each their own SbyTask sharing a single task loop) while at the same time reusing the same generated models (by having a common SbyTask for the overall autotune run).

When there are more configs to try than cores, this uses a soft timeout that is increased before the same config is retried again. These retries come with a constant factor overhead, but ensure that no effectively-forever-stuck config prevents us from making progress.

While autotune avoids generating the same model multiple times, it does keep track of the time needed to generate a model and takes that under consideration for ranking engine configs and for managing timeouts.

The current selection of configs and the order in which they are tried is a bit arbitrary, but should be enough to demonstrate the overall functionality. I haven't benchmarked it and might want to replace it completely.

Currently there is also no way to configure the autotune engine selection besides changing the values in SbyAutotuneConfig. This will need to change before merging this. I'm not sure what's the best place for such a configuration. Should it be part of the .sby file, a separate config file, just command line options?

jix commented 2 years ago

This is now essentially a complete first version