Abstract: Approximate Circuits are circuits that can tolerate known errors. The error tolerance is a tradeoff for achieving low power consumption, low area and increased speed of circuits. This unique quality of approximate circuits makes a huge impact on circuit design and is highly in demand in sectors like image processing, signal processing, etc. Due to this, performing verification for these circuits has become an essential part. However, formal verification techniques like formal error metrics, Mean Squared Error (MSE), Mean Absolute Error (MAE), and Maximum Error (MXE) cannot be used to prove 100% accuracy of approximate circuits due to error tolerant nature. Thus, in this work, we propose a formal verification methodology to generate a 100% verification assurance of these approximate techniques and reduce the verification time by 0.01 sec. Approximated Ripple Carry Adder (RCA) has been used as a case study and has performed verification for (28)2 input patterns and has proved for all input patterns that the approximate circuit stands true for the desired functional specifications. A Formal Verification technique called Bounded Model Checking (BMC) is used to perform the verification using Symbiyosys formal verification tool.

Keywords: Formal Verification, Approximate Circuits, Bounded Model Checking, Functional Specifications, Mean Squared Error, Mean Absolute Error

Pages: 25-34