7.2 Verilog

Verilog is a powerful hardware description language used in formal hardware verification. It enables engineers to model, simulate, and synthesize digital circuits at various abstraction levels, from high-level behavioral descriptions to low-level gate representations.

This section covers Verilog fundamentals, including syntax, data types, and operators. It explores modules, behavioral and structural modeling, synthesis considerations, testbench creation, and timing concepts. Advanced topics like tasks, compiler directives, and verification techniques are also discussed.

Fundamentals of Verilog

• Verilog serves as a hardware description language crucial for designing and verifying digital systems in formal hardware verification
• Enables engineers to model complex digital circuits at various abstraction levels, from high-level behavioral descriptions to low-level gate-level representations
• Provides a foundation for simulating and synthesizing hardware designs, essential for ensuring correctness before physical implementation

Syntax and structure

Top images from around the web for Syntax and structure

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL: Gate Level Modeling View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Synthesizable and Non-Synthesizable Verilog constructs View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL-Modules View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL: Gate Level Modeling View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Synthesizable and Non-Synthesizable Verilog constructs View original

  Is this image relevant?

1 of 3

Top images from around the web for Syntax and structure

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL: Gate Level Modeling View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Synthesizable and Non-Synthesizable Verilog constructs View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL-Modules View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Verilog HDL: Gate Level Modeling View original

  Is this image relevant?

• 

  ASIC-System on Chip-VLSI Design: Synthesizable and Non-Synthesizable Verilog constructs View original

  Is this image relevant?

1 of 3

• Modular design approach allows creation of reusable and hierarchical components
• Case-sensitive language with C-like syntax for familiar programming constructs
• Uses keywords to define module boundaries, behavioral blocks, and structural elements
• Supports both behavioral and structural modeling paradigms within the same design

Data types

• Wire data type represents physical connections between modules or gates
• Reg data type stores values and can be assigned in procedural blocks
• Integer and real types for arithmetic operations and loop counters
• Arrays enable grouping of related signals or storage elements
• Parameters allow for parameterizable designs and constants

Operators and expressions

• Bitwise operators (

  &

  ,

  |

  ,

  ^

  ) manipulate individual bits of operands
• Logical operators (

  &&

  ,

  ||

  ,

  !

  ) for boolean expressions and conditional statements
• Arithmetic operators (

  +

  ,

  -

  ,

  *

  ,

  /

  ) perform mathematical calculations
• Reduction operators (

  &

  ,

  |

  ,

  ^

  ) reduce vector operands to single-bit results
• Concatenation operator (

  {}

  ) combines multiple signals or bits into a single vector

Modules in Verilog

• Modules form the basic building blocks of Verilog designs, encapsulating functionality and promoting design reuse
• Enable hierarchical design methodologies, allowing complex systems to be broken down into manageable components
• Facilitate team collaboration by allowing different engineers to work on separate modules independently

Module declaration

• Begins with the

  module

  keyword followed by the module name and port list
• Defines the interface between the module and its environment or other modules
• Can include parameters for creating configurable and reusable designs
• Ends with the

  endmodule

  keyword to clearly delineate module boundaries

Port definitions

• Input ports receive data from external sources or other modules
• Output ports transmit data to external destinations or other modules
• Inout ports allow bidirectional data flow, useful for bus structures
• Port sizes can be specified using vector notation (

  [MSB:LSB]

  )
• Default port directions (input, output, inout) can be overridden during instantiation

Module instantiation

• Creates instances of previously defined modules within other modules
• Allows for hierarchical design by connecting modules to form larger systems
• Supports positional or named port connections for flexible instantiation
• Parameters can be overridden during instantiation for design customization
• Multiple instances of the same module can be created with different configurations

Behavioral modeling

• Describes the functionality of a design in terms of its behavior rather than its structure
• Allows for high-level abstraction of complex systems, focusing on functionality before implementation details
• Enables rapid prototyping and simulation of designs before committing to specific hardware structures

Always blocks

• Triggered by sensitivity list events (clock edges, signal changes)
• Used for describing sequential logic (flip-flops, registers)
• Can model combinational logic using level-sensitive always blocks
• Supports both blocking (

  =

  ) and non-blocking (

  <=

  ) assignments
• Allows for complex procedural statements (if-else, case, loops)

Initial blocks

• Execute once at the beginning of simulation
• Useful for initializing variables, setting up test conditions
• Cannot be synthesized, primarily used in testbenches or for simulation purposes
• Multiple initial blocks execute concurrently at time zero
• Can contain delay statements to schedule events at specific simulation times

Procedural assignments

• Blocking assignments (

  =

  ) update variables immediately, used for combinational logic
• Non-blocking assignments (

  <=

  ) schedule updates for the end of the time step, used for sequential logic
• Continuous assignments (

  [assign](https://www.fiveableKeyTerm:assign)

  ) model combinational logic outside procedural blocks
• Force and release statements allow overriding normal signal assignments for debugging
• Deassign statement removes a previous continuous assignment

Structural modeling

• Describes digital circuits in terms of their physical components and interconnections
• Provides a low-level representation of hardware, closely mirroring the actual circuit implementation
• Enables precise control over the hardware structure, useful for optimizing critical paths or implementing specific architectures

Gate-level primitives

• Built-in logical gates (AND, OR, NOT, XOR) for basic boolean operations
• Tri-state buffers and pull-up/pull-down resistors for bus modeling
• Multiplexers and decoders for data selection and routing
• Flip-flops and latches for sequential logic elements
• Delay specifications can be added to model gate propagation times

User-defined primitives

• Allow creation of custom logical elements not provided by built-in primitives
• Defined using truth tables to specify input-output relationships
• Can model complex combinational or sequential behavior
• Useful for creating reusable, technology-specific components
• Support specification of rise, fall, and turn-off delays

Switch-level modeling

• Models transistor-level behavior using MOS switches
• Allows for more accurate representation of CMOS circuits
• Includes built-in primitives for NMOS and PMOS transistors
• Can model bidirectional signal flow and charge storage effects
• Useful for analyzing power consumption and timing characteristics

Verilog for synthesis

• Bridges the gap between high-level design descriptions and actual hardware implementation
• Focuses on constructs and coding styles that can be efficiently translated into physical circuits
• Plays a crucial role in the formal verification process by ensuring that synthesized designs match their specifications

Synthesizable constructs

• Always blocks with edge-triggered sensitivity for sequential logic
• Combinational logic modeled using continuous assignments or level-sensitive always blocks
• Case statements for implementing multiplexers and decoders
• For loops for generating repetitive structures (unrolled during synthesis)
• Parameterized modules for creating flexible, reusable designs

Non-synthesizable constructs

• Initial blocks and time-based delays (used primarily for simulation)
• Force and release statements (not representable in hardware)
• Wait statements and event controls (not directly translatable to circuits)
• Certain system tasks and functions (e.g.,

  [$display](https://www.fiveableKeyTerm:$display)

  ,

  [$finish](https://www.fiveableKeyTerm:$finish)

  )
• Real number data types and floating-point arithmetic operations

Coding for hardware implementation

• Use synchronous design principles with a single clock domain when possible
• Avoid latches by fully specifying all conditions in combinational logic
• Implement finite state machines using one-hot or binary encoding
• Use generate statements for parameterized and repetitive structures
• Follow coding guidelines for inferring specific hardware structures (RAMs, ROMs, multipliers)

Testbenches in Verilog

• Essential component of the formal verification process, providing a controlled environment for design validation
• Enables simulation-based verification to complement formal methods
• Allows for automated testing and regression analysis of hardware designs

Stimulus generation

• Use initial blocks to set up test vectors and input sequences
• Implement clock generation using always blocks with toggle assignments
• Create random stimulus using Verilog's random number generation functions
• Use file I/O to read test vectors from external sources
• Implement bus functional models to simulate complex protocols

Response checking

• Compare design outputs against expected results using assertions
• Implement self-checking testbenches with automatic pass/fail reporting
• Use monitor tasks to observe and log signal changes during simulation
• Implement scoreboards to track and verify complex transaction sequences
• Utilize coverage analysis to ensure comprehensive testing of design features

Simulation control

• Use

  $finish

  system task to terminate simulation at specific conditions
• Implement

  $display

  and

  [$monitor](https://www.fiveableKeyTerm:$monitor)

  for printing simulation results and debugging
• Control simulation time resolution and precision using

  [timescale](https://www.fiveableKeyTerm:timescale)

  directive
• Use

  [$dumpfile](https://www.fiveableKeyTerm:$dumpfile)

  and

  [$dumpvars](https://www.fiveableKeyTerm:$dumpvars)

  for generating waveform files for analysis
• Implement save and restore functionality for long simulations using

  $save

  and

  $restart

Timing and delays

• Critical aspect of hardware design that impacts both functionality and performance
• Plays a significant role in formal verification, especially for ensuring timing correctness
• Enables accurate modeling of real-world circuit behavior in simulations

Delay models

• Inertial delay models signal changes only if the new value persists
• Transport delay passes all signal transitions, regardless of duration
• Distributed RC delay models wire capacitance and resistance effects
• Min-typ-max delays specify timing ranges for process variations
• Zero-time delays used for modeling ideal, instantaneous signal propagation

Timing constraints

• Setup and hold time requirements for flip-flops and latches
• Clock-to-q delays for sequential elements
• Maximum combinational path delays for critical timing paths
• Clock skew and jitter specifications for synchronous designs
• Asynchronous input constraints for metastability prevention

Race conditions

• Critical race occurs when multiple signals change simultaneously, affecting output
• Non-critical race results in glitches but settles to correct final value
• Delta delays used to model infinitesimal time differences between events
• Hazards (static, dynamic) cause unwanted output transitions in combinational logic
• Synchronous design techniques help mitigate race conditions in sequential circuits

Advanced Verilog concepts

• Enhances design efficiency and verification capabilities in formal hardware verification
• Provides powerful constructs for creating complex, reusable, and maintainable designs
• Enables advanced simulation and debugging techniques for thorough design validation

Tasks and functions

• Tasks encapsulate common sequences of statements, can have input and output arguments
• Functions return a single value, useful for computational operations within expressions
• Automatic tasks and functions create separate variable instances for each call
• Recursive functions allow for compact description of iterative operations
• Task and function ports can use various data types, including arrays and structures

Compiler directives

• `define creates macros for text substitution and conditional compilation
• [

  ifdef](https://www.fiveableKeyTerm:

  ifdef),

  else, 

  endif enable conditional code inclusion based on defined macros
• `include allows insertion of external Verilog source files
• `timescale sets time unit and precision for simulation

• celldefine and 

  endcelldefine mark boundaries of cell definitions for synthesis tools

System tasks and functions

• $display, 

  $write for formatted text output during simulation

• $fopen, 

  $fclose, `$fwrite for file I/O operations

• $time, 

  $realtime return current simulation time
• `[$random](https://www.fiveableKeyTerm:$random) generates pseudo-random numbers for stimulus generation

• [$readmemh](https://www.fiveableKeyTerm:$readmemh), 

  [$readmemb](https://www.fiveableKeyTerm:$readmemb) initialize memories from external files

Verilog vs VHDL

• Both languages are used in formal hardware verification, each with its own strengths
• Understanding the differences helps in choosing the appropriate language for specific design and verification tasks
• Many projects use a mix of both languages, leveraging their respective advantages

Syntax differences

• Verilog uses C-like syntax, while VHDL resembles Ada programming language
• Verilog is case-sensitive, VHDL is not (except for extended identifiers)
• Verilog uses begin/end for grouping statements, VHDL uses explicit block structures
• Verilog supports implicit port connections, VHDL requires explicit port mapping
• Verilog allows direct bit selection using array-like syntax, VHDL uses attributes

Design philosophy

• Verilog emphasizes concise, hardware-oriented descriptions
• VHDL focuses on strong typing and extensive error checking
• Verilog allows mixing of behavioral and structural descriptions more freely
• VHDL provides more robust support for complex data types and abstract modeling
• Verilog's looser type checking allows for faster initial development but can lead to subtle bugs

Industry adoption

• Verilog dominates in ASIC design, especially in North America and Asia
• VHDL remains popular in European markets and for FPGA development
• Many EDA tools support both languages, allowing mixed-language designs
• Verilog's SystemVerilog extension has gained traction for advanced verification
• VHDL's VHDL-2008 standard introduced features to compete with SystemVerilog

Verification with Verilog

• Integrates various verification methodologies to ensure correctness of hardware designs
• Combines simulation-based and formal verification techniques for comprehensive validation
• Crucial for detecting and preventing design errors before hardware implementation

Assertion-based verification

• SystemVerilog assertions (SVA) specify expected behavior of design
• Immediate assertions for checking conditions within procedural blocks
• Concurrent assertions for monitoring temporal relationships between signals
• Assertion coverage helps measure verification completeness
• Bind statements allow adding assertions to existing modules without modification

Coverage-driven verification

• Functional coverage measures which design features have been exercised
• Code coverage analyzes which lines of RTL code have been executed
• Toggle coverage tracks which signal bits have changed during simulation
• Cross coverage examines relationships between multiple coverage points
• Coverage-driven test generation automatically creates tests to reach coverage goals

Formal verification techniques

• Model checking verifies design properties against formal specifications
• Equivalence checking compares RTL against gate-level or optimized implementations
• Theorem proving uses mathematical reasoning to verify design correctness
• Bounded model checking explores design behavior up to a fixed number of time steps
• Assume-guarantee reasoning breaks complex designs into manageable verification tasks