'proc' command

[AdamKeith1]

Error: SBY 16:20:19 [counter] prep: Warning: Ignoring module counter because it contains processes (run 'proc' command first). SBY 16:20:19 [counter] prep: ERROR: The 'setundef' command can't operate in -undriven mode on modules with processes. Run 'proc' first. SBY 16:20:19 [counter] prep: finished (returncode=1) SBY 16:20:19 [counter] prep: task failed. ERROR.

Src: module counter #(parameter NUM_BITS = 16) ( input clk, output reg [(NUM_BITS-1):0] counter ); initial counter = 0;

always @(posedge clk) begin if (counter == ((2**NUM_BITS)-1)) counter <= 0; else counter <= counter + 1; end

ifdef FORMAL always @(posedge clk) begin cover (counter == (2**NUM_BITS) - 1); // assert (counter < 2**NUM_BITS); end endif

endmodule

Sby: [options] mode cover

[engines] smtbmc bootlector

[script] read -formal counter.sv prep -top counter hierarchy -check -top counter -chparam NUM_BITS 200

[files] counter.sv

[georgerennie]

prep -top counter implicitly calls hierarchy -check -top counter as the first thing it does. prep will run on the module with particular parameter values. Calling hierarchy separately afterwards causes a new version of the top module to be created with the different parameter, but the rest of what prep does isn't done.

You can fix this by reordering the commands like so

hierarchy -check -top counter -chparam NUM_BITS 200
prep -top counter

Note also that you have typoed the engine name in [engines], it should be boolector instead of bootlector

[AdamKeith1]

Thank you so much