形式验证可以判断

正确答案：A、D。形式验证（Formal Verification）是一种基于数学推理的验证方法，主要包括等价性检查（Equivalence Checking）和属性检查（Property Checking / Model Checking）。等价性检查可以比较两个设计（如RTL与门级网表、不同抽象层次模型）在功能上是否完全等价，因此A选项正确。属性检查通过断言（Assertion）或形式化规约（如SVA、LTL）来证明设计是否满足特定功能属性，从而验证设计功能是否正确，因此D选项正确。时序分析（如建立时间、保持时间检查）通常由静态时序分析（STA）完成，不属于形式验证的典型范畴，故B选项错误。C选项“其他均不能保证”显然错误，因为A和D均可由形式验证保证。易错点：有些考生认为形式验证只能做功能验证而忽略等价性检查，或者混淆了时序验证与形式验证的边界。注意：形式验证中也有对时序属性（如延迟）的形式化分析，但工业界狭义的形式验证通常不涵盖STA，STA属于独立的方法学。因此本题应选择A和D。