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:
- Use in RTL to indicated don't care degrees of freedom to synthesis.
- Uninitialized flops.
Terms
- X-propagation is the process of outputing an X from a block of logic when it's inputs are X.
- X-pessimism Is the condition when output of a block of logic is X in cases where it never could be based upon the inputs.
- X-optimism or X-squashing Is the condition when a block of logic outputs a non-X value when one or more of it's inputs are X. Note this naturally occurs in verilog due to the fact that X's are interpreted as 0's in conditional expressions.
Theory of Operation
Here is an example:
if( select )
out = in1;
else
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.
Transformations
If Transformation
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
Case Constructs
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
Assignment with Bit Select
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
Assignment with Part Select
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
Assignment to Array with Index
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:
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
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
? Operator
This code is transformed:
`
out = cond ? in1 : in2;
to:
out = cond ? in1 : ~cond ? in2 : 1'hx;
Clock Enables
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