A complete approach to unreachable state diagnosability via property directed reachability

— In modern hardware design, substantial manual effort is required to fix a design when verification discovers a state unreachable. This paper addresses this growing pain where given an unreachable target state, a methodology is presented to return all design locations where a change can be implemented to make the target state reachable. In contrast to previous state reachability rectification techniques that use bounded model checking, our approach addresses the issue using unbounded model checking. It first enhances the circuit transition relation by inserting a novel error model construction at each suspect location. An unbounded model checking algorithm is then applied to the enhanced transition relation to find which of the suspect locations can be changed to make the target state reachable. The use of unbounded model checking allows it to identify the complete problem solution set. As an added benefit, it also returns a proof that no further solution(s) exist in the form ...

• Type: Journal
• Year: 2016
• Where: ASPDAC
• Authors: Ryan Berryhill, Andreas G. Veneris
• Keywords: ASPDAC 2016, Hardware