MDG-Based Verification of the Look-Aside Interface

In this paper a formal verification of the look-aside interface using MDG-based model checking technique is presented. MDGs (multiway decision graphs) are an extension of BDD-like data structures with a distinction of concrete sorts and abstract sorts. The look-aside interface is a memory-mapped interface, targeted at devices that offload certain tasks from a network processing unit. A synthesizable RTL model in Verilog has been developed from the standard specification of the look-aside interface with the design properties specified in a CTL-like specification language called L_MDG. An MDG model was also built in MDG-HDL language, a Prolog-style hardware description language, from the RTL model. Finally L_MDG properties were checked against the MDG-HDL model in the MDG model checker. Through our experiments, we showed a practical example of a full formal verification using MDGs