|
CTL Model checking in VIS
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.
|
