Article ID: 000080715 Content Type: Troubleshooting Last Reviewed: 09/11/2012

Why do state machines with the full_case synthesis attribute result in formal verification mismatches?

Environment

BUILT IN - ARTICLE INTRO SECOND COMPONENT
Description

When you apply a full_case synthesis attribute to a case statement header, it instructs tools to interpret unspecified states as “don’t care” values.  The Quartus® II software infers additional logic to represent the "don't care" states. This additional logic can be different from the logic inferred by the formal verification tool, resulting in formal verification mismatches.

To overcome the mismatches, define all the states in the state machine. 

Refer to the Recommended HDL Coding Styles (PDF)  chapter in volume 1 of the Quartus II handbook for more information on state machine coding guidelines.

Related Products

This article applies to 1 products

Stratix® FPGAs