XST bug on illigal states of a FSM ?

Hi,

 I coded a very simple state machine (verilog code below).
The state machine has the "default" condition; this should ensure that
if an illegal state is reached, the machine will recover and go back
to a legal state.
I synthesized it with Xilix XST (ISE 9.2) with the Encoding option one-
hot.
I really suspect that the synthesis does not handle properly the
illegal states; for instance looking at the RTL schematics or the
technolgy schematics generated by ISE: if I assume that there is an
illigal state like "000" I see that the machine will stay there
forever.
Is there any more formal way to prove it (to myself and to the xilinx
support) other than a visual inspection of the schematic ?
Simulation (with xilix simulator) is not easy because in simulation
the machine will never go to an illigal state.
But I suspect that is what happens very rarely on my real hardware
(and this is costing me a lot).

 Thanks,

   Tullio

//////////////////////////////////////////////////////
`timescale 1ns / 1ps

module I2D_State  (
  input  clk, Er, DV,
  output reg I2D      );

  reg  [2:0]  I2D_State = 3'b001;

 // Detect a transition of (Er, DV) from (0, 0) to (0, 1)
 always @(posedge clk)   case(I2D_State)
    3'b001: begin
      I2D <= 0;
      if (~Er & ~DV) I2D_State  <= 3'b010;  // (0, 0) detected
    end
    3'b010: if (~Er & DV) begin
         I2D_State  <= 3'b100;  // (0, 1) detected
         I2D <= 1;
      end   // else do nothing, regs will keep their values.
    3'b100: begin
         I2D_State  <= 3'b001;   // stay only 1 tick in this state.
         I2D <= 0;
      end
    default: I2D_State <= 3'b001;
 endcase

endmodule
/////////////////////////////////////////////

XST-Guide:

"XST can add logic to your FSM implementation that will let your state
machine recover
from an invalid state. If during its execution, a state machine enters
an invalid state, the
logic added by XST will bring it back to a known state, called a
recovery state. This is
known as Safe Implementation mode.
To activate Safe FSM implementation: [...]
"

Did you really "activate" Safe FSM implementation ?

I (personally) wouldn't like to activate it on a 1-hot FSM, as it
intoduces "a lot" of additional ressources...

Regards
Jochen

Your state machine should never get into an "illegal state" regardless
of what it does if you are operating in a "standard" environment (ie,
not in space, in a nuclear reactor, or in the engine bay of a car). If
it is getting into such a state, your design breaks synchronous design
principles. Adding in a default case to try to "fix" that is at best
fixing a symptom instead of the cause and at worse could break your
system. Are you sure your system actually could tolerate randomly
going into your default state? I suspect the inputs to your state
machine are not actually synchronized into the state machine's clock
domain. If you are currently using a synchronizer, ensure that the
delay between the first and second flip-flops is as little as
possible. At very high frequencies, it is possible that the routing
delay between the two flip-flops in a synchronizer plus the possible
metastable delay in your synchronizer can exceed one clock cycle.

As an aside, if you are actually operating in an extreme environment
and do need to consider state corruption due to particle-induced
events, you can actually force the state machine into an illegal state
since you're using Verilog. Just do a gate-level simulation and use
the Verilog "force" keyword to override the state variable into what
you want it to be. This can be useful to see if your system actually
will survive going to the default case.

tullio wrote:
> Hi,
> 
>  I coded a very simple state machine (verilog code below).
> The state machine has the "default" condition; this should ensure that
> if an illegal state is reached, the machine will recover and go back
> to a legal state.

An "extracted" FSM won't be "safe" unless you specify a safe option or 
explicitly code it and turn off the FSM extraction mode.  But there is 
no reason for an FSM to be safe unless you expect metastability or alpha 
particle hits.  Making the FSM safe requires a lot of extra logic and a 
decrease in speed.
-Kevin

On Wed, 3 Sep 2008 08:00:31 -0700 (PDT), tullio
<tullio.grassi@gmail.com> wrote:

>Is there any more formal way to prove it (to myself and to the xilinx
>support) other than a visual inspection of the schematic ?
>Simulation (with xilix simulator) is not easy because in simulation
>the machine will never go to an illigal state.

Yes... simulate it properly! Use a 'force' statement to set your state
register to an illegal value, clock it, see what happens.

Of course, this is hard work, it's pretty tedious, it looks a lot like
programming, and you're much more likely to make a mistake in your
testbench than your RTL. So, I've gone to the trouble of doing it for
you. Testbench attached below; you'll notice that it tests the entire
FSM, rather than just the illegal state exit.

The good news is that your RTL works. save the code below to
'test1.tv', save your own code as 'test.v', and run rtv:

# rtv test1.tv test1.v
(Log)        (150 ns) 15 vectors executed (22 passes, 0 fails)

As a sanity check, change the expected output value in the last
statement from 0b001 to 0b111, and rtv's output changes to:

# rtv test1.tv test1.v
(Error)      ('test1.tv', line 36, 149 ns) 'top.I2D_State.I2D_State':
expected 'b111; got 'b001
(Log)        (150 ns) 15 vectors executed (21 passes, 1 fails)

Now get a Verilog netlist out of  XST, and repeat the test with the
netlist rather than 'test1.v'. If the test now fails, XST is broken.

You can get rtv from www.maia-eda.net.

-Evan

[and yes, this *is* a plug for Maia; couldn't help myself. The code
below is trivial; it gets much better than this].

=============================================================
test code: watch out for line wrapping; some of the comments
may appear to be on a second line

DUT {
   module I2D_State(                // declare the module
      input  clk, Er, DV,
      output reg I2D);

   signal(inout [2:0] I2D_State);   // declare any internal sigs to
test

   // declare any clocks, and any vectors
   create_clock clk;
   [clk, I2D_State, Er, DV] -> [I2D_State, I2D];
}

// no FSM reset, so force to a known state, and check transition from
3`b001
[.C, 0b001,  1,  1] -> [0b001, 0];  // force the state register
[.C, .R,     1,  1] -> [0b001, 0];  // release the state register 
[.C, -,      1, .X] -> [0b001, 0];  // leave the state register
undriven
[.C, -,     .X,  1] -> [0b001, 0];
[.C, -,      0,  0] -> [0b010, 0];

// transition from 3`b010
[.C, -,      1, .X] -> [0b010, 0];
[.C, -,     .X,  0] -> [0b010, 0];
[.C, -,      0,  1] -> [0b100, 1];

// transition from 3`b100
[.C, -,     .X, .X] -> [0b001, 0];

// force to an illegal state, check exit
[.C, -,     .X, .X] -> [-,     -];  // flush: see FAQ
[.C, 0b000, .X, .X] -> [0b000, -];  // force the state register to 0
[.C, .R,    .X, .X] -> [0b001, -];  // confirm that we recover to
0b001

// try another illegal state
[.C, -,     .X, .X] -> [-,     -];  // flush: see FAQ
[.C, 0b111, .X, .X] -> [0b111, -];  // force the state register to
0b111
[.C, .R,    .X, .X] -> [0b001, -];  // confirm that we recover to
0b001
======================================================================

Evan Lavelle wrote:
> On Wed, 3 Sep 2008 08:00:31 -0700 (PDT), tullio
> <tullio.grassi@gmail.com> wrote:
...
> 
> The good news is that your RTL works....
> 
> Now get a Verilog netlist out of  XST, and repeat the test with the
> netlist rather than 'test1.v'. If the test now fails, XST is broken.
> ...
If XST doesn't pass the test, that doesn't mean it is broken in this 
case.  An extracted FSM is not supposed to be identical to RTL.  That is 
the whole idea of FSM extractors.  They take the RTL and recode it, 
possible using a different encoding, and also removing logic related to 
moving to a default state.  You can turn off the extractor, but you 
wouldn't want to.

Here's an example.  These two counters operate in the same way:

reg [7:0] count1=0, count2=0;
always@(posedge clk)
   begin
     if (count1==135) count1 <= 0;
     else count1 <= count1 + 1;
     if (count2>134) count2 <= 0;
     else count2 <= count2 + 1;
   end

You can see that both counters are identical, but if synthesized 
according to the RTL, count2 will have a lot more logic and will be 
slower, because the > with synthesize a subtractor.  But it's just a 
waste of logic, because count2 will never have a value of 136 or 
greater, unless there is an alpha hit or setup violation from a too-fast 
clock.  You actually want the synthesizer to realize this and violate 
the RTL during synthesis.
-Kevin

tullio wrote:
> Hi,
> 
>  I coded a very simple state machine (verilog code below).
> The state machine has the "default" condition; this should ensure that
> if an illegal state is reached, the machine will recover and go back
> to a legal state.
> I synthesized it with Xilix XST (ISE 9.2) with the Encoding option one-
> hot.
> I really suspect that the synthesis does not handle properly the
> illegal states; for instance looking at the RTL schematics or the
> technolgy schematics generated by ISE: if I assume that there is an
> illigal state like "000" I see that the machine will stay there
> forever.
> Is there any more formal way to prove it (to myself and to the xilinx
> support) other than a visual inspection of the schematic ?
> Simulation (with xilix simulator) is not easy because in simulation
> the machine will never go to an illigal state.
> But I suspect that is what happens very rarely on my real hardware
> (and this is costing me a lot).

Your example seems to have only 3 active states, so one way to be sure, 
is to explicitly code the unwanted states.

You can chose a simple binary code, which gives one more illegal state,
or one-hot, which gives 5 more to cover.

Also watch Reset exit : that is usually chosen as a 'safe' state.

-jg

On Wed, 03 Sep 2008 13:43:44 -0600, Kevin Neilson
<kevin_neilson@removethiscomcast.net> wrote:

>Evan Lavelle wrote:
>> On Wed, 3 Sep 2008 08:00:31 -0700 (PDT), tullio
>> <tullio.grassi@gmail.com> wrote:
>...
>> 
>> The good news is that your RTL works....
>> 
>> Now get a Verilog netlist out of  XST, and repeat the test with the
>> netlist rather than 'test1.v'. If the test now fails, XST is broken.
>> ...
>If XST doesn't pass the test, that doesn't mean it is broken in this 
>case.  An extracted FSM is not supposed to be identical to RTL.  That is 
>the whole idea of FSM extractors.  They take the RTL and recode it, 
>possible using a different encoding, and also removing logic related to 
>moving to a default state.  You can turn off the extractor, but you 
>wouldn't want to.

Can you back up the "also removing logic related to moving to a
default state"?

The original RTL is very specific; it describes what to do if the
state is not 001, 010, or 100 (which, BTW, requires a tiny amount of
logic). If the synthesiser doesn't do this, then it's broken.
Specifying a global one-hot option (which, IIRC, is the default
anyway) doesn't give the synth carte blanche to find any sequential
case statements and to remove the default branch.

Besides, how would XST know that this was an FSM anyway? If the docs
are to be believed, it needs to find a state register which is reset,
and (for Verilog) which is either "an integer or a set of defined
parameters". None of these conditions are true in this case.

Yes, if you have an identifiable state register, and you ask the synth
to recode it, then you can get differences in pre- and post-synth
simulation, *if* you expect specific values on your state register.
But, if you want the synthesiser to recode, your simulation should be
testing against enumerated or parameterised values anyway. That's not
the problem the OP is seeing here; he thinks he's losing logic.

Your counter example isn't relevant. Let's assume that the counters
actually are identical, and the synthesiser can determine that it's
impossible for either count1 or count2 to leave the range [0,135]. In
this hypothetical case, the synthesiser is permitted to change the
terminal count logic, *because the change is not observable*. The
synthesiser can do anything it wants, as long as the simulation
semantics of the original code is preserved, or you specifically
request a change in semantics - register retiming, state register
recoding, whatever. This is *not* true of the OP's case; the loss of
logic - if it has actually happened - has changed the behaviour of the
code.

-Evan

Evan,

XST isn't broken, and the FSM optimization is legit. In fact, every
commercial FPGA synthesis tool (Synplify, Precision, QIS, XST, etc)
will perform the same FSM optimization, unless explicitly instructed
not to (typically by tagging the FSM as 'safe').

What we're looking at is called 'dead code elimination'. The synthesis
tools performs a boolean reachability analysis on the state register.
In the Verilog code, there is *no* assignment that ever assigns a
value other than 001, 010, and 100 to the state register. Within the
Verilog semantic, the state register will *never* reach any value
other than these 3. The default clause is thus rightfully ignored and
no 'recovery' logic is generated. As a matter of fact, in absence of
SEUs, your design will *never* get into any other state than these 3.
From a Verilog semantic standpoint, the RTL and the synthesized
netlist are fully equivalent. One can certainly complain that the
Verilog (and VHDL) semantic have no room for SEUs, but that's the way
it is.

Note that this optimization is orthogonal to the state encoding. Also,
while this optimization is frequent for FSMs, it actually also applies
to random logic, although the reachability analysis is often more
difficult to perform.

 - gael

Gael -

I hadn't noticed the initial condition on the register, so I missed
this; my apologies to X for casting aspersions.

The OP's original question was "is there a more formal way to prove it
[to confirm that the RTL and netlist are different]". In this case, he
probably has to do it by simulation, since formal analysis is likely
to show no difference, so the TB is still required to show that a
transformation has taken place. Still, a useful reminder of the
pitfalls of comparing pre- and post-synth results.

-Evan