1 PSL - Property specification language
1.1 Property
- Characteristics of the designs/verification environment
– Behavior represented by a sequence of temporal (over time) relationships of Boolean expressions.
1.2 Verification
- confirming that, for a given design and a given set of constraints, a property that is required to hold in design actually does hold those constraints
1.3 ABV with PSL
- ABV is a documentation and verification methodology (Instruments system requiremets, interfaces, design and verification enviroments with assertions)
- PSL is a property specification language
2 External assertion files
Syntax and example
1 -- VHDL flavor, Separate file linked at compile time 2 vunit abc_if_vu (entity_name(architecture_name)) 3 { 4 default clock is (clk'event and clk = '1'); 5 property A1 is never (a and b); 6 assert A1 ; 7 }
3 More on PSL
-- Documents requirements
* system, interface, design
-- Defines combinational temporal properties
* embedded into design HDL spurce, or
* seperately in vunit files
* carried at all phases of sublocks process
-- Enable verification of assertions
* dynamically during simulation
* statically through formal verification