Designers who use hardware description language (HDL) tools for automated synthesis, those involved with HDL language research, and those interested in design verification will find this paper interesting. The authors apply the well-known mathematical concept of program slicing to HDL verification at the register transfer level (RTL) of design. In addition, their approach has potential benefits for efficient automated synthesis at the RTL level.

Casual readers should be able to understand the basic ideas and concepts without involving themselves in the complex formal development. Verilog experience is needed to understand the details of the examples, and advanced capability with discrete mathematical structures is needed to understand the formal theoretical development. Readers unfamiliar with program slicing concepts will find it necessary to do some background reading, as the formal development is abbreviated, sometimes ambiguous, and contains typographical errors at critical points. The programming concept of “variable” is indiscriminately mixed with the HDL concept of “signal” in ways that are confusing.

I found the paper interesting, and recommend it to both applied and theoretical computer scientists. Experimental results performed on medium-sized designs show that slices generated by the authors’ tools match the specifications exactly. I would like to have seen some efficiency comparisons with other tools.