formality问题求教
时间：10-02
整理：3721RD
点击：
有一段代码两个寄存器有相同的驱动电路：
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。
请高手指点，感激不尽！
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。
请高手指点，感激不尽！
使用寄存器合并命令，好像是guide_register_merging，记不太清了
SVF有哪些项被Rejected?
加载svf，我只能说
我试了一下：
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里都可以吗，是不是我写的格式不对?
谢谢解答 ！
综合不是自动有svf产生的么，从dc， 不需要自己写的啊
我不是用DC综合的，用的RC
那用conformal lec 做formal吧， 用formality不容易过的
有没有一个例子啊，贴一段我参照一下。
多谢了啊！
good tips