MDG-Based Verification of the Look-Aside Interface
Dong-Lin Li, Otmane Aı̈t Mohamed · 2006
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 LMDG. An MDG model was also built in MDG-HDL language, a Prolog-style hardware description language, from the RTL model. Finally LMDGproperties 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