Using PSL/Sugar for Formal and Dynamic Verification: Guide to Property Specification Language for Assertion-based Verificationvhdlcohen publishing, 2004 - 396 lappuses |
Saturs
iv | 1 |
2 | 23 |
5 | 40 |
7 | 65 |
Temporal layer | 73 |
6 | 90 |
8 | 98 |
PSL In Design Process | 147 |
FORMAL VERIFICATION USING PSL | 229 |
AMBATM AHB | 279 |
PSL GUIDELINES | 313 |
PSL BNF and Examples | 335 |
Optional Branching Extensions OBE of PSL | 347 |
Existential OBE Properties | 355 |
PSL Dictionary | 363 |
Definitions | 385 |
Bieži izmantoti vārdi un frāzes
abort Boolean Accellera ack_local architecture behavior Boolean Boolean Boolean expression Boolean until Boolean bus request bus_available Cadence Incisive chapter clk'event and clk clock edge clock is clk'event code coverage current cycle deasserted defined definition demonstrates design and verification downto error eventually example fail false FIFO word count FL_Property formal verification functional coverage functional verification hardware verification languages htrans implementation implicit repetition inactive active input interface layer logical IF implication methodology model checking negedge never next_a next_event next_event_e occur parity posedge clk property holds Property Specification Language protocol provides psl assert psl default clock PSL LRM psl property requirements reset reset_n RTL design s_bits Safelogic SERE shown in Figure signal state2 std_logic suffix implication operator syntax SystemVerilog terminating testbench top level module true UART unified simulator vendors verification unit Verilog flavor VHDL flavor vunit whilenot