formality问题求教

thrall_17 · 发表于 2015-9-14 21:33:24

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

有一段代码两个寄存器有相同的驱动电路：
always@(posedge clk or negedge rstn）
begin
if(!rstn)
a <= 0;
else
a <= x & y | z;
end

always@(posedge clk or negedge rstn）
begin
if(!rstn)
b<= 0;
else
b <= x & y | z;
end

a和b 的有相同的逻辑，所以b在综合是被优化掉了。
在用formality做形式验证时r:a_reg 和 i:a_reg能match上；而r:b_reg无法match。
因为a和b各自又驱动其他电路，所以导致r:b_reg驱动的电路verify失败。

尝试用set_user_match r:b_reg i:a_reg约束，这样会导致r:a_reg又无法match。

请高手指点，感激不尽！

zmt206 · 发表于 2015-9-15 20:25:17

使用寄存器合并命令，好像是guide_register_merging，记不太清了

Timme · 发表于 2015-9-15 20:43:55

本帖最后由 Timme 于 2015-9-15 20:44 编辑

SVF有哪些项被Rejected？

icfbicfb · 发表于 2015-9-17 11:25:25

加载svf，我只能说

thrall_17 · 发表于 2015-9-21 20:29:36

我试了一下：
1. 在tcl里加入：
guide
guide_reg_merging -design top -from a_reg -to b_reg
setup
read ...
...
这样没效果。

也试了设置SVF
set_svf top.svf
在top.svf里加入guide_reg_merging，也没有效果。

请问加在tcl里和svf里都可以吗，是不是我写的格式不对？
谢谢解答！