Formal Verification

Index

Note: Page numbers followed by “f” and “t” refer to figures and tables, respectively.

A

Abstraction models, for complexity reduction, 313–320

counter, 313, 314f, 316–319

localization, 313

memory, 313, 316–319

sequence, 313, 315–316, 316f

structural, 169–170

types, 313, 313, 313

ABV, See Assertion-based verification (ABV)

Action block, 56

Algebra, See Boolean algebra

Algorithms, FV

BDD, 14, 35–39

computing, for circuit design, 37–38

model checking, 38–39

for MUX specification, 35, 35f

overview, 23

satisfiability (SAT), 17, 39–46

algorithms improvements, 45–46

Cook’s theorem, 17

Davis Logemann Loveland (DLL) algorithm, 45–46

Davis-Putnam algorithm, 43–45

model checking, 40–41

solving, 41–43

tautology, 39, 39, 39–40

ALU, See Arithmetic ...