Since this example uses large memories, the This engine uses the array-theories provided by those solvers toĮfficiently model memories. This project uses the smtbmc engine, which uses SMT solvers to perform the This example is expected to fail verification (see the BUG comment). rdata ( rdata ) ) ( * anyconst * ) reg test_addr reg test_data_valid = 0 reg test_data always posedge clk ) begin if ( addr = test_addr ) begin if ( wen ) begin test_data <= wdata test_data_valid <= 1 end if ( test_data_valid ) begin assert ( test_data = rdata ) end end end endmodule module memory ( input clk, wen, input addr, input wdata, output rdata ) reg bank0 reg bank1 reg bank2 reg bank3 wire mem_sel = addr wire mem_addr = addr always posedge clk ) begin case ( mem_sel ) 0 : if ( wen ) bank0 <= wdata 1 : if ( wen ) bank1 <= wdata 2 : if ( wen ) bank1 <= wdata // BUG: Should assign to bank2 3 : if ( wen ) bank3 <= wdata endcase end assign rdata = mem_sel = 0 ? bank0 : mem_sel = 1 ? bank1 : mem_sel = 2 ? bank2 : mem_sel = 3 ? bank3 : 'bx endmodule Module testbench ( input clk, wen, input addr, input wdata, output rdata ) memory uut (. (Trial and error canĪlso be a useful method for evaluating engines.) The documentation for the individualĮngines can provide some guidance for engine selection. Select the right engine for each project. Returned by the first engine to finish is the result returned by SymbiYosys.)Įach engine has its strengths and weaknesses. (When multipleĮngines are selected, all engines are executed in parallel and the result sby file for a project selects one or more engines. Is an open source VCD viewer that you can use.) Selecting the right engine ¶ The modified design and see if the proof now fails. Time for a simple exercise: Modify the design so that the property is falseĪnd the offending state is reachable within 100 cycles. Without -f the command willįail because the output directory demo/ already exists.) (Use sby -f demo.sby to re-run the proof. Such as a copy of the design source, various log files, and trace data in case This will also create a demo/ directory tree with all relevant information, SBY summary: engine_0 (smtbmc) returned PASS SBY summary: Elapsed process time : 0:00:00 (0) SBY summary: Elapsed clock time : 0:00:00 (0) SBY engine_0: Status returned by engine: PASS SBY engine_0: # 0 0:00:00 Checking asserts in step 99. SBY engine_0: # 0 0:00:00 Checking asserts in step 98. SBY engine_0: # 0 0:00:00 Checking asserts in step 97. SBY engine_0: # 0 0:00:00 Checking asserts in step 96.
0 kommentar(er)
