When doing property checking there are some additional verification work that will ensure the success of applying formal to a design. In this session we’ll review what makes a design observable and controllable. Next we’ll look at doing reachability analysis for understanding if a design is a good candidate for applying formal techniques. This can also be used in more advanced techniques for bounded proof analysis. We’ll also explore how reachability can be used in over constraint analysis. This is possible by looking at how much of the design is unreachable with one set of constraints vs. another set of constraints. If a design is over constrained, formal can’t explore the full state space of the design and bugs may be missed. This is a vital component of an assurance based flow.