Towards machine learning techniques for coverage-directed test generation
Constrained random verification (CRV) and formal verification are currently the state-of-the-art approaches to functional verification. CRV's advantage is that does not suffer from size restrictions. Hence it can be applied to large designs. However, CRV is inefficient, with many simulation cycles spent exploring the same state space. Furthermore, guiding the tools into interesting corner cases typically requires considerable manual effort from verification engineers. Conversely, formal verification can find corner cases with little manual steering; but due to complexity limits, it can only be applied exhaustively to relatively small designs. How can we take advantage of the benefits offered by both CRV and formal verification, while at the same time mitigating (or even eliminating) their drawbacks? Nyasha's research, conducted in collaboration with Infineon Technologies, aims to find concrete answers to this question.
As part of the "Trustworthy Robotic Assistants" project, preliminary research (link to: Intelligent Agent-Based Stimulation for Testing Robotic Software in Human-Robot Interactions; URL: https://arxiv.org/pdf/1604.05508.pdf) has been conducted to determine the feasibility of using intelligent agents as models for test generation in robotic systems verification. Using a case study from the human-robot interaction (HRI) domain, Belief-Desire-Intention (BDI) agents were found to provide the level of agency and causality inherent in the real world, leading to a smart testing environment. Reinforcement learning (RL), a semi-supervised machine learning technique, was introduced to automate exploration of the BDI model using a reward function based on feedback regarding how much of the design/specification had been covered during a specific test cycle. The research concluded that RL could be used to automate test generation, although implementation of such a coverage-directed test generation system in an industrial setting is difficult and requires significant engineering expertise.
Nyasha's research is taking this concept even further by employing advanced machine learning techniques, to investigate the middle ground between CRV and formal verification. An RL based approach, with its reward/punishment system, offers high-level, goal-directed planning to achieve set goals whilst facilitating intelligent, agent-based generation of test stimuli which can automatically find and hit the interesting corner cases on a highly complex design, such as a CPU. This results in less reliance on hand-written constraints and random test generation. Effectively, verification engineers would have access to a verification model that is efficient (less repetitive simulation), effective (high coverage quickly reached) and requires less manual labour. The solution could also be applicable to other verification use-cases such as post-silicon debug and test case automation at cluster level.