3.4 Sequential circuits

Sequential circuits are the backbone of digital systems, storing and processing information over time. Understanding these circuits is crucial for formal verification of hardware, ensuring correct temporal behavior. Verification techniques for sequential circuits are more complex than combinational ones due to their state-dependent nature.

Types of sequential circuits include synchronous and asynchronous, as well as level-triggered and edge-triggered. Clock signals provide timing reference for synchronous circuits, determining maximum operating frequency. Flip-flops and latches are key components, with flip-flops offering more stable behavior in synchronous systems.

Fundamentals of sequential circuits

• Sequential circuits form the backbone of digital systems storing and processing information over time
• Understanding sequential circuits crucial for formal verification of hardware ensuring correct temporal behavior
• Verification techniques for sequential circuits more complex than combinational due to state-dependent nature

Types of sequential circuits

Top images from around the web for Types of sequential circuits

• 

  Triggering of Flip Flops | Todays Circuits ~ Engineering Projects View original

  Is this image relevant?

• 

  postive edge triggered D flipflop - Theory articles - Electronics-Lab.com Community View original

  Is this image relevant?

• 

  clkTFF - Electronics-Lab.com View original

  Is this image relevant?

• 

  Triggering of Flip Flops | Todays Circuits ~ Engineering Projects View original

  Is this image relevant?

• 

  postive edge triggered D flipflop - Theory articles - Electronics-Lab.com Community View original

  Is this image relevant?

1 of 3

Top images from around the web for Types of sequential circuits

• 

  Triggering of Flip Flops | Todays Circuits ~ Engineering Projects View original

  Is this image relevant?

• 

  postive edge triggered D flipflop - Theory articles - Electronics-Lab.com Community View original

  Is this image relevant?

• 

  clkTFF - Electronics-Lab.com View original

  Is this image relevant?

• 

  Triggering of Flip Flops | Todays Circuits ~ Engineering Projects View original

  Is this image relevant?

• 

  postive edge triggered D flipflop - Theory articles - Electronics-Lab.com Community View original

  Is this image relevant?

1 of 3

• Synchronous sequential circuits operate based on clock signals ensuring coordinated state transitions
• Asynchronous sequential circuits change states in response to input changes without a global clock
• Level-triggered sequential circuits respond to signal levels (SR latch)
• Edge-triggered sequential circuits activate on clock edge transitions (D flip-flop)

Clock signals and timing

• Clock signals provide timing reference for synchronous sequential circuits
• Clock period determines maximum operating frequency of the circuit
• Positive edge-triggered circuits change state on rising clock edge
• Negative edge-triggered circuits change state on falling clock edge
• Clock-to-Q delay measures time from clock edge to output change

Flip-flops vs latches

• Latches level-sensitive devices changing state while enable signal active
• Flip-flops edge-triggered devices changing state only on clock edge
• Master-slave flip-flops use two latches to prevent unwanted state changes
• Flip-flops provide more stable and predictable behavior in synchronous systems
• Latches sometimes used in asynchronous designs or power-sensitive applications

Flip-flop architectures

D flip-flop

• D (Data) flip-flop stores input value present at D input on clock edge
• Output Q follows D input when clock transitions occur
• Widely used in registers and data storage applications
• Characteristic equation: Q(t+1) = D(t)
• Setup time specifies minimum time D must be stable before clock edge

JK flip-flop

• JK flip-flop has two inputs J (Set) and K (Reset) controlling next state
• Toggles output when both J and K inputs high
• Characteristic equation: Q(t+1) = J·Q'(t) + K'·Q(t)
• Can implement D flip-flop functionality by connecting J to D and K to D'
• Useful in counter and shift register designs

T flip-flop

• T (Toggle) flip-flop changes state when T input high on clock edge
• Maintains current state when T input low
• Characteristic equation: Q(t+1) = T·Q'(t) + T'·Q(t)
• Often used in frequency divider circuits
• Can implement using JK flip-flop with J and K inputs tied together

SR flip-flop

• SR (Set-Reset) flip-flop has two inputs S (Set) and R (Reset)
• S=1, R=0 sets output to 1; S=0, R=1 resets output to 0
• S=R=0 maintains current state; S=R=1 produces undefined behavior
• Characteristic equation: Q(t+1) = S + R'·Q(t)
• Less commonly used due to undefined state but useful in some control applications

State machines

Mealy vs Moore machines

• Mealy machines output depends on current state and inputs
• Moore machines output depends only on current state
• Mealy machines typically require fewer states than equivalent Moore machines
• Moore machines provide more stable outputs less susceptible to input glitches
• Choice between Mealy and Moore affects circuit complexity and timing characteristics

State diagrams

• Graphical representation of state machine behavior
• Circles represent states, arrows represent state transitions
• Labels on arrows indicate input conditions causing transitions
• Output values associated with states (Moore) or transitions (Mealy)
• Useful for visualizing and analyzing state machine operation

State tables

• Tabular representation of state machine behavior
• Rows represent current states, columns represent input combinations
• Entries specify next state and output for each state-input pair
• Can be directly translated into logic equations or hardware description language
• Facilitate systematic analysis and synthesis of sequential circuits

Registers and counters

Shift registers

• Store and shift data serially or in parallel
• Serial-in serial-out (SISO) shifts data one bit at a time
• Parallel-in parallel-out (PIPO) loads and outputs data simultaneously
• Bidirectional shift registers can shift left or right
• Applications include data serialization, delay lines, and pattern generation

Parallel-in serial-out registers

• Load data in parallel and output serially
• Used in parallel-to-serial conversion (multiplexing)
• Enable data transmission over single-wire interfaces
• Consist of D flip-flops with multiplexers for parallel loading
• Clock signal controls shifting of data through the register

Synchronous vs asynchronous counters

• Synchronous counters change state simultaneously on clock edge
• Asynchronous counters propagate changes through cascaded flip-flops
• Synchronous counters operate at higher speeds with predictable timing
• Asynchronous counters simpler design but limited by propagation delays
• Modulo-N counters cycle through N states before resetting (binary, BCD)

Sequential circuit analysis

Timing diagrams

• Graphical representation of signal behavior over time
• Show relationships between clock, inputs, and outputs
• Illustrate setup and hold time requirements
• Help identify timing violations and race conditions
• Essential tool for verifying correct sequential circuit operation

State transition analysis

• Examines how circuit moves between states over time
• Identifies reachable states and potential deadlock conditions
• Verifies correct implementation of desired state machine behavior
• Uses state diagrams or tables to track state sequences
• Critical for ensuring proper operation of complex sequential systems

Setup and hold times

• Setup time minimum time input must be stable before clock edge
• Hold time minimum time input must remain stable after clock edge
• Violating setup or hold times can lead to metastability
• Affected by circuit design, manufacturing process, and operating conditions
• Critical parameters for ensuring reliable operation of sequential circuits

Design considerations

Metastability issues

• Occurs when setup or hold times violated causing unstable output
• Can lead to unpredictable behavior and system failures
• Mitigated by using synchronizers or increasing clock period
• Mean time between failures (MTBF) used to quantify metastability risk
• Formal verification techniques can help identify potential metastability scenarios

Clock skew and jitter

• Clock skew difference in arrival times of clock signal at different components
• Clock jitter variations in clock period or edge timing
• Can cause setup and hold time violations leading to errors
• Managed through careful clock distribution network design
• Formal verification must account for clock uncertainties in timing analysis

Power consumption in sequential circuits

• Dynamic power consumption due to charging/discharging of capacitances
• Static power consumption from leakage currents in transistors
• Clock gating technique to reduce dynamic power by disabling unused clock domains
• Low-power design techniques include voltage scaling and power gating
• Trade-offs between power consumption, performance, and reliability

Verification challenges

State space explosion

• Number of possible states grows exponentially with circuit complexity
• Exhaustive verification becomes infeasible for large sequential circuits
• Formal methods must employ abstraction and reduction techniques
• Symbolic model checking uses efficient representations of state space
• Bounded model checking limits verification to fixed number of time steps

Temporal properties

• Specify behavior of circuit over time (safety, liveness, fairness)
• Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) commonly used
• Challenge in expressing and verifying complex temporal relationships
• Requires specialized model checking algorithms for temporal properties
• Important for verifying protocols, arbitration schemes, and control systems

Reachability analysis

• Determines set of states reachable from initial state
• Identifies unreachable states and potential design flaws
• Can uncover unintended behaviors or deadlock conditions
• Computationally expensive for large sequential circuits
• Formal methods use symbolic techniques to handle large state spaces efficiently

Formal methods for sequential circuits

Model checking techniques

• Automated verification of temporal properties against circuit model
• Symbolic model checking uses Binary Decision Diagrams (BDDs) to represent state space
• Bounded model checking uses SAT solvers to check properties up to fixed bound
• Abstraction techniques reduce complexity by simplifying circuit model
• Counterexample-guided abstraction refinement (CEGAR) iteratively improves abstractions

Theorem proving approaches

• Use logical deduction to prove correctness of sequential circuits
• Higher-order logic allows expressing complex temporal properties
• Interactive theorem provers (Coq, Isabelle) guide proof construction
• Automated theorem provers (ACL2, PVS) attempt to find proofs automatically
• Can handle infinite state spaces but require significant human expertise

Equivalence checking

• Verifies functional equivalence between two sequential circuit designs
• Used to check correctness of optimizations or design revisions
• Combinational equivalence checking compares next-state functions
• Sequential equivalence checking considers reachable states
• Induction-based techniques prove equivalence over all possible input sequences

Testing and debugging

Scan chain design

• Connects flip-flops into shift register for improved testability
• Allows direct control and observation of internal states
• Increases fault coverage and simplifies test pattern generation
• Multiplexers added to flip-flops to select between functional and test modes
• Scan-based testing standard practice in modern VLSI design

Built-in self-test (BIST)

• Integrates test pattern generation and response analysis on-chip
• Linear Feedback Shift Registers (LFSRs) generate pseudo-random test patterns
• Multiple Input Signature Registers (MISRs) compress test responses
• Enables in-field testing and reduces need for external test equipment
• Challenges include area overhead and achieving high fault coverage

Fault models for sequential circuits

• Stuck-at faults model permanent defects in logic gates
• Transition faults represent slow-to-rise or slow-to-fall defects
• Delay faults model timing violations in critical paths
• Sequential fault models consider faults affecting state elements
• Formal verification techniques can prove absence of certain fault classes

Advanced topics

Asynchronous sequential circuits

• Operate without global clock signal relying on handshaking protocols
• Potential for higher speed and lower power consumption
• Challenges in design, verification, and testing due to lack of synchronization
• Hazards and race conditions more prevalent in asynchronous designs
• Formal verification techniques adapted for asynchronous circuit models

Low-power sequential design

• Clock gating disables clock to unused circuit portions
• Multi-threshold CMOS uses transistors with different threshold voltages
• Power gating turns off power to inactive circuit blocks
• Dynamic voltage and frequency scaling adapts to workload demands
• Formal methods verify correct operation across different power modes

Radiation-hardened sequential circuits

• Designed to operate reliably in high-radiation environments (space, nuclear)
• Triple Modular Redundancy (TMR) uses voting between triplicated flip-flops
• Error-Correcting Codes (ECC) protect memory elements from bit flips
• Temporal redundancy techniques re-sample inputs to filter out transients
• Formal verification ensures correctness of fault-tolerant design techniques