Avoiding False Negatives in Formal Verification for Protocol-Driven Blocks
Görschwin Fey, Daniel J. Grosse, Rolf Drechsler · 2006
During bounded model checking (BMC) blocks of a design are often considered separately due to complexity issues. Because the environment of a block is not available for the proof invalid input sequences frequently lead to false negatives, i.e. counter-examples that can not occur in the complete design. Finding and understanding such false negatives is currently a time-consuming manual task. Here, we propose a method to automatically avoid false negatives which are caused by invalid input sequences for blocks connected by standard communication protocols