大规模集成电路验证3.ppt

* * * * * * * * * * * * * * * * * Sequential Equivalence Checking Example Sequential Equivalence Checking Example Sequential Equivalence Checking Example Sequential Equivalence Checking Example * * * * * * * * * * * * * * * * * * * * * * * * * * * * Agenda Part.1 Basic of FV Part.2 Equality Check Part.3 ABV Part.3 Assertion-Based Verification Assertion: An if statement with an error condition that indicates that the condition in the if statement be(come) false. Assertions used in SW design for a long time. assert() function part of C #include assert.h Used to detect NULL pointers, out-of-range data, ensure loop invariants, etc VHDL also has assert() statement - but never popular. Only used to terminate simulation. Foster and Bening’s OVL for Verilog. SystemVerilog now offers assertions to Verilog users. SW Assertion Checks SW assertions: Check that condition evaluates to TRUE exactly at time when assert statement is executed. Essentially a “zero-time test”. Not sufficient for HW assertions! Why? SW vs HW Assertions HW assertions: static (i.e. “zero-time”) conditions that ensure functional correctness Must be valid at all times “This buffer never overflows.” “This register always holds a single-digit value.” temporal conditions - to verify functional behaviour over a period of time “The grant signal must be asserted for a single clock cycle.” “A request must always be followed by a grant or an abort within 5 clock cycles.” HW Assertions (Some) HW assertion conditions must be evaluated over time!! Need temporal assertion specification language! Classes of Assertions – Implementation Implementation assertions: Specified by the designer. encode designer’s assumptions e.g. on interfaces state conditions of design misuse or design faults detect buffer over/under flow, signal read write at the same time Implementation assertions can detect discrepancies between design assumptions and implementation. But implementation assertions won’t detect discrepancies betwe