Hardware Design Verification

Chapter 7. Chapter Highlights Sets and operationsRelation, partition, partially ordered set, and latticeBoolean functions and representationsBoolean functional operatorsFinite-state automata and languages Simulation-based verification relies much...

7.1. A set is a collection of distinct objects, and the objects, called the members of the set, are enclosed in a pair of curly braces. Set S, consisting of alphanumeric symbols x, 2, $, 3, %, and L2, can be written as S = {x, 2, $, 3, %, L2}. Insi...

7.2. Mapping m between two sets S1 and S2, denoted by m(S1,S2), associates each element in S1 with an element or a subset in S2. An example of a mapping is the procedure that takes in a photograph and outputs all colors in the photograph. In this e...

7.3. Let B denote the set {0, 1}. A Boolean function of n variables is a mapping from Bn to B, written as . An example is . The set of variables in a Boolean function is called the support, denoted by supp(f). Thus, for the previous example functi...

7.4. In this section, we will study some common operators encountered in formal verification. Cofactor operation on function f with respect to a variable x has two phasesa positive and negative phasedenoted by fx and respectively. Cofactor fx is c...

7.5. In computer science literature, finite-state automata are used in the place of finite-state machines, with minor differences. A finite-state automaton accepts input symbols and transits just like a finite-state machine, but it does not produce...

7.6. In this chapter we reviewed some of the basic mathematics encountered in formal verification. We started with set operations and then defined relations among sets. An especially interesting relation is the equivalence relation, based on which ...

7.7. 1.The power set of set S, denoted by 2s, is defined to be the set of all subsets of S. Find the power set of set S ={{a,b}, {8, 11}, {%}}.For any arbitrary set S, relate |2S| to |S|. 2.Determine which of the following is an equivalence relat...