lec formality inconclusive举例

情况1：output port连接常量电平(形成loop)

设计

module sub( input a,b,c,output d,e );
assign d = a ^ b | c;
assign e = a ^ b ^ c;
endmodule

module rtl_out_fixed1( input in1,
input in2,
output reg out1,
input clk,
input rstn);
wire d;
always@(posedge clk or negedge rstn)
if(!rstn)
out1 <= #1 1’b0;
else
out1 <= #1 d;
sub u_sub(.a(in1),.b(in2),.c(1’b1),.d(d),.e**(1’b1)**);
endmodule

综合结果

module sub_0 ( a, b, c, d, e );
input a, b, c;
output d, e;
wire n1;
wand e;

AOI21B1X1AS9 U3 ( .A1(n1), .A2©, .B1B(d), .O(e) );
AOI22B2X1AS9 U1 ( .A1(a), .A2(b), .B1B(a), .B2B(b), .O(n1) );
OR2X1AS9 U2 ( .I1©, .I2(n1), .O(d) );
endmodule

module rtl_out_fixed1 ( in1, in2, out1, clk, rstn );
input in1, in2, clk, rstn;
output out1;
wire d, n5;

sub_0 u_sub ( .a(in1), .b(in2), .c(n5), .d(d), .e(n5) );
DFFRBQX1AS9 out1_reg ( .D(d), .CK(clk), .RB(rstn), .Q(out1) );
endmodule

现象

********************************* Verification Results *********************************
Verification INCONCLUSIVE
(Equivalence checking aborted due to complexity)
Reference design: r:/WORK/rtl_out_fixed1
Implementation design: i:/WORK/rtl_out_fixed1
1 Passing compare points
1 Aborted compare points
0 Unverified compare points
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
Passing (equivalent) 0 0 0 0 1 0 0 1
Failing (not equivalent) 0 0 0 0 0 0 0 0
Aborted
Loop (cycle-driven) 0 0 0 0 0 1 0 1

---

fm>analyze_points -failing
Error: No matched compare points to diagnose or analyze (FM-213)
fm> diagnose
Error: Diagnosis and analysis can only be performed after an unsucessful verification (FM-006)

根据报告中的Loop问题，
fm> report_loops
There is(are) 1 loop(s) found in the implementation design :
Loop 1 :
(Pin) i:/WORK/rtl_out_fixed1/u_sub/U2/O
==> (Net) i:/WORK/rtl_out_fixed1/u_sub/d
(Net) i:/WORK/rtl_out_fixed1/u_sub/d
==> (Pin) i:/WORK/rtl_out_fixed1/u_sub/U3/B1B
(Pin) i:/WORK/rtl_out_fixed1/u_sub/U3/O
==> (Net) i:/WORK/rtl_out_fixed1/u_sub/e
(Net) i:/WORK/rtl_out_fixed1/u_sub/e
==> (Pin) i:/WORK/rtl_out_fixed1/u_sub/e
(Pin) i:/WORK/rtl_out_fixed1/u_sub/e
==> (Net) i:/WORK/rtl_out_fixed1/n5
(Net) i:/WORK/rtl_out_fixed1/n5
==> (Pin) i:/WORK/rtl_out_fixed1/u_sub/c
(Pin) i:/WORK/rtl_out_fixed1/u_sub/c
==> (Net) i:/WORK/rtl_out_fixed1/u_sub/c
(Net) i:/WORK/rtl_out_fixed1/u_sub/c
==> (Pin) i:/WORK/rtl_out_fixed1/u_sub/U2/I1
==> (Pin) i:/WORK/rtl_out_fixed1/u_sub/U3/A2

实际上不存在loops，但是工具会把 n5连接回去，形成loop。

改正

sub u_sub(.a(in1),.b(in2),.c(1'b1),.d(d),.e());
1

********************************* Verification Results *********************************
Verification SUCCEEDED
Reference design: r:/WORK/rtl_out_fixed1
Implementation design: i:/WORK/rtl_out_fixed1
2 Passing compare points

Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL

Passing (equivalent) 0 0 0 0 1 1 0 2
Failing (not equivalent) 0 0 0 0 0 0 0 0

---