星用数据总线是卫星电子系统各部件之间传输数据的枢纽。CAN总线作为星用数据总线的一种,在我国卫星中已得到广泛应用。本文以航天需求为背景,研究抗辐射加固的CAN IP核设计。本文根据地面模拟实验结果和空间轨道上重离子和质子分布,预估了轨道上半导体器件的单粒子翻转率。这对正确选用半导体器件,提高可靠性和寿命意义重大,且对半导体器件的抗单粒子效应能力有参考价值和指导作用。通过深入分析CAN总线协议和某公司的CAN IP核,针对航天应用的特殊要求设计了一款功能满足实际应用需要的加固CAN IP核。该IP核既可单独应用,又可以通过APB总线集成到SoC内应用。针对空间环境的单粒子翻转问题,本文采用TMR、EDAC等技术对CAN IP核内部的寄存器、存储器及有限状态机等SEU敏感单元进行了相应的加固设计,同时采用故障注入技术对加固设计的有效性进行了检验。在验证方面,本文在EDA环境下,采用SystemVerilog Assertion语言作指导,结合形式化验证工具Magellan,对加固后的CAN总线IP核进行基于断言的混合形式化验证,来保证其功能的正确性和验证的高效性。通过该验证方法对其进行的功能验证,功能覆盖率和代码覆盖率均达到96%以上。与传统的仿真方法相比,改进后的形式验证方法对功能属性的证明更加完整,且高效的断言机制可以从海量测试用例的编写中解放出来,有效缩短设计验证周期,且提高了航天电子设计的可靠性。