assertions part2

SystemVerilog Assertions (SVA) are an essential part of Design Verification used to check whether a digital design behaves according to its specification by expressing expected behavior as executable properties that are evaluated during simulation or formal verification; the first image explains the practical application of assertions through action blocks, traditional verification, controllability and observability, and the responsibilities of design and verification engineers, while the second image explains the fundamental building blocks of SVA, including Boolean expressions, sequences, properties, assertion keywords, temporal operators, sampled-value functions, and coverage properties. An assertion generally consists of a Boolean expression, which represents a condition that must be true at a sampling point, a sequence, which describes a temporal pattern of events across clock cycles, and a property, which combines sequences and temporal relationships to specify the required design behavior; the assert property statement activates the check during simulation or formal verification, and an optional action block executes when the assertion passes or fails, using system tasks such as $display to print informational messages, $info to report information, $warning to generate warnings, $error to report errors while allowing simulation to continue, and $fatal to terminate simulation. For example, a request-and-acknowledgment protocol can be verified using property p_req_ack; @(posedge clk) disable iff (!rst_n) req |##[1:3] ack; endproperty assert property (p_req_ack) else $error("ACK missing");, which checks that whenever req is sampled high, ack must be sampled high within one to three clock cycles, provided reset is inactive; the overlapped implication operator starts checking the consequent from the same sampling cycle as the antecedent, whereas the non-overlapped implication operator starts checking from the next sampling cycle. Sequence delay operators such as ##1, ##2, and ##[1:3] specify exact or ranged clock-cycle delays, while repetition operators such as [*3], [*1:4], and [*0:$] describe consecutive repetitions, bounded repetition, and zero-or-more repetitions, respectively. Boolean expressions can combine signals using logical AND (&&), logical OR (||), logical NOT (!), equality (==), inequality (!=), relational operators , and set-membership expressions using inside; for example, req && ready checks that both signals are high at the sampling point. Sampled-value functions provide additional temporal checks: $past(signal) retrieves a previous sampled value, $stable(signal) checks whether a signal has remained unchanged between consecutive sampled values, $rose(signal) detects a transition from low to high, $fell(signal) detects a transition from high to low, $changed(signal) detects a change from the previous sampled value, and $isunknown(signal) detects X or Z values. These functions are useful for checking requirements such as data stability during a stalled AXI transaction, reset behavior, and control-signal transitions. The images also distinguish traditional verification from assertion-based verification: traditional verification typically uses stimulus generators, drivers, monitors, scoreboards, checkers, and coverage collectors to apply transactions to the DUT, observe its responses, compare actual results against expected results, and measure verification progress, while assertions continuously check specific protocol rules and internal design requirements. For FIFO verification, assertions can check that full and empty are never simultaneously high, that a read is not accepted when the FIFO is empty, and that a write is not accepted when it is full; for example, property p_no_full_empty; @(posedge clk) disable iff (!rst_n) !(full && empty); endproperty assert property (p_no_full_empty) else $error("FIFO full and empty both high");. Controllability refers to the ability to drive the DUT into a particular state or condition through suitable inputs and stimulus, whereas observability refers to the ability to detect the resulting behavior through outputs, internal signals, assertions, or status indicators; both are important for reaching corner cases and identifying failures. For example, an APB testbench can control PSEL, PENABLE, and PREADY to create setup, access, and wait states, while assertions observe whether the protocol transitions occur correctly. The images further explain that design engineers generally write implementation-specific assertions for internal state machines, counters, pipelines, and datapath rules, while verification engineers write protocol- and specification-based assertions for interface handshakes, timing requirements, and protocol compliance.