企业官网建设流程全解析

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482

目录

默认情况

set_parameter命令

consensus

blackbox

and

or

set_net_resolution命令

Formality：匹配(match)是如何进行的？一文中谈到，多驱动线网会被Formality识别为被识别为BBNet（某些情况下不会），并成为一个新的比较点，本文将详细讨论关于多驱动线网的处理细节。

Formality在验证过程中会确保每一条具有多个驱动源的线网都被解析为正确的逻辑功能并在preverify阶段Check designs时提示"Info: * (*）multiply-driven nets found in reference (implementation) design; see formality.log for list."，用户还可以使用report_multidriven_nets命令进行报告。

默认情况

默认情况下，Formality会首先检查该线网所有驱动源的类型：如果所有驱动源中都不存在输入端口(Port)和黑盒输出引脚(BBPin)，那么Formality会使用consensus函数进行解析；但是如果驱动源中存在输入端口和黑盒输出引脚，Formality无法确定该驱动源的实际值，在这种情况下，Formality会在该位置插入一个被称为BBOX_NET或称为BBNet的黑盒比较点（也就是说，不是所有的多驱动线网都会被识别为BBNet）。

set_parameter命令

set_parameter命令可用于设置一个设计的多驱动线网的解析方式，其语法如下所示。

set_parameters {-resolution consensus | blackbox | and | or} designID

consensus

当-resolution选项指定为consensus时（默认），Formality使用consensus函数进行解析对多驱动线网进行解析，即将按照与四态仿真器相同的方式解析每个网络，每个驱动源可以具有以下四种输出值之一：0、1、X、Z。

表1展示了有两个驱动源的线网解析结果。

对于两个驱动源以上的线网，其解析方式类似，遵循下面的规则：

1、如果该驱动线网只受到驱动源为Z（如有）和驱动源非X的同值驱动源驱动，其结果为该共同值。

2、如果任意两个非Z驱动源产生冲突，则结果为X。

3、如果任意一个驱动源为X，则结果为X。

在逻辑锥视图中把鼠标悬停到多驱动线网上时，会显示"Consensus resolution"，如图1所示。

图1 consensus解析方式

blackbox

当-resolution选项指定为blackbox时，Formality将把多驱动线网视为一个新的BBNet类型的比较点，当其扇入逻辑锥中的比较点匹配且值相等时，比较点被认为等价。

在逻辑锥视图中把鼠标悬停到多驱动线网上时，会显示"Black box resolution"，如图2所示。

图2 blackbox解析方式

and

当-resolution选项指定为and时，Formality使用线与的方式解析多驱动线网，当使用CMOS工艺时，不应该指定该参数。线与遵循下面的解析规则：

1、如果该驱动线网只受到驱动源为Z（如有）和驱动源非X的同值驱动源驱动，其结果为该共同值。

2、如果任意一个驱动源为0，则结果为0。

3、如果任意一个驱动源为X，且不存在驱动源为0，则结果为X。

在逻辑锥视图中把鼠标悬停到多驱动线网上时，会显示"AND resolution"，如图3所示。

图3 and解析方式

or

当-resolution选项指定为or时，Formality使用线或的方式解析多驱动线网，当使用CMOS工艺时，不应该指定该参数。线或遵循下面的解析规则：

1、如果该驱动线网只受到驱动源为Z（如有）和驱动源非X的同值驱动源驱动，其结果为该共同值。

2、如果任意一个驱动源为1，则结果为1。

3、如果任意一个驱动源为X，且不存在驱动源为1，则结果为X。

在逻辑锥视图中把鼠标悬停到多驱动线网上时，会显示"OR resolution"，如图4所示。

图4 or解析方式

set_net_resolution命令

使用set_net_resolution命令还可以指定特定多驱动线网的解析方式，其语法如下所示。

set_net_resolution [-force] {-resolution consensus | blackbox | and | or | onehot | parallel | parallel_onehot} objectID

相比与set_parameter命令，set_net_resolution命令多了三个选项参数onehot、parallel、 parallel_onehot。这些选项用于UPF相关的多驱动线网，它们来自create_supply_net命令的-resolve选项的同名参数，具体信息可参考UPF中的"Resolutions methods"一节，在此不进行赘述。