Industrial Strength Formal Using Abstractions
Authors:
Ashish Darbari,
Iain Singleton
Abstract:
Verification of concurrent systems with thousands of multiple threads and transactions is a challenging problem not just for simulation or emulation but also for formal. To get designs to work correctly and provide optimal PPA the designers often use complex optimizations requiring sharing of multiple resources amongst active threads and transactions using FIFOs, stallers, pipelining, out-of-order…
▽ More
Verification of concurrent systems with thousands of multiple threads and transactions is a challenging problem not just for simulation or emulation but also for formal. To get designs to work correctly and provide optimal PPA the designers often use complex optimizations requiring sharing of multiple resources amongst active threads and transactions using FIFOs, stallers, pipelining, out-of-order scheduling, and complex layered arbitration. This is true of most non-trivial designs irrespective of a specific application domain such as CPU, GPU or communication. At the outset a lot of these application domains look diverse and complex; however at some level of detail all of these employ common design principles of sequencing, load balancing, arbitration and hazard prevention. We present in this paper a key abstraction based methodology for verifying ordering correctness and arbitration across a range of designs which are derived from different application domains. We show how by using abstractions and supporting them with invariants one can not only find deep corner case bugs in sequentially very deep designs; we can also build exhaustive proofs to prove the absence of critical bugs such as deadlock, starvation, and loss of data integrity. We present experimental results on a range of different designs and show that on some of the designs such as FIFOs we can verify over 100 different types of FIFOs for ordering correctness using a single assertion in a single testbench. We also show how the methodology of FIFO verification can be adapted to verify over half-a-dozen different types of arbiters including a very complex memory subsystem arbiter. We verify a multi-clocked synchronizer and a packet based design from a networking domain using the same abstraction as used in FIFO verification. The results demonstrate the strength of our methodology which is both reusable and compact.
△ Less
Submitted 30 April, 2017; v1 submitted 7 June, 2016;
originally announced June 2016.
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
Authors:
Ashish Darbari,
Iain Singleton,
Michael Butler,
John Colley
Abstract:
The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we presen…
▽ More
The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we present a formal model of HSA which can be used in the development and verification of both concurrent software applications as well as in the development and verification of the HSA-compliant platform itself. We use the Event-B language to build a provably correct hierarchy of models from the most abstract to a detailed refinement of HSA close to implementation level. Our memory models are general in that they represent an arbitrary number of masters, programs and instruction interleavings. We reason about such general models using refinements. Using Rodin tool we are able to model and verify an entire hierarchy of models using proofs to establish that each refinement is correct. We define an automated validation method that allows us to test baseline compliance of the model against a suite of published HSA litmus tests. Once we complete model validation we develop a coverage driven method to extract a richer set of tests from the Event-B model and a user specified coverage model. These tests are used for extensive regression testing of hardware and software systems. Our method of refinement based formal modelling, baseline compliance testing of the model and coverage driven test extraction using the single language of Event-B is a new way to address a key challenge facing the design and verification of multi-core systems.
△ Less
Submitted 16 May, 2016;
originally announced May 2016.
