2. Formality是由Synopsys公司开发的一种形式验证(Formal Verification)工具，用于两个Design之间的等价性验证。它可以支持如下哪些等价性验证?

Synopsys Formality 支持多种等价性验证场景，主要包括：RTL 级代码之间的等价性验证（RTL vs RTL）、RTL 与门级网表之间的等价性验证（RTL vs Gate）、门级网表之间的等价性验证（Gate vs Gate），以及带扫描链（scan chain）的设计之间的等价性验证。此外，Formality 还能处理综合前后、版图前后（如 LVS 前的网表比对）的验证，支持对组合逻辑和时序逻辑的等价性检查。常见的错误选项可能包括仅支持单一比较对象或仅支持同步电路，实际上 Formality 通过将设计转换为内部标准格式并利用布尔可满足性（SAT）引擎，验证任意两个设计在功能上是否等价。