[feature request] sby writes its output to a main log file

[tudortimi]

It would be helpful if sby would write its output to an sby.log file.

[ZipCPU]

SBY does create a log file every time you run it, several in fact. The primary log file is in the created task directory and named logfile.txt. There's also a log file in each engine_? directory for each proof that the solver runs for that given task. You'll also find a log file describing the processing of your design in the task directory /model/design*.log.

Dan

[tudortimi]

But if I'm running multiple tasks, using sby <file> it would be useful to get an overview of all tasks that were run, etc. With a lot of tasks it can get pretty crowded.

[tudortimi]

Plus, even for one task, it's easier to open one log file from a standard location, look at it, leave the editor open, run the next task, refresh the contents of the log file in the open editor, etc,

[ZipCPU]

I typically use "make" to handle directories with multiple sby tasks in them. You can find an example Makefile here. make -n then gives me a beautiful view of what's not yet passed, and make -kj4 will run all outstanding proofs on 4 CPU cores. I also have a passcheck.sh that I use to see if anything has failed. I can then examine that to if anything has failed. There's also an sby-gui command you can use to get a GUI view of (mostly) the same thing.