## operator

and operation and 148, 156

branching and 60, 151

cycle delays and 45, 47, 56

or operation and 143

precedence of 132, 266

sequences and 12, 41, 46, 51, 274

$assertoff system task 435

$asserton system task 435–436

$bits( ) function 222

$countones function 40

$error function 311–312, 315

$ eventuality operator 61–67, 354

$fatal function

functionality 311, 313, 315

syntax 311

$fell function

disable iff clauses and 265

infinite pattern after reset 354

PSL/SVA support 20

sampled values 30, 36

syntax 33

$info function

functionality 312, 315, 331

syntax 311

$isunbounded function 40

$isunknown function 39

$onehot0 function 38

$onehot function 38

$ova_category_stop system task 440

$past function

coding guidelines 471, 474

disable iff clauses and 265

local variables and 609

overview 30, 36–37

$rose function

disable iff clauses and 265

intersignal dependencies 353

PSL/SVA support 20

sampled values 30, 35–36

syntax 32

$sampled function 30–31

$stable function

disable iff clauses and 265

sampled values 30, 36

syntax 34

$warning function

functionality 312, 315, 331

syntax 311

%m format specification 307, 316

+sva_disable_category plusarg 441, 646

A

abstractions (nondeterminism) 598–601, 642

action blocks

assume property directive and 331

defined 309

immediate assertions and 9

multiple 310

overview 349

pass or fail statements 310

Reactive region and 15

utility functions 311–313, 315, 331

Active region

execute_time_slot routine 16

immediate assertions 315–316, 318

overview 14–15

.triggered method and 198

actual arguments 221

addr signal 544

aggregate number of assertions 460

always blocks 342–343, 346

and operator (conjunction)

Boolean expressions and 158–159

bounding and 364

branching sequences and 151–156

concatenating with sequences 156–157

flow of local variables and 210–212

legal property expressions 271

multiclocked 280–284

multiple consequent matches and 254

non-branching sequences and 148–151

overview 131, 146–148, 213–214, 233–235, 303

property layer and 269

synchronizers and 274

antecedents

condition expressions and 236

consequent matches and 247–250

cycle delays and 291

enabling condition inference 347

implications and 611

multiple matches 247–250, 254

negated vacuous matches and 259

overlapping implication operator and 240,  262

passing implications vacuously 236

as preconditions 246

properties and 240, 260, 263, 269

as sequence expressions 269

sequences and 257

unbounded 251–253

vacuity and 244

verifying consequents to 235

arbiters, monitoring 422–424

arguments

actual 221

formal 44, 76–79, 221

local variables in 85

property 221

recursive properties and 299–301

assert_always_on_edge function 446

assert_always function 445, 449, 452–453

assert_change function 447

assert_cycle_sequence function 447

assert_decrement function 446

assert_delta function 446

assert_even_parity function 445

assert_fifo_index function 446, 452–453

assert_frame function 447

assert_handshake function 448

assert_increment function 446

assert_never_unknown_async function 444

assert_never_unknown function 445

assert_never function 445

assert_next function 448

assert_no_overflow function 446

assert_no_transition function 446

assert_no_underflow function 447

assert_odd_parity function 445

assert_one_cold function 445

assert_one_hot function 445

assert_proposition function 444

assert_quiescent_state function 447

assert_range function 445

assert_time function 448

assert_transition function 447

assert_unchange function 448 , 647

assert_width function 448

assert_win_change function 448

assert_win_unchange function 449

assert_window function 448

assert_zero_one_hot function 445

Assert class 485, 490–494

assert directive

examples 317–318

execution of 318–319

immediate assertions 13, 306, 314–315

overview 305, 349

syntax 316–317

assertion density 460

assertion directives

assert. See assert directive

assert property. See assert property directive

assume property. See assume property directive

clock flow 334–337

clock inference 337–346

compiler 438

concurrent assertions and 10

cover property. See cover property directive

enabling condition inference 346–348

functionality 219

overview 305–307

properties and 12

sequence start time and 49

summary 349–350

SVA support 13

assertion languages 7–8, 590

assertion libraries 480, 503

assertion problems

bounding unbounded property 360–364

infinite pattern after reset 354–357

intersignal dependencies 352–354

no consecutive transaction IDs 357–360

signal assertion windows 367–375

signal length 365–367

summarized 404–405

assertions

adding 414–428, 458

antecedents as 612

benefits of 1–4

binding 480–485

clocking events and 221, 342–343

concurrent. See concurrent assertions

constraints as 567, 583

control logic and 575, 590

coverage. See coverage assertions creating 13

data integrity 528, 538–540

debugging 429–435

defined 1

defining within modules 476–478

determining sufficient number of 459

dynamic hybrid engines and 594

enabling/disabling 435–441, 506

exhaustivity of formal proof 567–568

external to RTL 479–485

FIFO model checking example 620–639

FIFO testbench example 498–503

four-state operators and 609

freed signals and 597

functionality 574

general practices 414

in HDLs 7–9

identifying 527–535

immediate. See immediate assertions

implementation 529–534, 541–563

implementation coverage 534–535

implementation guidelines 463–475

implementation-specific 582

interface 527, 536–540, 581

interface coverage 528, 540–541

invariants and 575

liveness 577–580, 641

Miss Buffer block 550–563

model checking engines and 569–571

model checking usage 573, 575–582, 640

models and 590

naming 465

non-synthesizable constructs 475

overview 4–6, 503–507

partitioning 607–608

pass or fail directives 9, 309

performance impact 441–442

pragma usage 478

properties as 566, 648

protocol 527, 536–537, 582

proving 622

pruning 601–602

re-using 442–455, 505

RTL support 21

safety. See safety assertions

searching state space 568–569

simulations and 566, 572

starvation 577, 580

SVA support 9

SystemVerilog support 8–9, 21

tracking coverage 456–462

unbounded engines and 591

usage guidelines 503–506

using with other languages 475–503

verifying 429–435

writing 428–429

assertion test tools 434–435

$assertoff system task 435

$asserton system task 435–436

assert property directive

action block utility functions 311–313

assertions and 567

assume property directive and 329

constraints and 584

examples 17, 310–311

execution rules 313–314

naming conventions 469

overview 13, 20, 305, 349

syntax 307–310

assume/guarantee methodology 584, 641

assumed distributions 332–334

assume property directive

assumed distributions 332–334

constraints and 567, 583–584, 588

examples 331–332

naming conventions 469

overview 13, 20, 305, 349

reset signal and 624

stimulus generators and 428

syntax 330–331

usage overview 328–330

assumptions

concurrent 328–334

constraints and 567, 588–589

defined 588

defining 6

documenting 415

validating 424

attributes 25, 440

B

BDDs (binary decision diagrams) 591

behavioral checkers 426–427

binary decision diagrams (BDDs) 591

bind construct 480–485

$bits( ) function 222

bit-slicing technique 606

black box testing 5

Boolean expressions

and operator and 158–159

clock cycles and 42

concatenating 45–47, 54–69

concurrent assertions and 10, 24

condition expressions and 236

consequent property and 240

directives and 13

disable expressions and 264

examples 28–29

immediate assertions and 9, 24, 219, 314, 349

implementation guidelines 466

local variables and 82

or operator and 145–146

overview 23–24

property declarations and 222

repetitions and 88–125

repetitions in 105

restrictions in 25–28

sampling variables 29

sequence operations and 267

summary 125–127

X and Z values 24, 308, 315

bounded engines 592–593, 595, 649

bounded ranges 115–119

bounding unbounded properties 360–364, 396

branching sequences

and operator and 151–156

concatenating 69, 73–75

defined 130

intersect operator and 161–168

local variables in 86–87

or operator and 139–142

overview 58–61

repetitions in 91, 96–99

summarized 126

throughout operator and 188–190

within operator and 176–184

bug-hunting algorithms 570–571

C

cache_hit_d interface signal 543

cache fill transaction 511

case statement 315, 346

categories, assertion control using 438–441

chaining implication operators 257–258

check_always property 288–293

checker functions

common parameters 450–452

common syntax 450

listed 444–449

checker libraries

assertion 480, 503

creating 443, 454–455

functional groups 444–450

multiple consequent matches 255

checkers

behavioral 426–427

concurrent assertions 305

functional 5

groups of 444

HVL-based 4

immediate assertions 305

inferring logic 330

procedural 427

re-using for behaviors 443–455

See also model checking

clear counter input/output 375, 379–380

clk counter input/output 375

clk interface signal 514, 542

clock domains

FIFO example 386

implementation guidelines 467

multiclocked properties and 281

synchronizer behavior and 273

clock flow 280, 334–337, 350

clock inference 334, 337–346, 350

clocking blocks

clocks declared in 343–346

sequences and 42

static variables 25

clocking events

assertions and 342–343

assert property directive and 308

back-to-back 337

clocking blocks and 344

disable iff construct and 264

enabling condition inference 347

event control expressions and 77, 79

leading clock 334

multiclocked expressions and 273

property declarations and 221

property expressions and 268

sampled value functions 31

sampling variables 29

sequence delay and concatenation

operator 275

sequences and 45, 50

synchronizers and 273

coding guidelines (SVA) 470–475, 506–507, 608–612

comments, assertions as 416

composite sequences 130, 209

compound property 228

concatenation

and operation with sequences 156–157

back-to-back 47

Boolean expressions 45–47, 54–69, 650

branching sequences 73–75

coding guidelines 475

constant range 46

of empty sequences 99–102

fixed delay 46

non-branching 54–56

or operation with sequences 143–145

overlapping 56–58, 69, 71

property expressions 268, 271

range delays in 69, 72

sequences 12, 54–69

sequences of sequences 50, 69–76

simple 54–56, 70

summarized 126

unbounded range 47, 61–67

unbounded sequences 69, 76

zero delay 46

concurrent assertions

assert property directive 307–314, 349

Boolean expressions and 10, 24

clock cycles and 23

counter example 378–383, 406–407

directive support 13

enabling condition inference 348

FIFO example 390–402, 409–412

immediate assertions and 315

overview 305

sampling variables 29

condition expressions 236, 262

cone of logic

assertion coverage and 461

pruned logic and 602–603

state space and 641

cones of influence 4

configuration registers freeing 598

max_depth 626–628, 631–633

Configure( ) method (Engine) 488

consequent property 240, 243

consequents

antecedent matches and 247–250

enabling condition inference 347

evaluating 236

multiple matches 253–254

negated vacuous matches and 259

non-vacuous matches and 244

overlapping implication operator and 240

overlapping matches 254–255

unbounded 255–256, 262

unbounded antecedents and 253

verifying 235

constant range concatenation 46

constants, concatenating with 73–74

constraints

assumptions and 567, 588–589

defined 588

false negatives 597

functionality 574

initialization 585–587

interface 587

internal design 587

model checking usage 573, 582–589

models and 590

overconstraining 583–584, 597, 601, 641

overview 567

protocol 587

reset 585–587, 622–624

state space reduction 589

SVA support 6, 567

types of 585–589

underconstraining 584, 597, 641

control logic

assertions and 575, 590

corner cases and 572

interface assertions 581

model checking and 571, 590

corner cases

implementation coverage assertions 534

implementation guidelines 464

interface coverage assertions 529, 541

Miss Buffer assertions 561

counters

abstracting 599–600

binding assertions example 481–485

concurrent assertions 378–383, 406–407

coverage statistics 383–385, 407–408

features and description 375–376, 651

immediate assertions 377–378, 406

implementation 376–377

$countones function 40

coverage assertions

implementation 534–535

interface 528, 540–541

overview 458

coverage binning

generate statement 323–325

overview 323

task calls 325–327

coverage metrics/statistics

counter example 383–385, 407–408

cover property directive 319–328, 349

FIFO example 402–403, 412

tracking with assertions 456–463

coverage monitors 5, 428

coverage points 457, 459

covergroup construct 327

cover property directive 458

antecedents and 612

binning 323–327

examples 322–323, 383–385

naming conventions 469

overview 13, 20, 305, 319, 349, 457

syntax 319–322

using coverage data 327–328

CPU bus, FIFO example 614–616, 628–631

cycle delay operator

cover property directive 321

delay and concatenation operator and 275

overlapping concatenation 56

overview 45

parentheses support 90

D

Data Cache block

implementation assertions and 545–548

overview 523

read hits 519–520, 524–525

read misses 519–520, 524–525

write hits 519–521

write misses 519, 521

data integrity assertions 528, 538–540

data path logic

model checking and 571

procedural languages and 575

simulations and 573

data transfers (OCP) 512–517

debugging assertions 429–435

dec counter input/output 375, 379, 382–383

declarations. See property declarations

decoupled transactions 513

default clocking statement 340

default clocks 340–341, 343

delay operator. See cycle delay operator

dependencies, intersignal 352–354

design under test. See DUT

din counter input/output 375, 377, 380

DisableCount( ) method (Assert) 492

disable expressions

assertion control and 437

Boolean expressions in 24

clock flows 337

disabling properties/sequences 439

enabling conditions and 293–296

false positives and 430

implementation guidelines 467

nesting 266

overview 222, 263–266

recursive properties and 297

.triggered method and 198, 285

DisableTrigger( ) method

Assert class 493

Engine class 490

distributions, assumed 332–334

divide-by-zero 425

DoAction( ) method

Assert class 491

Engine class 488

drop_fill_u interface signal 543

DUT (design under test)

assertions and 3–4, 415–416

constraints and 584, 652

feature-specific coverage and 456

FIFO model checking example 612–620

freeing signals 597

interface assertions 581

model checking and 6, 574

standards-based languages and 8

verification approaches with 1, 6

dynamic hybrid engines 593–594

dynamic simulation 593

E

empty output signal

concurrent assertions 410

coverage data 402

defined 386

FIFO example 635–639

immediate assertions 389

verifying 393

empty repetitions

coding guidelines 475

gaps between iterations 114–115

overview 99–102

empty sequences

coding guidelines 475

concatenating 99–102

synchronizers and 273

within operator and 184–185

EnableCount( ) method (Assert) 492

EnableTrigger( ) method

Assert class 493

Engine class 490

enabling conditions

assertion directives and 306

automatic inference 346–348, 350

check_always property and 291–293

disabling conditions and 293–296

.ended method

local variables and 201–206

overview 196–197, 215

.ended sequence method

clock flows 337

disable expressions and 264

.matched method and 287

sequence end detection 286

synchronizers and 274

Engine class 485, 487–490

enumeration technique 607

equivalence checking, model checking vs. 568

$error function 311–312, 315

Event class 486, 494–497

event control expressions 79

Event data member (Event) 497

event scheduling. See scheduling

eventuality operator $ 61–67, 354

execute_region routine 16–17

execute_simulation routine 16

execute_time_slot routine 16

explicit declaration 338

expressions

Boolean. See Boolean expressions

condition 236, 262

event control 79

property. See property expressions

repetitions in 108–113

sequence. See sequence expressions

sequential regular 20

signals and 76

temporal. See temporal expressions

true property. See true property expressions

zero-time 24, 267

F

failures

coding guidelines and 473

forcing 430–433

interim 225–227

property. See property failures

sequence 53

fairness (arbiters) 422, 424

false negatives 429, 597, 600

false positives 429, 605

false property attempts 223, 653

false property expressions

evaluating 236

if...else operator and 237

vacuity and 244

$fatal function

functionality 311–313, 315

syntax 311

$fell function

disable iff clauses and 265

infinite pattern after reset 354

PSL/SVA support 20

sampled values 30, 36

syntax 33

FIFO (first in, first out)

abstracting 600

checker libraries 454–455

concurrent assertions 390–402, 409–412

coverage statistics 402–403, 412

data consistency 620–635

features and description 386–387

immediate assertions 389, 408

implementation 387–389

implementation-specific coverage and 457

model checking example 612–620

monitoring 421

multiple consequent matches 255

testbench example 498–503

fill_addr_l interface signal 543

fill_valid_l interface signal 543

Fill transaction type

Miss Buffer block 525–526, 557

overview 519, 521

finite state machines 419–420, 442

first_match operator

implicit property match 224–225

multiple consequent matches and 253

multiple matches per cycle 193–194

overriding defaults 215, 250

overview 191–192

passing local variables 194–196

fixed delay concatenation 46

follows_by property 260–261, 321

formal arguments 44, 76–79, 221

formal proof

dependencies of 573

exhaustivity of 567–568

pruning and 605

formal property checking, See model checking

formal verification

overview 571–572

simulation and 573

variance in coverage 461

format modifiers 311

four-state operators 609, 643

freeing (nondeterminism)

overview 596–598, 642

pruning and 603, 605

FSMs (finite state machines) 419–420, 442

full output signal

concurrent assertions 410

coverage data 402

defined 386

FIFO example 635–639

immediate assertions 389

verifying 393

function calls 26

G

Gen_pop class (Vera) 501

Gen_push class 500–501

generate statement

bit-slicing example 606

coverage binning 323–325

enumeration technique 607

FIFO example 398, 402

GetAssert( ) method (Engine) 490

GetCount( ) method (Assert) 492

GetFirstAssert( ) method (Engine) 489

GetName( ) method (Assert) 493

GetNextAssert( ) method (Engine) 489

GetNextEvent( ) method (Event) 496

goto operator 360–361

goto repetitions

bounded ranges 115–119, 654

empty repetitions and 114–115

followed by expressions 108–113

gaps between iterations 102–106

summarized 127

SVA support 89

unbounded ranges 122

Until condition 123

gray box testing 5, 21

H

HDLs (Hardware Description Languages) 7–9

HVL-based checkers 4

I

ideal results 569–571

identifiers, substituting 77–78

idle phase 513–514

IEEE

P1800 standard 9

standard languages and 8

SystemVerilog and 8

IEEE 1800-2005 standard 482

if...else implication operator

condition expression and 236

examples 237–240

nesting 256

overview 235–236, 262

pass/fail behavior 237

synchronizers and 279

vacuity and 244–246

ifdef directive 438

ifndef directive 438

if statement 315, 346

immediate assertions

assert directive 314–319

Boolean expressions and 9, 24, 219, 314, 349

counter example 377–378, 406

directive support 13

enabling condition inference 348

FIFO example 389, 408

overview 9, 305

simulation tick and 23

implementation assertions 529–534, 541–563

implementation coverage assertions 534–535

implementation-specific assertions 582

implication operators

chaining 257–258

if...else 235–236

nesting 256

non-overlapping. See non-overlapping

implication operators

overlapping. See overlapping implication

operators

sequence requirements 271

synchronizers and 277–280

implications

chaining 257–258

coding guidelines 473, 611–612, 643

cover property directive 321

FIFO example 633–635

follows_by property and 260–261

intersignal dependencies 353

multiple antecedent matches 247–250

multiple consequent matches 253

negated 259

nesting 256

not operator and 258–260

overlapping consequent matches 254–255

overview 261–263

passing vacuously 236

as property expressions 291

sequences vs. 246

unbounded antecedents 251–253

unbounded consequents 255–256

vacuity and 244–246

verifying behaviors 235, 246

import construct 455

Inactive region 14–15

inc counter input/output 375, 379, 381, 383

indeterminate results 569–570

infinity 62

$info function

functionality 312, 315, 331

syntax 311,  655

initial blocks 338, 341–342, 345

instantiations

assertions inside test modules 433–434

clock flows and 336

clocking blocks and 344

leading clocks 338–340

property declarations and 222

intellectual property (IP) 424, 512

interface assertions 527, 536–540

interface coverage assertions 528, 540–541

interfaces

assertions and 581

checking interactions 418–419

leading clocks 338, 341–342, 345

sequences and 42

static variables and 25

SVA support 485–487

interim failures 225–227

intersect operator

bounding eventualities 363–364

branching sequences and 161–168

FIFO example 396

flow of local variables and 210–212

non-branching sequences and 160–161

overview 131, 159–160, 213–214

signal assertion windows 373–375

throughout operator and 186–187

unbounded ranges and 166–168

within operator and 169–171

invariants

assertions checking 5, 21

functionality 575

implementing 417–418

SVA support 6

IP (intellectual property) 424, 512

$isunbounded function 40

$isunknown function 39

iterative regions 15–16

L

Language Reference Manual (LRM) 28

leading clock

concurrent assertions and 338–340

default clock and 340

defined 334

inference rules 341–342, 345

unique 281

linked lists, monitoring 421

<list_of_arguments> declaration 221

liveness assertions 577–580, 641

liveness property 20

load counter input/output 375–381

local variables

assigning values 82–84

in branching sequences 86–87

coding guidelines 470, 609–611, 643

declaring 81

disable expressions and 264

.ended method and 201–206

first_match operator and 194–196

instantiated sequences and 198–201

as loop counters 398–399

naming conventions 469

in non-branching sequences 86

Observe region 308

property instances and 221

scope 85

in sequences 44, 80–87

substituting 84–85

summarized 216–217

logical operators 43, 280–284

LRM (Language Reference Manual) 28

M

MAddr interface signal 514

Magellan tool 612

master_no_l interface signal 542

Master Interface block 522

.matched function 198

.matched sequence method

clock flows 337

disable expressions and 264, 656

sequence end detection 286–288

synchronizers and 274

mathematical functions 425

max_depth configuration register 626–628,

631–633

MCmd interface signal 514

MData interface signal 514

MDataValid interface signal 514

memory

checking 420–421

model checkers and 6

pruning 602–603

searching state space and 569

%m format specification 307, 316

Miss Buffer block

assertions 550–563

implementation assertions and 545–548

interface signals 542–543

overview 523–526

pipelines 544–545

read hits 525

read misses 524–525

storage elements 543

transaction types 525

write misses 525

mode bits 605

model checking

assertion usage 5, 573, 575–582, 640

constraint usage 567, 573, 582–589

data consistency 620–635

defined 6

environment components 574

equivalence checking vs. 568

exhaustivity of formal proof 567–568

FIFO DUT example 612–620

formal verification 571–572

ideal vs. realistic results 569–571

mathematical reasoning of 6

model checking engines 590–594

model usage 589–590

overview 565–566

pruning and 602, 605

searching state space 568–569

simulation and 572–573, 642

standards-based languages and 8

state space reduction techniques 594–608

summary 640–644

SVA coding guidelines 608–612, 643

typical process 643–644

usage environment 573–574

model checking engines

bounded 592–593, 595

depicted 574

dynamic hybrid 593–594

engine optimization 595

four-state operators and 609

invariants and 576

language and 590

liveness assertions 577–580

overview 590–594

pruning and 604

safety assertions 576–577, 579–580, 641

searching state space 568–572

types of 591–594, 641

unbounded 591, 595

models

abstracting 598–599

assertions and 590

constraints and 590

functionality 574

model checking usage 589–590

modules

defining assertions within 476–478

leading clocks 338, 341–342, 345

sequences and 42

static variables 25

monitors, coverage 5, 428

MRespAccept interface signal 514

MSBs (most significant bits) 388

MThreadID interface signal 514

multiclocked and operator 280–284

multiclocked or operator 284

multiclocked properties 272–288, 304

multiclocked sequences 272–288, 304

multiple antecedent matches 247–250, 254

multiple consequent matches 253–254

mutually recursive properties 288, 657

N

<name> declaration 220

naming conventions 468–470

NBA region 14–15

negated sequences 358–360

negated unbounded consequents 256, 263, 473

negated vacuous matches 258–259

negation operator. See "not" operator

negedge specifier 342

nesting 256, 266

new( ) method (Event) 494–495

non-branching concatenation 54–56

non-branching sequences

and operator and 148–151

defined 130

intersect operator and 160–161

or operator and 134–139

throughout operator and 187–188

within operator and 171–176

non-consecutive repetitions

bounded ranges 115–119

empty repetitions and 114–115

followed by expressions in

sequences 109–113

gaps between iterations 102–104

summarized 127

SVA support 89

syntax 106–108

unbounded ranges 121

Until condition 124

nondeterminism 596–601, 642

non-overlapping implication operator

chaining 257–258

chaining and 258

clock cycle delays and 243

cover property directive 321

cycle delays and 291

declaring 262

example 244

multiclocked and expressions 282

multiple antecedent matches 247–248

synchronizers and 274, 277–278

vacuity and 244

non-vacuous matches 245, 251–253

not operator (negation)

antecedents as assertions 612

coding guidelines 474

implications and 258–260

overview 227–230, 303

recursive properties and 296–297

vacuous matches and 245

O

Observe region

concurrent assertions 29, 308

local variables 308

overview 14–15, 18

.triggered method and 198

OCP (Open Cores Protocol)

data transfers 512–517