FPGA状态机综合可靠性探究 ①

2021-04-09丁宗杰门永平白正尧

空间电子技术 2021年1期

丁宗杰，门永平，白正尧，陈锐

(中国空间技术研究院西安分院，西安 710000)

0 引言

FPGA研制过程一般需进行设计输入、设计综合、实现与布局布线、芯片编程等几个阶段。设计输入是将所设计的系统或电路以开发软件要求的某种形式表示出来，并输入给EDA工具的过程，常用的方法有硬件描述语言(HDL)和原理图输入方式等。设计综合是将设计输入编译成基本逻辑单元组成的逻辑连接网表。针对状态机，综合器提供了一个名为安全实现的综合属性，综合器根据该属性设置的不同对设计输入的状态机完成不同的网表转化，从而使综合后的逻辑网表表现出不同的功能。本文结合常用的XILINX公司的ISE集成开发环境和ACTEL公司的LIBERO集成开发环境对FPGA状态机安全实现综合属性的作用与应用进行分析与探究，同时通过等价性验证的方式分析状态机安全实现设置对网表转化的影响。

1 状态机安全实现设置

ISE集成开发环境下的XST综合器和LIBERO集成开发环境下的Synplify综合器可进行FPGA状态机的安全实现。状态机的安全实现是通过综合器增加的逻辑电路使状态机从一个非法状态恢复到特定状态，当状态机运行进入一个无效状态时，通过综合器增加的逻辑，可以使状态机恢复到一个已知态，我们一般将该状态称之为恢复态。该功能被称为状态机安全实现。

使用XST综合器应用状态机安全实现可以通过设置综合选项方式和应用safe_implimentation约束的方式。综合选项设置方式是打开XST综合选项面板，在HDL Options选项中设置-safe_implementation参数，该参数默认值为“NO”，即不进行状态机安全属性设置，当将该参数设置为YES时，则XST进行状态机安全实现综合。安全属性设置如图1所示。

图1 XST综合选项安全属性设置

使用safe_implimentation约束的方法是在代码中使用attribute safe_implementation语句来进行状态机安全属性设置。

XST对状态机进行安全属性设置，其恢复态默认为复位时的状态，也可以通过safe_recovery_state参数将恢复态指定为特定的状态。

以下是一个状态机的定义示例，使用safe_implementation设置了状态机安全实现的综合属性，使用safe_recovery_state将恢复态指定为s1状态。

typestate_type is (s1,s2,s3,s4,s5);

signal state,next_state: state_type ;

attributefsm_encoding : string;

attributefsm_encoding of state,next_state : signal is "sequential";

attributesafe_implementation : string;

attributesafe_implementation of state,next_state: signal is "yes";

attributesafe_recovery_state : string;

attributesafe_recovery_state of state,next_state : signal is "s1";

状态机综合后的编码结果、安全实现结果等信息均可从综合报告中进行查阅。

在使用Synplify综合器对ACTEL公司FPGA进行设计时，可以在Synplify中建立sdc约束文件，在sdc文件中的attributes面板中进行状态机的安全属性设置。也可在代码中通过增加attribute syn_encoding进行设置。

2 状态机安全实现分析

将上述定义的状态机设计成为s1至s5循环运转的状态机，作为设计输入进行差异化分析。

对于XILINX公司FPGA开发，建立ISE工程，使用XST进行综合，状态机不设置安全属性，综合编码结果如表1所示。

表1 状态机编码映射表

状态s1至状态s5分别对应000至100。其综合后电路如图2所示，state[1]至state[3]分别对应FFD1至FFD3寄存器：

各LUT查找表中运算多项式如下所示：

FFD1=FFD3 * FFD2

FFD2= (!FFD3*FFD2 )+(FFD3*!FFD2)

FFD3= (!FFD3*FFD2)+(!FFD3*!FFD1)

状态机state[1:3]运行方式为：000→001→010→011→100→000→001……，综合后状态机运行方式与设计输入相同。

图2 XILINX厂商FPGA未设置安全属性的状态机电路图

当状态机出现101,110,111的无效状态时，状态机的运行方式为101→010,110→011,111→100，从这个例子可以看到该状态机恢复到了一个有效状态，但不可控不确定。

对于这同一编码，当状态机设置安全属性，其综合报告提示状态机设置了恢复态Recovery State为s1，即三级寄存器应为000。

综合结果如图3所示：

图3 XILINX厂商FPGA设置安全属性的状态机电路图

增加安全属性综合后，电路相对于之前寄存器位置和查找表发生了一定的变化，其状态机运算多项式如下：

FFD1=FFD3*FFD2*!FFD1

FFD2=(!FFD1*!FFD2*FFD3)+(!FFD1*FFD2*!FFD3)

FFD3=!FFD3*!FFD1

其工作方式仍为000→001→010→011→100→000→001……，当状态机出现101,110,111的无效状态时，状态机的运行方式为101→000,110→000,111→000，与综合报告恢复态数据一致。

对于ACTEL公司FPGA开发，建立Libero工程，使用synplify进行综合，状态机不设置安全属性，状态机综合编码方式与上述XILINX公司FPGA设计保持一致，综合结果如图4所示：

图4 ACTEL厂商FPGA未设置安全属性的状态机电路图

由图4可见，状态机的运算多项式如下：

state[0]= !state[2]*!state[0]

state[1]= state[0]^ state[1]

state[2]= state[1]* state[0]

状态机state[2]state[1]state[0]运行方式为：000→001→010→011→100→000→001……

当状态机出现101,110,111的无效状态时，状态机的运行方式为101→010,110→010,111→100，从这个例子可以看到该状态机恢复到了一个有效状态，但不可控不确定。

对于这同一编码，当状态机设置安全属性，综合结果如图5所示：

图5 ACTEL厂商FPGA设置安全属性的状态机电路图

增加状态机安全属性后，综合的电路和未增加安全属性的电路发生了一定的变化。电路A部分仍然是三级寄存器组成的状态机，其工作方式仍为000→001→010→011→100→000→001……，电路B和电路C则是额外增加部分。电路B部分的组合逻辑，将状态机的有效状态和无效状态做了区分，分别输出逻辑0和逻辑1。电路B的输出经过电路C的两级寄存器state_illegalpipe1和state_illegalpipe2采样后与外部复位共同作用在状态机的异步复位/置位端。该电路中一旦状态机出现无效状态，则会通过电路B和电路C向状态机发送一个复位信号，对状态机进行自复位。

3 状态机安全实现设置对逻辑等价性验证的影响

FPGA设计从设计输入到最终的烧录程序要经过综合、实现、布局布线等多个环节的网表转化，为了验证各环节转化的网表功能相同，在FPGA验证中会使用逻辑等价性的验证方法。

逻辑等价性验证工具采用数学方法直接比对各阶段网表的一致性，其基本思想是，对于做比对的两个网表如果对于所有可能的输入其输出也一致，则证明输入输出间的组合逻辑正确，即网表一致。逻辑等价性工具一般按以下步骤执行验证。

第一步：读取网表。将待比对的两个网表分别定义为golden(经验证的)和revised(待修订的)网表，由等价性验证工具读取。根据golden网表来核对其它设计网表(综合后网表，布局布线后网表)。设计流程中任何阶段生成的网表都可以用作golden网表，如综合前网表、布局布线后网表。设计输入的网表是最常被采用的golden网表。

第二步：设置关键点。遵循等价性验证的基本思想，验证工具把网表划分成许多基本的小段，称为“逻辑锥”。如果所有的逻辑锥等价，则整个网表等价。逻辑锥的输入输出就是关键点。关键点主要由网表的基本输入输出、触发器、寄存器、黑盒子等元素构成。

第三步：映射关键点。等价性验证工具会根据名称或功能将两个网表对应的关键点进行关联，从而划分出相应的组合逻辑。

第四步：比对。验证工具按照数学方法给逻辑锥输入激励，比对输出，从而验证逻辑锥的等价性。如果所有逻辑锥都等价，则两个网表等效。否则调试非匹配点，确认问题，修改设计，再次进行比对。

安全属性使综合器对设计增加了额外恢复电路，从其含义及设置前后的电路来看综合后网表与设计输入的网表不应等价。这里使用的逻辑等价性工具对图5的设计输入与综合后网表进行验证，可以看到综合后网表多出两个无法映射的关键点，见图6的state_illegalpipe1和state_illegalpipe2，这两个关键点对应图5的电路C部分。

图6 关键点映射图

对比golden和revised电路图时可以看到，综合前状态机的复位只由外部复位reset决定。而综合后同一寄存器的复位由外部复位reset和内部寄存器state_illegalpipe1、state_illegalpipe2输出信号共同决定，综合前后的网表已不等价。在将state_illegalpipe1或state_illegalpipe2绑定为不使状态机复位的常量后，综合前后的网表逻辑等价。