CTL Model checking in VIS

Create a description of your model in the form of a finite state machine (using Verilog).
Prepare a list of properties you want to check.
Translate them into CTL formulae and put them in a file.
Use the VIS command “mc file.ctl”.
If some property fails, debug your design with the help of the error trace.
At the end, you should feel more confident about your design.
Onus on the designer to come up with a set of suitable properties.