主要职责：
1. 制定形式化验证策略：针对复杂的数字设计模块（如CPU核、GPU、互连、内存控制器、一致性协议、安全模块等），制定全面的形式化验证计划和策略。
2. 属性规范与开发：理解设计规范和微架构，编写高质量、精确的形式化属性（Assertions）。
3. 形式化验证环境搭建与执行：** 配置、设置并运行业界主流的形式化验证工具（如 Cadence JasperGold, Synopsys VC Formal, Siemens Questa Formal 等）。
4. 调试与根本原因分析：** 分析形式化工具报告的失败（Failures）和反例（Counterexamples, CEX），与设计工程师紧密合作，定位并解决设计中的逻辑错误。
5. 等价性检查：执行顺序逻辑等价性检查（Sequential Equivalence Checking, SEC），确保RTL修改或综合过程中的逻辑一致性。
6. 覆盖率分析与收敛：定义和分析形式化验证覆盖率，确保属性充分覆盖设计意图，并推动验证收敛。
7. 方法学开发与改进：探索、评估并引入新的形式化验证技术和方法学，优化现有流程，提高验证效率和质量。
8. 协作与沟通： 与设计团队、仿真验证团队、架构师等紧密合作，确保验证目标的一致性。
9. 知识分享与指导：（可选，若为资深职位）指导团队内其他工程师，分享形式化验证的最佳实践。
任职要求：
1. 学历背景： 电子工程、计算机科学、微电子或相关专业的硕士或博士学位（特别优秀的本科学历也可考虑）。
2. 经验要求：
- 拥有 5年的芯片（ASIC/SoC/FPGA）形式化验证相关工作经验。
- 必须具有丰富的形式化验证项目实战经验，而非仅仅了解概念或短期使用。
3. 专业技能：
- 深刻理解形式化验证的基本原理（如模型检查 Model Checking、定理证明 Theorem Proving、等价性检查 Equivalence Checking）。
- 精通至少一种主流形式化验证工具（JasperGold, VC Formal, Questa Formal 等），并具备深入的调试技巧。
- 精通属性规范语言，特别是 SystemVerilog Assertions (SVA)。
- 深入理解数字逻辑设计原理、计算机体系结构。
- 熟练掌握硬件描述语言（Verilog / SystemVerilog / VHDL）。
- 熟练使用脚本语言（如 Python, Perl, Tcl）进行环境搭建和流程自动化。
4. 软技能：
- 优秀的分析问题和解决问题的能力。
- 良好的沟通能力和团队合作精神。
- 积极主动，具备较强的学习能力和探索精神。