|
|
Xprop is a tool that instruments verilog code such that x's are propagated and not squashed.
This is desirable as it reduces the simulation differences between RTL and gate level simulations. This sometimes masks bugs in RTL simulations and thereby requires a much greater degree of gate level simulation be performed. It is the experience of many who have used this tool that most of the discovered bug at the gate level would have been caught at the RTL simulation level if an xprop tool had been applied prior to RTL simulation.
X's occur in simulation for a number of reasons:
Here is an example:
if( select ) // this branch is taken when cond is 1 out = in1; else // this branch is taken when cond is either 0 or X out = in2;
In this case an X on signal select does not result in out being X. Hence X's are squashed. Synthesis may result in code that looks like this:
out = (in1 & select) | (in2 & select)
The simulation of these statements will not match in all cases. Another example where gate level simulation may not match RTL is for a 2-to-1 mux expressed as:
out = select ? in1 : in2;
However synthesis may result in the following:
out = (in1 & select) | (in2 & select)
When select is X the simulation of these statements will differ.
Similar issues arise with case statements and assignments to variables that use non-constant indices. The solution is to instrument the verilog code to add pessimism to such statements.
One way to model this is whenever an ambitious (relative to X) construct is used there are multiple possible outcomes. These multiple possible outcomes need to be modeled resolving the ambiguity create by the X. This can be done using a XResolution() function. It takes two inputs, one for each possible expression output. The resolution function combines the two possiblities and creates a pessimistic output. For instances the code:
if( select ) out = in1; else out = in2;</pre>
Can be abstractly represented as:
if( ^select === 1'bX ) out = XResolution( in1, in2 ); else if( select ) out = in1; else out = in2;
Vrq uses a very simplistic XResolution function that results in less code bloat and overhead at the expense of increased pessimism. The XResolution function ignores the inputs and always returns X.
The following code snippet:
if( cond ) being
r1 = r2;
end
Is transformed into:
if(cond) begin r1 = r2; end else if(~cond) ; else begin r1 = 1'hx; end
When an else clause is included, this code snippet:
if( cond ) begin r1 = r2; end else begin r1 = r3; end
is transformed into:
if(cond) begin r1 = r2; end else if(~cond) begin r1 = r3; end else begin r1 = 1'hx; end
A case statement without a default clause, like this:
case( cond )
0: out = in0;
1: out = in1;
2: out = in2;
endcase
Is transformed into this:
case(cond) 0: begin out = in0; end 1: begin out = in1; end 2: begin out = in2; end default: begin case(^cond) 1'b0, 1'b1: ; default: begin out = 1'hx; end endcase end endcase
A case statement with a default clause is transformed from:
case( cond ) 0: out = in0; 1: out = in1; 2: out = in2; default: out = in3; endcase
to this:
case(cond) 0: begin out = in0; end 1: begin out = in1; end 2: begin out = in2; end default: begin case(^cond) 1'b0, 1'b1: begin out = in3; end default: begin out = 1'hx; end endcase end endcase
A case statement with a constant case expression is transformed from:
case( 1'b1 ) cond1: out = in0; cond2: out = in1; cond3: out = in2; default: out = in3; endcase
to this:
case(^{cond1,cond2,cond3}) 1'b0, 1'b1: begin case(1'b0) cond1: begin out = in0; end cond2: begin out = in1; end cond3: begin out = in2; end default: begin out = in3; end endcase end default: begin out = 1'hx; end endcase
An assignment with a bit select is transformed from:
reg [3:0] out; ... out[i] = in;
to:
case(^i) 1'b0, 1'b1: begin out[i] = in; end default: begin out = 4'hx; end endcase
An assignment with a part select is transformed from:
reg [1:0] in; reg [3:0] out; ... out[i+:2] = in;
to:
case(^i) 1'b0, 1'b1: begin out[i+:2] = in; end default: begin out = 4'hx; end endcase
The following code gets transformed:
reg [3:0] in; reg [3:0] array[8:0][2:0]; ... array[w][y] = in; array[w][1] = in; array[w][y][1:0] = in[1:0];
to:
// array[w][y] = in; case(^{w,y}) 1'b0, 1'b1: begin array[w][y] = in; end default: begin : ___block0002 integer ___index0000; integer ___index0001; for(___index0001 = 2>=0 ? 0 : 2;___index0001<=(2>=0 ? 2 : 0);___index0001 = ___index0001+1) begin for(___index0000 = 8>=0 ? 0 : 8;___index0000<=(8>=0 ? 8 : 0);___index0000 = ___index0000+1) begin array[___index0000][___index0001] = 4'hx; end end end endcase // array[w][1] = in; case(^w) 1'b0, 1'b1: begin array[w][1] = in; end default: begin : ___block0004 integer ___index0003; for(___index0003 = 8>=0 ? 0 : 8;___index0003<=(8>=0 ? 8 : 0);___index0003 = ___index0003+1) begin array[___index0003][1] = 4'hx; end end endcase // array[w][y][1:0] = in[1:0]; case(^{w,y}) 1'b0, 1'b1: begin array[w][y][1:0] = in[1:0]; end default: begin : ___block0007 integer ___index0005; integer ___index0006; for(___index0006 = 2>=0 ? 0 : 2;___index0006<=(2>=0 ? 2 : 0);___index0006 = ___index0006+1) begin for(___index0005 = 8>=0 ? 0 : 8;___index0005<=(8>=0 ? 8 : 0);___index0005 = ___index0005+1) begin array[___index0005][___index0006][1:0] = 2'hx; end end end endcase
This code is transformed:
` out = cond ? in1 : in2;
to:
out = cond ? in1 : ~cond ? in2 : 1'hx;
This code is transformed:
always @(posedge clk)
r <= r_P;
to:
`ifdef XPROP_BOTH_EDGES always @(clk) `else always @(posedge clk) `endif if( clk ) begin r <= r_P; end else if( ~clk ) ; else begin r <= 1'bx; end
1.7.1