admin管理员组

文章数量:1125913

I was looking into set_max_trace_length:

According to the reference manual:

Use the set_max_trace_length command to specify the maximum length for traces in the JasperGold Apps Visualize window and the limit for the proof or visualization depth. When max_trace_length is set, if one engine reaches the length limit for some property, all other engines will stop working on that property. Note: You can also use this command to specify a bounded proof, that is, a proof that terminates after reaching the specified maximum length. Use the get_max_trace_length command to display the value specified with the companion set command.

Which I interpreted as bounding JasperGold to a number of clock cycles. But in some cases this seems to be preventing the tool from finding counterexamples within the specified clock cycle range.

I do not understand exactly what this option is doing any clarification would be very helpful.

I ran JasperGold with set_max_trace_length 16 and it was not able to find a counterexample in the first 16 clock cycles. Then, I ran it without that option and it found a counterexample within the first 16 clock cycles.

本文标签：

版权声明：本文标题：system verilog - Is there a JasperGold FPV option to bound a proof to a specific number of clock cycles? - Stack Overflow 内容由网友自发贡献，该文观点仅代表作者本人， 转载请联系作者并注明出处：http://www.betaflare.com/web/1736623116a1945616.html， 本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌抄袭侵权/违法违规的内容，一经查实，本站将立刻删除。