In reply to bmorris:
In reply to ben@SystemVerilog.us:
After reviewing your reply, Let me know if the following statements are accurate…
An assertion can be made at several levels, and described with little to no wiggle-room for misunderstanding, using SVA (as one method).
[Ben] Agreed. Complex assertions should be verified on their own merit. Code reviews and simulation with constrained-random tests is another way.
There can be assertions based on requirements; these assertions are independent of architecture or implementation.
[Ben] Yes, absolutely. In SVA, use “SV checkers” bound to the DUT and/or SV interfaces.
There can ALSO be assertions placed on low-level design constructs as the designer sees fit (writing a full-FIFO is not allowed). It has zip to do with the DUT requirements, but it enforces healthy RTL behavior according to the implementer. These assertions are tightly coupled / dependent on architecture or implementation. Do these have a special name?
[Ben] They are often referred to as RTL assertions, as they affect the design. They also define/clarify the designer’s assumptions (SVA assume directive). These include things that the designer may take advantage of, of knows of because of other partition interfaces, and thus can take advantage of. They are useful in code reviews too.
// Never a request when ready is false.
m pRequestReady : assume property (@ (posedge clk) not(request && !ready));
am1: assume property (req |=> !req) else $error(“req for more than 1 cycle”);
ap_min_load: assume property(
ld |-> not(data_in<MIN_COUNT));