Avoiding False Negatives in Formal Verification for Protocol-Driven Blocks

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