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 studyCustom instruction specificationAbstract domain checkSoftware analysis rules check
Saturating additionSourceCheck #1Check #2
Conditional setSourceCheck #1Check #2
Parallel decrementSourceCheck #1Check #2