Multi-core processors and Systems-on-Chips are composed of a large number of processing and memory elements interconnected by complex communication fabrics. These fabrics are large systems made of many queues and distributed control logic. Recent studies have demonstrated that high levels models of these networks are either tractable for verification or can provide key invariants to improve hardware model checkers. Formally verifying Register Transfer Level (RTL) designs of these networks is an important challenge, yet still open. This paper bridges the gap between high level models and RTL designs. We propose an algorithm that from a Verilog description automatically produces its corresponding micro-architectural model. We prove that the extracted model is transfer equivalent to the original RTL circuit. We illustrate our approach on a typical example of communication fabrics: a scoreboard with credit-flow control.
Associated Source Code here
To get our implementation of the method described in our paper, we recommend installing the Haskell platform. You should be able to compile from the command line by typing: ghc --make eMOD. To run it, specify the input file with -i, and the output files with -p and -g. We have used Haskell version 7.6.3, and also tried 7.8.2. The latter gave the warning that one of the files will stop working in ghc 7.10 (not released yet). Drop me a line if you are using 7.10 or newer and would like me to fix this (s.j.c.joosten at tue.nl).