Formal Verification - Equivalence Checking (Part2)

This video is Part6 of the Key Learnings from Chip Development series, which is on Formal Verification, particularly on equivalence checking.
FV Equivalence checking of Combinatorial circuit analyzing methods, such as Truth Tables, Binary decision diagram, Combinational circuit Satisfiability and Tseitin transformation are covered in this video.
Boolean satisfiability problem (SAT), for a given Boolean formula, checks whether it is satisfiable or not. SAT solvers have emerged as powerful tools for tackling combinational problems in various domains
The Tseitin transformation, takes the combinatorial logic circuit as input and uses it on Boolean expression and performs De Morgan's law and the distributive property , to convert it into an equisatisfiable boolean formula.