An assertion is the execution of a property within a dynamic execution environment, such as a simulator or emulator. A property defines functionality about a design in a way that something must either be true or never true. In rare cases it can also define fairness. As an example, a property for a car may be that the car may not accelerate when the brake pedal is depressed, or that the key cannot be removed until the car has been placed in park. An example of fairness may be that everyone from an expanding pool of people will get served within a specified period of time. Properties may or may not involve time. In the second example, a sequence is defined whereby the car has to be placed in park before the key is removed. A similar sequence could be defined to say that the car cannot be taken out of park until the key is in the ignition. Once such properties have been written, they can become part of a simulation and if they are ever triggered, will display a warning or stop the simulation.
Properties can be written in languages such as the Property Specification Language (PSL, IEEE 1850) or SystemVerilog (IEEE 1800). Their language structure is very different than other aspects of the testbench and belong to the class of language called declarative languages. Most of the other languages used within design and verification are procedural languages.
declarative languages generally have three parts, the left hand side, called the antecedent, an operator and a right hand side, called the consequent. An expression can be read as when something happens (the antecedent) then it implies (the operator) that something else will happen (the consequent). Each language has different rules for the construction of each of these parts.
Properties can also be used in formal verification tools where the tool will explore if it ever possible to make a property become true or false. Properties are also used as a means of determining coverage.