Accompanying material for iFM publication
This site contains a collection of all the Verilog code from our case studies for our following publication:
Marie-Christine Jakobs, Marco Platzner, Heike Wehrheim, and Tobias Wiersema. Integrating Software and Hardware Verification. In Proceedings of the 11th International Conference on Integrated Formal Methods (iFM). Springer, LNCS, pp. 307-322. Bertinoro, Italy, September 2014.
The following table contains links to the source code of the custom instruction and of the second two approaches for integrating software and hardware verification. For the first approach does not involve an intermediate Verilog representation and is thus not listed. All sources contain the 32bit version of the circuits.
| Case study | Custom instruction specification | Abstract domain check | Software analysis rules check |
|---|---|---|---|
| Saturating addition | Source | Check #1 | Check #2 |
| Conditional set | Source | Check #1 | Check #2 |
| Parallel decrement | Source | Check #1 | Check #2 |