Syntactic and Semantic Analysis of Temporal Assertions to Support the Approximation of RTL Designs

Approximate Computing (AxC) aims at optimizing the hardware resources in terms of area and power consumption at the cost of a reasonable degradation in computation accuracy. Several design exploration approaches and metrics have been proposed so far to identify the approximation targets, but only a few of them exploit information derived from assertion-based verification (ABV). In this paper we propose an ABV methodology to guide the AxC design exploration of RTL descriptions; we consider two main approximation techniques: bit-width and statement reduction. Assertions are automatically mined from the simulation traces of the original design to capture the golden behaviours. Then, we consider the syntactic and semantic aspects of the assertions to rank the approximation targets. The proposed methodology generates a list of statements sorted by their increasing impact on altering the functional correctness of the original design, when selected to be approximated. Through experiments on a case study, we show that the proposed approach represents a promising solution toward the automation of AxC design exploration at RTL.