Exercise(cont)

Exercise(cont)

• Formulate properties in CTL, and model check.
• Does the design satisfy the property ?
• If not modify the design to make property pass.
• Note that arbiter is inefficient. Construct a more efficient arbiter.
• Write a property to show your arbiter is better.

Previous slide

Next slide

Back to the first slide

View Graphic Version