Skip to content

Invariant Violation Report #290

Closed
Closed
@Rico1900

Description

@Rico1900

I tried to verify a simple design in vcegar-benchmarks, but I encountered the following error message.

hw-cbmc version: main-lastest
Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

endmodule

ebmc command:

ebmc example.v --top main --bound 10 -p "a < 200"

error messag:

Parsing example.v
Converting
Type-checking Verilog::main
file example.v line 9: implicit wire main.clock
--- begin invariant violation report ---
Invariant check failed
File: ../../lib/cbmc/src/util/message.h:188 function: get_message_handler
Condition: message_handler!=nullptr
Reason: message handler should be set before calling get_message_handler
Backtrace:
0   ebmc                                0x000000010e3fcfea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   ebmc                                0x000000010e3fd587 _Z13get_backtracev + 183
2   ebmc                                0x000000010e4b19fc _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   ebmc                                0x000000010e4b19c9 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   ebmc                                0x000000010e648643 _ZN8messaget19get_message_handlerEv + 115
5   ebmc                                0x000000010e5f5f5f _ZN17verilog_languaget7to_exprERKNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEES8_R5exprtRK10namespacet + 175
6   ebmc                                0x000000010e659c28 _ZN16ebmc_propertiest17from_command_lineERK8cmdlinetRK18transition_systemtR16message_handlert + 200
7   ebmc                                0x000000010e654eab _ZN10ebmc_baset14get_propertiesEv + 59
8   ebmc                                0x000000010e657f81 _ZN19ebmc_parse_optionst4doitEv + 3105
9   ebmc                                0x000000010e42891c _ZN19parse_options_baset4mainEv + 140
10  ebmc                                0x000000010e65ead8 main + 40
11  dyld                                0x00007ff81ca2a41f start + 1903


--- end invariant violation report ---
[1]    7888 abort      ebmc example.v --top main --bound 10 -p "a < 200"

However, if I write the property that needs to be verified directly in the Verilog file, it just works.
Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

always begin
assert property: (a<200);
end

endmodule

ebmc command:

ebmc example.v --top main --bound 20

Is this expected behavior? And do I misunderstand how to use ebmc?

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions