Extracting Assertions for Conflicts in HDL Descriptions

Data access conflicts may arise in hardware designs. One of the ways of detecting such conflicts is static analysis of hardware descriptions in HDL. We propose a static analysis-based approach to data conflicts extraction from HDL descriptions. This approach has been implemented in the Retrascope tool. The following types of conflicts are considered: simultaneous reads and writes, simultaneous writes, reading of uninitialized data, no reads between two writes. Conflict assertions are formulated as conditions on variables. HDL descriptions are automatically translated into formal models suitable for the nuXmv model checker. The translation process consists of the following steps: 1) preliminary processing; 2) Control Flow Graph (CFG) building; 3) CFG transformation into a Guarded Actions Decision Diagram (GADD); 4) GADD translation into a nuXmv format. Conflict assertions are automatically built using static analysis of the GADD model and passed to the nuXmv model checker.  Bounded model checking is used to check whether these assertions are satisfiable. If true, counterexamples are generated and then translated to HDL testbenches by the Retrascope tool. The proposed approach was applied to several open source HDL benchmarks like Texas-97, Verilog2SMV, VCEGAR and mips16 modules. Potential conflicts have been detected for all of these benchmarks. Future work includes propagation of conflict assertions to the interface level (thus getting assertions on modules’ communication protocols) and generation of built-in HDL checkers.

1. S.Tahar, R. Kumar. Formal Verification of Pipeline Conflicts in RISC Processors. In Proc. of the European Design Automation Conference (EURO-DAC), 1994, pp. 285-289.

2. M. Gordon,T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993, 492 p.

3. S. Hertz, D. Sheridan, S. Vasudevan. Mining Hardware Assertions with Guidance From Static Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 32, No. 6, 2013, pp. 952-965.

4. Cadence Incisive Formal Verifier. https://community.cadence.com//CSSharedFiles/forums/storage/22/10078/IncisiveFV_ds.pdf

5. A.V. Aho, R. Sethi, J.D. Ullman. Compilers: principles, techniques, and tools. Addison-Wesley, 1986, 796 p.

6. J. Brandt, M. Gemunde, K. Schneider, S. Shukla, J.-P. Talpin. Integrating system descriptions by clocked guarded actions. In Proc. of Forum on Specification and Design Languages (FDL), 2011, pp. 1-8.

7. R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, F.K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, vol. 13, issue 4, 1991, pp. 451-490.

8. A. Pnueli. The temporal logic of programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science, 1977, vol. 00, pp. 46-57.

9. nuXmv model checker. https://nuxmv.fbk.eu

10. Retrascope toolkit. https://forge.ispras.ru/projects/retrascope

11. Texas-97 Verification Benchmarks. https://ptolemy.berkeley.edu/projects/embedded/research/vis/texas-97

12. VCEGAR benchmark collection. https://www.cprover.org/hardware

13. Verilog2SMV tool. https://es-static.fbk.eu/tools/verilog2smv

14. Educational 16-bit MIPS Processor. https://opencores.org/projects/mips_16