IODINE

Overview
IODINE is a technique to automatically extract invariants from hardware design simulations. The idea was motivated by the challenge of using formal verification in practice on large microprocessor designs at Sun Microsystems: no one person has the time or ability to write down all the properties to be checked, and manually written invariants are always subject to human blind spots and biases. IODINE proved that it can infer accurate and relevant invariants for hardware designs, including protocol diagrams and design structures such as FIFOs.
Papers
DAC-2005 IODINE paper, slides. Unfortunately, this paper did not have enough space to discuss all the work that we did and insights we obtained -- we should have written up a longer version elsewhere.
Collaborators
Naveen Chandra, Sridhar Narayanan, Sandeep Chakravorty
History
IODINE was originally inspired by my work on DIDUCE which inferred dynamic invariants from software programs. At Sun, we were struggling to use model checking tools in practice - even though we had access to all the leading commercial tools, including Real Intent, Zero-in (then an interesting new idea) and later Jasper Design and Synopsys Ketchum, we were unable to use them effectively because it was hard to get designers to write relevant design properties to be checked. It seemed obvious that we could use the extensive simulation testing we already did to automatically infer good properties. I was looking for something to do after the UltraJava (MAJC) processor project ended, so I sent a message to Bill Joy, Mike Splain and others, describing the idea and was gratified to get a reply from Bill saying he thought it was worth pursuing. Sunil Joshi and Shrenik Mehta sponsored the project in the new team called Global Validation that was just being born at the time. I started implementing IODINE in mid-2001 and after I moved to Bangalore in 2002, Naveen Chandra joined me and took over most of the implementation. Over time, we completed several analyzers and applied them to various projects (e.g. the memory controller of the dual core Gemini processor) and showed that we could extract useful and interesting properties. Moreover, we learned tricks to speed the analysis, remove irrelevant, coincidental or duplicate invariants, visualize a large number of invariants and figured out how to rank the important invariants above others.
Learnings
Our overall success on IODINE was limited by the mechanics of using the FV tools in practice on significant-sized designs. Most tools were designed to verify a small number of properties, and could not scalably handle the hundreds of automatically generated properties we were throwing at them. An even bigger problem in practice was that to use property checkers effectively, you need a robust set of input constraints to be created by the designer. In our case, we did not have designer written input constraints, and IODINE generated constraints were not good enough to be complete on their own. We therefore had to spend a good deal of time on dealing with false positives or understanding the input interfaces to create constraints ourselves. Thus designer involvement at least for writing constraints appears to be essential. Another factor that slowed us down was simply the logistics of dealing with hundreds of huge simulation dumps. Even though IODINE analysis was multi-threaded and we eventually tuned it to run overnight on 10-20 servers for reasonable-sized design blocks with a few hundred simulation traces, this took a lot of implementation work. To get to this level of performance, we had to switch to the FSDB interface (from the zipped VCD files we were using initially), which our intern Ajit Pasi implemented over the course of a summer.
Licensing
The IODINE software is proprietary to Sun Microsystems. For licensing opportunities, please contact Durgam.Vahia (at) sun.com.