IEEE-1800-2009/2012 Features

Abstract

This chapter describes the new features of the 2009/2012 LRM. In that sense, it is a long chapter. It describes features such as “strong” and “weak” properties, abort system tasks, deferred immediate assertions, and past and future global clock-based sampling functions such as $rose_gclk, $fell_gclk, $rising_gclk, and $falling_gclk. It further covers “followed by” property operators and “always,” “eventually,” “until,” “nexttime,” “case,” as well as $inferred_clock and $inferred_disable. Also covered are “restrict” operator for formal verification, “reject”/“accept” properties, and assertion control tasks.