Simulation and formal verification are the two most commonly used techniques for verifying a digital design described at the Register-Transfer Level (RTL). Compared to simulation, formal verification shows an advantage in terms of exhaustive design coverage. However, due to state-space explosion, it is limited in size of designs that can be analyzed, and this capacity problem remains a big issue for application in large designs, such as processors.

In this thesis, a waypoint-based semiformal verification (SFV) method is proposed in order to extend formal tool capacity for large designs. Our algorithm involves formal engines to explore traces to hit waypoints, reducing the computation time and memory required to reach a desired state. In addition, an automatic waypoint generation tool is developed. Criteria are developed to identify important flip-flops in the design to generate the waypoints, based on information from the synthesized netlist. A neural network is trained to score all the flip-flops in the target design. Based on the predicted scores, we set a threashold to select the critical flip-flops and then generate waypoint guides for RTL verification.

The process is first studied using a small FIFO example. Then an expandable end-to-end ISA verification framework designed around a RISC-V core is evaluated with the proposed SFV techniques. The results show that waypoint-based SFV and the automatic waypoint generation algorithm have great potential in RTL verification. SFV can save a substantial amount of the time and memory required to cover all important scenarios, compared to direct application of FV.