Abstract: In the agile hardware design methodology, a domain specific hardware description language is often used for RTL modeling. This novel situation brings new challenges for design verification. In order to support design verification techniques such as (bounded) model checking and equivalence checking, a symbolic simulator is designed and implemented for PyRTL and its intermediate representations. This paper introduces the design principle, conversion rules and other key technologies of our symbol simulator. The experimental results show the correctness of the implemented symbol simulator.

Key words: symbolic simulator, PyRTL, agile hardware design, verification