Formal property checking

Question 1

Which is the typical methodology for Property Checking

of SoC modules:

Answer 1

• Adopt an operational view of the design
• Each operation can be associated with certain
“important control states” in which the operation
starts and ends
• Specify a set of properties for every operation,
i.e., for every important control state
• Verify the module operation by operation by
moving along the important control states of the
design
• The module is verified when every operation
has been covered by a set of properties

Question 2

What a property for RT-level module verification consists of?

Answer 2

Assumptions:

• we start in a certain control state.
• a certain input sequence arrives.

Commitments:

• certain input/output relations hold.
• operation ends in a certain control state.

Question 3

What is the task of reachability analysis and why its a problem?

Answer 3

Given: finite state machine M with initial states S0
task: find the set of all states R which are possible (“reachable”) in M through arbitrary input sequences starting from S0.

Computation and representation of state sets are very hard problems !

Question 4

What is a bounded model for property checking.

Answer 4

Is the unrolled finite state machine: Concatenate k copies of combinational logic for the output and transition function („time frames“).

Question 5

What is completeness proving?

Answer 5

Describing all possible behaviors using properties.

Question 6

By considering design behavior within bounded time interval it is possible to map design and property (assumption + commitment) to a Boolean satisfiability problem (SAT). What problem may occur using this method?

Answer 6

Assuming that all states are reachable at time t may lead to counterexamples in bounded model that are not reachable in actual design
(Partial) cure: careful formulation of assumptions