Blackbox

[AdamKeith1]

Is there a means to blackbox modules in sby?

[georgerennie]

Yes, using the Yosys blackbox command in the scripts section. e.g. the following yosys script blackboxes the module bb, so it just exists in top as a cell with the blackbox attribute set and contents ignored.

read_verilog <<EOT
module top(input a, output y);
bb b(.a(a), .y(y));
endmodule

module bb(input a, output y);
assign y = !a;
endmodule
EOT

blackbox bb
prep -top top -flatten
show

[AdamKeith1]

Do I actually need to include the SV in the [scripts] section or is that just for reference?

[georgerennie]

Oh thats just for reference. SBY is a wrapper around yosys, and the scripts section is just a set of yosys commands. You can see a list of available yosys commands by starting yosys (yosys on the command line) and running help.

I will also add that a lot of questions about language support etc are probably more likely to get responses if filed as issues on the main Yosys repo rather than SBY, as that is where the code for most stuff actually lies, however things relating to the actual SBY configuration files and formal engines are better placed here.

[AdamKeith1]

Do you know if this works for vhdl modules as well or just SV?

[georgerennie]

Yosys makes no distinction internally, a module could have come from either SV or VHDL or something else, it works with a somewhat generic netlist representation.