Incremental Verification Techniques for an Updated Architectural Specification

This paper explores the utility of making use of previously proved component properties and available simulation traces at the component and system level of a composite design for proving a newly added architectural property of the design. We present two techniques of reusing these prior verification results for proving or disproving the architectural property without doing full-scale formal verification of it on the total design from scratch, which runs into capacity issues, or running the already run simulations once again with this new property as an assertion, which is extremely time-consuming and leads to significant wastage of validation effort. We have experimented with our proposed approach on AMBA AHB example and have obtained encouraging results.