( ESNUG 345 Item 7 ) ---------------------------------------------- [3/1/00]
Subject: ( ESNUG 343 #5 ) "Don't Care" X's In DC 99.05/.10 Are Messed Up
> Here's a recent issue I found with Synopsys DC 99.05/.10 that other users
> may be interested in hearing about. I have a wire defined as:
>
> assign mask3 = {byte1[7],6'hx,byte1[7],byte2[7],byte2[7],5'hx,byte2[7],
> byte1[6],6'hx,byte1[6],byte2[6],byte2[6],5'hx,byte2[6],
> byte1[5],6'hx,byte1[5],byte2[5],byte2[5],5'hx,byte2[5],
> byte1[4],6'hx,byte1[4],byte2[4],byte2[4],5'hx,byte2[4],
> byte1[3],6'hx,byte1[3],byte2[3],byte2[3],5'hx,byte2[3],
> byte1[2],6'hx,byte1[2],byte2[2],byte2[2],5'hx,byte2[2],
> byte1[1],6'hx,byte1[1],byte2[1],byte2[1],5'hx,byte2[1],
> byte1[0],6'hx,byte1[0],byte2[0],byte2[0],5'hx,byte2[0]};
>
> And used in the RTL as:
>
> casex({ena1, ena2, ena3, ena4, DATA[191:0]})
> {1'b1, 1'bx, 1'b0, 1'b1, 1'bx,mask1,63'hx}: flag <= #1 1;
> {1'b0, 1'b1, 1'b0, 1'b1, 1'bx,mask2,63'hx}: flag <= #1 1;
> {1'b0, 1'b0, 1'b0, 1'b1, 1'bx,mask3,63'hx}: flag <= #1 1;
> default: flag <= #1 0;
> endcase
>
> Well, it turns out DC is not carrying the "don't care" x's over into the
> casex statements correctly when analyzing/mapping/etc of the RTL.
> Verilog-XL sims are functionally correct, but the gate-level are wrong.
> When I edit the RTL and place the wire assignment value directly into the
> casex statements, all is fine with the Synopsys gate-level result. I let
> Synopsys know about this problem and they have been examining the problem
> for the last several weeks. If it is an illegal coding style, Synopsys DC
> never complains about it.
>
> - Mike Jarchi
> Vitesse Semiconductor Corp. Camarillo, CA
From: Vigyan Singhal <vigyan@home.com>
To: Michael Jarchi <jarchi@vitesse.com>
Hi Mike,
What you have found is not a synthesis bug, but a problem with a synthesis
and simulation semantic mismatch when signals are assigned to "X"s. I am
surprised that Synopsys is taking weeks to figure this one out! Let me
explain the reasoning, using a simple example, inspired by your design:
module test(cond, tag, value, data);
input cond, tag;
output value, data;
reg data;
assign value = cond ? 1'b0; 1'bx;
always @(tag or value) begin
casex(tag)
value : data <= 1'b0;
default: data <= 1'b1;
endcase
end
endmodule
Consider the case when "cond" is 0. Depending on the synthesis tool you
have, the value of "value" will be either 0 or 1 (and not X, unlike
simulation; most synthesis tools will pick 0 in order to simplify the
logic). Regardless of whether the synthesis tool chooses 0 or 1, you will
have a synthesis-simulation mismatch. See below:
If the synthesized gates set "value" to 0 (when "cond" is 0):
simulation: when input "tag" is 1, output "data" will be 0
synthesis: when input "tag" is 1, output "data" will be 1
If the synthesized gates set "value" to 1 (when "cond" is 0):
simulation: when input "tag" is 0, output "data" will be 0
synthesis: when input "tag" is 0, output "data" will be 1
I do not know any way around this. If it was me, I would in-line the
assignment into the case statement (like you already tried), AND use
"casez" instead of "casex" (the latter for different reasons; see the
ESNUG'99 article from Mills/Cummings).
- Vigyan Singhal
---- ---- ---- ---- ---- ---- ----
From: Michael Jarchi <jarchi@vitesse.com>
Hi John,
I sent the text of Vigyan Singhal's email to me to the Synopsys tech support
engineer working my case. He was not making a lot of headway with their
Formaility equivalence checker as it ran for over 2 days before he had to
kill the run. (As a side note even Chrysalis with the correct design took
only a few hours.) In any event, Vigyan's comments made sense to me given
that my workaround was successful; our CAD group also pulled something
similar from the SNUG'99 Proceedings. Basically, there is an issue with the
usage/interpretation of "don't cares". This is not the same issue regarding
"X"(unknown) in simulation and "x"(don't care) in synthesis where mismatches
can occur and are dangerous. This is more of DC assigning a value (0/1) to
the "dont care" assignment prior to insertion into the casex statement. My
solution, as was Vigyan's, was to paste the assignment statement directly
into the casex statement to work around this problem. The closure from my
understanding is that Synopsys planned on putting this explanation into
their support database for future issues related to this. I did not get the
feeling that this was interpreted as a DC "bug". Another case why even for
RTL-to-Gate compares, Formal Verification has huge value.
- Mike Jarchi
Vitesse Semiconductor Corp. Camarillo, CA
|
|
