An Introduction to

Formal Methods

Gisselquist Daniel E. Gisselquist, Ph.D.

Technology, LLC
 Lessons
Ź Welcome Day one
Motivation
1. Motivation
Basics
2. Basic Operators
Clocked and $past

k Induction
3. Clocked Operators
Bus Properties
4. Induction
Free Variables 5. Bus Properties
Abstraction
Day two
Invariants

Multiple-Clocks 6. Free Variables

Cover 7. Abstraction
Sequences 8. Invariants
Quizzes 9. Multiple-Clocks
10. Cover
11. Sequences
12. Final Thoughts

2 / 351
 Course Structure
Ź Welcome ˝ We’ll be primarily using the immediate assertion subset of the
Motivation full SystemVerilog assertion language
Basics ˝ Each lesson will be followed by an exercise
Clocked and $past There are 12 exercises
k Induction
˝ My goal is to have 50% lecture, 50% exercises
Bus Properties
˝ Leading up to building a bus arbiter
Free Variables
and testing an synchronous FIFO
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

3 / 351
Welcome

Ź Motivation
Intro

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables Motivation

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

4 / 351
 Lesson Overview
Welcome 1. Why are you here?
Motivation 2. What can I provide?
Ź Intro
3. What have I learned from formal methods?
Basics

Clocked and $past Our Objectives

k Induction

Bus Properties
˝ Get to know a little bit about each other
Free Variables ˝ Motivate further discussion
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

5 / 351
 Your expectations
Welcome What do you want to learn and get out of this course?
Motivation
Ź Intro

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

6 / 351
 From an ARM dev.
Welcome ˝ “I think the main difference between FPGA and ASIC
Motivation development is the level of verification you have to go
Ź Intro
through. Shipping a CPU or GPU to Samsung or whoever,
Basics
and then telling them once they’ve taped out that you have a
Clocked and $past

k Induction
Cat1 bug that requires a respin is going to set them back
Bus Properties
$1M per mask.
Free Variables ˝ “. . . But our main verification is still done with constrained
Abstraction random test benches written in SV.
Invariants ˝ “Overall, you are looking at 50 man years per project
Multiple-Clocks minimum for an average project size.”
Cover

Sequences

Quizzes

7 / 351
 Would not exist
Welcome “If we would not do formal verification, we would
Motivation no longer exist.”
Ź Intro

Basics
– Shahar Ariel, Head of VLSI design at Mellanox
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

8 / 351
 Pentium FDIV
Welcome One little mistake . . .
Motivation
Ź Intro

Basics

Clocked and $past . . . $475M later.

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

9 / 351
 Personal Experience
Welcome I have proven such things as,
Motivation
Ź Intro
˝ Formal bus properties (Wishbone, Avalon, AXI, etc.)
Basics ˝ Bus bridges (WB-AXI, Avalon-WB, WB-WB)
Clocked and $past ˝ Prefetches, cache controllers, memory controllers, MMU
k Induction ˝ SPI based A/D controllers
Bus Properties ˝ SDRAM
Free Variables
˝ UART, both TX and RX
Abstraction
˝ FIFO’s, signal processing flows, DSP delay
Invariants
˝ Display (VGA) Controller
Multiple-Clocks
˝ LFSR’s
Cover

Sequences
˝ Flash controllers
Quizzes ˝ Formal proof of the ZipCPU

10 / 351
 Some Examples
Welcome I’ve found bugs in things I thought were working.
Motivation
Ź Intro
1. FIFO
Basics 2. Pre-fetch and Instruction cache
Clocked and $past 3. SDRAM
k Induction 4. A peripheral timer
Bus Properties Just how hard can a timer be to get right? It’s just a
Free Variables
counter!
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

11 / 351
 Ex: FIFO
Welcome ˝ It worked in my test bench
Motivation ˝ Failed when reading and writing on the same clock while
Ź Intro
empty
Basics

Clocked and $past – Write first then read worked

k Induction
– R+W on full FIFO is okay
Bus Properties
– R+W on an empty FIFO
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

12 / 351
 Ex: FIFO
Welcome ˝ It worked in my test bench
Motivation ˝ Failed when reading and writing on the same clock while
Ź Intro
empty
Basics

Clocked and $past – Write first then read worked

k Induction
– R+W on full FIFO is okay
Bus Properties
– R+W on an empty FIFO . . . not so much
Free Variables

Abstraction ˝ My test bench didn’t check that, formal did

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

12 / 351
 Ex: Prefetch
Welcome ˝ It worked in my test bench
Motivation ˝ Ugliest bug I ever came across was in the prefetch cache
Ź Intro
It passed test-bench muster, but failed in the hardware with a
Basics
strange set of symptoms
Clocked and $past
˝ When I learned formal, it was easy to prove that this would
k Induction

Bus Properties
never happen again.
Free Variables ˝ Low logic has always been one of my goals.
Abstraction Always asking, “will it work if I get rid of this condition?”
Invariants Formal helps to answer that question for me.
Multiple-Clocks

Cover

Sequences

Quizzes

13 / 351
 Ex: SDRAM
Welcome ˝ It worked in my test bench
Motivation ˝ It passed my hardware testing
Ź Intro

Basics – Test S/W: Week+, no bugs

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

14 / 351
 Ex: SDRAM
Welcome ˝ It worked in my test bench
Motivation ˝ It passed my hardware testing
Ź Intro

Basics – Test S/W: Week+, no bugs

Clocked and $past – Formal methods found the bug
k Induction – Full proof took less than ă 30 min
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

14 / 351
 Ex: SDRAM
Welcome ˝ It worked in my test bench
Motivation ˝ It passed my hardware testing
Ź Intro
˝ Background
Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

15 / 351
 Ex: SDRAM
Welcome ˝ It worked in my test bench
Motivation ˝ It passed my hardware testing
Ź Intro
˝ Background
Basics

Clocked and $past – SDRAM’s are organized into separate banks, each having
k Induction rows and columns
Bus Properties – A row must be “activated” before it can be used.
Free Variables
– The controller must keep track of which row is activated.
Abstraction
– If a request comes in for a row that isn’t activated, the
Invariants
active row must be deactivated, and the proper row must
Multiple-Clocks
be activated.
Cover

Sequences ˝ A subtle bug in my SDRAM controller compared the active

Quizzes row address against the immediately previous (1-clock ago)
required row address, not the currently requested address.
This bug had lived in my code for years. Formal methods
caught it.

15 / 351
 Problem with Test Benches
Welcome

Motivation
Ź Intro

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
˝ Only examines a known good branch
Quizzes
˝ Cannot check for every out of bounds conditions

16 / 351
 Problem with Test Benches
Welcome ˝ Demonstrate code works
Motivation ˝ Through a normal working path
Ź Intro

Basics – or a limited number of extraneous paths

Clocked and $past
˝ Never rigorous enough to check everything
k Induction
˝ Not uniform in rigour
Bus Properties

Free Variables For the FIFO,

Abstraction

Invariants
˝ I only read when I knew it wasn’t empty
Multiple-Clocks For the Prefetch,
Cover

Sequences
˝ I never tested jumping to the last location in a cache line
Quizzes For the SDRAM,
˝ The error was so obscure, it would be hard to trigger

17 / 351
 Before Formal
Welcome This was my method before starting to work with formal.
Motivation
Ź Intro
˝ After . . .
Basics
– Proving my code with test
Clocked and $past
benches
k Induction
– Directed simulation
Bus Properties

Free Variables ˝ I was still chasing bugs in hard-

Abstraction ware
Invariants

Multiple-Clocks I still use this approach for DSP al-

Cover gorithms.
Sequences

Quizzes

18 / 351
 Design Approach
Welcome

Motivation
Ź Intro

Basics

Clocked and $past ˝ After finding the bug in my

k Induction FIFO . . . I was hooked.
Bus Properties
˝ Rebuilding everything
Free Variables
. . . now using formal
Abstraction
˝ Formal found more bugs
Invariants

Multiple-Clocks
. . . in example after example
Cover
˝ I’m hooked!
Sequences

Quizzes

19 / 351
 When to use it?
Welcome

Motivation
Ź Intro

Basics

Clocked and $past

k Induction
˝ Bus component
Bus Properties
I would not build a bus compo-
Free Variables nent without formal any more
Abstraction ˝ Multiplies
Invariants Formal struggles with multipli-
Multiple-Clocks cation
Cover

Sequences

Quizzes

20 / 351
Welcome

Motivation

Ź Basics
Basics
General Rule
Assert
Assume
BMC
Ex: Counter
Formal Verification
Sol’n

Clocked and $past

k Induction
Basics: assert and assume
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

21 / 351
 Lesson Overview
Welcome Let’s start at the beginning, and look at the very basics of formal
Motivation verification.
Basics Our Objective:
Ź Basics
General Rule ˝ To learn the basic two operators used in formal verification,
Assert
Assume
BMC
– assert()
Ex: Counter – assume()
Sol’n

Clocked and $past ˝ To understand how these affect a design from a state space
k Induction perspective
Bus Properties ˝ We’ll also look at several examples
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

22 / 351
 Basic Premise
Welcome Formal methods are built around looking for redundancies.
Motivation
˝ Basic difference between mediocre and excellent:
Basics
Ź Basics Double checking your work
General Rule ˝ Two separate and distinct fashions
Assert
Assume
BMC
– First method calculates the answer
Ex: Counter – Second method proved it was right
Sol’n

Clocked and $past ˝ Example: Division

k Induction
– 89, 321{499 “ 179
Bus Properties
– Does it? Let’s check: 179 ˚ 499 “ 89, 321 — Yes
Free Variables

Abstraction ˝ Formal methods are similar

Invariants
– Your code is the first method
Multiple-Clocks

Cover
– Formal properties describe the second
Sequences

Quizzes

23 / 351
 Basic Operators
Welcome There are really only two basic operators
Motivation
1. assume()
Basics
Ź Basics An assume(X) statement will limit the state space that the
General Rule formal verification engine examines.
Assert
Assume 2. assert()
BMC
Ex: Counter
An assert(X) statement indicates that X must be true, or the
Sol’n design will fail to prove.
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

24 / 351
 Two basic forms
Welcome always @ ( ∗ )
Motivation assert (X ) ;
Basics
Ź Basics
// Use when y o u r p r o p e r t y h a s c l o c k d e p e n d e n c i e s ,
General Rule
Assert // s u c h a s r e f e r e n c i n g an i t e m s v a l u e i n t h e p a s t
Assume always @ ( posedge clk )
BMC
Ex: Counter assert (X ) ;
Sol’n

Clocked and $past As an example,

k Induction
always @ ( ∗ )
Bus Properties
a s s e r t ( counter < 2 0 ) ;
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

25 / 351
 General Rule
Welcome

Motivation

Basics
Basics
Ź General Rule
Assert
Assume
BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

26 / 351
 Assert
Welcome

Motivation

Basics
Basics
General Rule
Ź Assert
Assume
BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Assertions define the illegal state space.

Invariants
˝ Additional assertions will increase the size of the illegal state
Multiple-Clocks
space.
Cover

Sequences

Quizzes

27 / 351
 Assume
Welcome

Motivation

Basics
Basics
General Rule
Assert
Ź Assume
BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Assumptions limit the universe of all possibilities

Invariants
˝ Additional assumptions will decrease the size of the total
Multiple-Clocks
state space
Cover
˝ Caution: One careless assumption can void the proof
Sequences

Quizzes

28 / 351
 The Careless Assumption
Welcome reg [15:0] counter ;
Motivation

Basics i n i t i a l counter = 0 ;
Basics
General Rule
always @ ( posedge clk )
Assert counter <= counter + 1 ’ b1 ;
Ź Assume
BMC
Ex: Counter always @ ( ∗ )
Sol’n begin
Clocked and $past a s s e r t ( counter <= 1 0 0 ) ;
k Induction assume ( counter <= 9 0 ) ;
Bus Properties end
Free Variables

Abstraction Question: Will counter ever reach 120?

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

29 / 351
 restrict vs assume
Welcome restrict () is very similar to assume()
Motivation

Basics
Basics
Operator Formal Verification Traditional Simulation
General Rule
Assert
restrict () Restricts search Ignored
Ź Assume assume() space Halts simulation
BMC
Ex: Counter assert() Illegal state with an error
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

30 / 351
 restrict vs assume
Welcome restrict () is very similar to assume()
Motivation

Basics
Basics
Operator Formal Verification Traditional Simulation
General Rule
Assert
restrict () Restricts search Ignored
Ź Assume assume() space Halts simulation
BMC
Ex: Counter assert() Illegal state with an error
Sol’n

Clocked and $past

k Induction ˝ restrict () : Like assume(X), it also limits the state space

Bus Properties ˝ But in a traditional simulation . . .
Free Variables

Abstraction
– restrict () is ignored
Invariants
– assume() is turned into an assert()
Multiple-Clocks

Cover

Sequences

Quizzes

30 / 351
 Bounded Model Checking
Welcome

Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables
For bounded model checking,
Abstraction

Invariants 1. Start at the initial state

Multiple-Clocks 2. Examine all possible states for N clocks
Cover
3. Try to find a way to make an assert (); fail
Sequences
4. If it’s not possible in N clocks, then pass
Quizzes

31 / 351
 No Solution
Welcome

Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Problem: initial assume(!initial_state);
Invariants
Model fails, no line number given.
Multiple-Clocks

Cover

Sequences

Quizzes

32 / 351
 No Solution
Welcome

Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Problem: assume(!reachable_state);
Invariants
Model fails, no line number given.
Multiple-Clocks

Cover

Sequences

Quizzes

33 / 351
 Further thoughts
Welcome Unlike the rest of your digital design, formal properties . . .
Motivation
˝ don’t need to meet timing
Basics
Basics ˝ don’t need to meet a minimum logic requirement
General Rule
Assert We’ll discuss this more as we go along.
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

34 / 351
 Example Bus Slave
Welcome Here’s an example of a bus slave
Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
˝ Inputs are assumed
Sequences
˝ Outputs are asserted
Quizzes

35 / 351
 Example Bus Master
Welcome Question: How would a bus master be different?
Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

36 / 351
 Example Bus Master
Welcome Question: How would a bus master be different?
Motivation

Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks The slave’s outputs are the master’s inputs

Cover
˝ assume() the inputs from the slave
Sequences
˝ assert() the outputs from the master
Quizzes

36 / 351
 Internal Bus
Welcome Question: What if both slave and master signals were part of the
Motivation same design?
Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

37 / 351
 Internal Bus
Welcome Question: What if both slave and master signals were part of the
Motivation same design?
Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks ˝ All of the wires are now internal

Cover ˝ They should therefore be assert() ed
Sequences

Quizzes

37 / 351
 Serial Port Transmitter
Welcome ˝ Whenever the serial port is idle, the output line should be
Motivation high
Basics
Basics i f ( state == IDLE )
General Rule a s s e r t ( o_uart_tx ) ;
Assert
Assume
Ź BMC ˝ Whenever the serial port is not idle, busy should be high
Ex: Counter
Sol’n i f ( state != IDLE )
Clocked and $past a s s e r t ( o_busy ) ;
k Induction else
Bus Properties a s s e r t ( ! o_busy ) ;
Free Variables

Abstraction ˝ The design can only ever be in a valid state

Invariants
a s s e r t ( ( state <= TXUL_STOP )
Multiple-Clocks
| | ( state == TXUL_IDLE ) ) ;
Cover

Sequences

Quizzes

38 / 351
 Bus Arbiter
Welcome ˝ Arbiter cannot grant both A and B access
Motivation
always @ ( ∗ )
Basics
Basics
a s s e r t ( ( ! grant_A ) | | ( ! grant_B ) ) ;
General Rule
Assert ˝ While one has access, the other must be stalled
Assume
Ź BMC
always @ ( ∗ )
Ex: Counter
Sol’n i f ( grant_A )
Clocked and $past a s s e r t ( stall_B ) ;
k Induction always @ ( ∗ )
Bus Properties i f ( grant_B )
Free Variables a s s e r t ( stall_A ) ;
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

39 / 351
 Bus Arbiter
Welcome ˝ While one is stalled, its outstanding requests must be zero
Motivation
always @ ( ∗ )
Basics
Basics
i f ( grant_A )
General Rule begin
Assert
a s s e r t ( f_nreqs_B == 0 ) ;
Assume
Ź BMC a s s e r t ( f_nacks_B == 0 ) ;
Ex: Counter a s s e r t ( f_outstanding_B == 0 ) ;
Sol’n
end
Clocked and $past

k Induction

Bus Properties I use the prefix f_ to indicate a variable that is

Free Variables
˝ Not part of the design
Abstraction
˝ But only used for Formal Verification
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

40 / 351
 Avalon bus
Welcome ˝ Avalon bus: will never issue a read and write request at the
Motivation same time
Basics
Basics always @ ( ∗ )
General Rule assume ( ( ! i_av_read ) | | ( ! i_av_write ) ) ;
Assert
Assume
Ź BMC ˝ The bus is initially idle
Ex: Counter
Sol’n initial assume ( ! i_av_read ) ;
Clocked and $past initial assume ( ! i_av_write ) ;
k Induction initial assume ( ! i_av_lock ) ;
Bus Properties initial a s s e r t ( ! o_av_readdatavalid ) ;
Free Variables initial a s s e r t ( ! o_av_writeresponsevalid ) ;
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

41 / 351
 Avalon bus
Welcome ˝ Cannot respond to both read and write in the same clock
Motivation
always @ ( ∗ )
Basics
Basics
assume ( ( ! i_av_readdatavalid )
General Rule | | ( ! i_av_writeresponsevalid ) ) ;
Assert
Assume
Ź BMC Remember ! (A&&B) is equivalent to (!A )||(! B)
Ex: Counter ˝ Cannot respond if no request is outstanding
Sol’n

Clocked and $past always @ ( ∗ )

k Induction begin
Bus Properties i f ( f_wr_outstanding == 0 )
Free Variables a s s e r t ( ! o_av_writeresponsevalid ) ;
Abstraction i f ( f_rd_outstanding == 0 )
Invariants a s s e r t ( ! o_av_readdatavalid ) ;
Multiple-Clocks end
Cover

Sequences

Quizzes

42 / 351
 Wishbone
Welcome ˝ o_STB can only be high if o_CYC is also high
Motivation
always @ ( ∗ )
Basics
Basics
i f ( o_STB ) a s s e r t ( o_CYC ) ;
General Rule
Assert ˝ Count the number of outstanding requests:
Assume
Ź BMC
assign f_outstanding = ( i_reset ) ? 0
Ex: Counter
Sol’n : f_nreqs ´ f_nacks ;
Clocked and $past

k Induction ˝ Acks can only respond to valid requests

Bus Properties
i f ( f_outstanding == 0 )
Free Variables
assume ( ! i_wb_ack ) ;
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

43 / 351
 Wishbone
Welcome ˝ Well, what if a request is being made now?
Motivation
i f ( ( f_outstanding == 0 )
Basics
Basics
&&((! o_wb_stb ) | | ( i_wb_stall ) ) )
General Rule assume ( ! i_wb_ack ) ;
Assert
Assume
Ź BMC ˝ If not within a bus request, the ACK and ERR lines must be
Ex: Counter low
Sol’n

Clocked and $past i f ( ! o_CYC )

k Induction begin
Bus Properties assume ( ! i_ACK ) ;
Free Variables assume ( ! i_ERR ) ;
Abstraction end
Invariants

Multiple-Clocks ˝ Following any reset, the bus will be idle

Cover ˝ Requests remain unchanged until accepted
Sequences

Quizzes

44 / 351
 Cache
Welcome Want a guarantee that the cache response is consistent?
Motivation
˝ A valid cache entry must ...
Basics
Basics
always @ ( posedge i_clk )
General Rule
Assert i f ( o_valid )
Assume begin
Ź BMC
// Be marked v a l i d i n t h e c a c h e
Ex: Counter
Sol’n a s s e r t ( cache_valid [ f_addr [ CW ´1: LW ] ] ) ;
Clocked and $past // Have t h e same c a c h e t a g a s a d d r e s s
k Induction a s s e r t ( f_addr [ AW ´1: LW ] ==
Bus Properties cache_tag [ f_addr [ CW ´1: LW ] ] ) ;
Free Variables // Match t h e v a l u e i n t h e c a c h e
Abstraction a s s e r t ( o_data ==
Invariants cache_data [ f_addr [ CW ´ 1 : 0 ] ) ;
Multiple-Clocks // Must be i n r e s p o n s e t o a v a l i d
Cover
// r e q u e s t
Sequences
a s s e r t ( waiting_requests != 0 ) ;
Quizzes
end

45 / 351
 Multiply
Welcome Consider a multiply
Motivation
˝ Just because an algorithm doesn’t meet timing
Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

46 / 351
 Multiply
Welcome Consider a multiply
Motivation
˝ Just because an algorithm doesn’t meet timing, or
Basics
Basics ˝ Just because it take up logic your FPGA doesn’t have
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

46 / 351
 Multiply
Welcome Consider a multiply
Motivation
˝ Just because an algorithm doesn’t meet timing, or
Basics
Basics ˝ Just because it take up logic your FPGA doesn’t have,
General Rule doesn’t mean you can’t use it now
Assert
Assume
Ź BMC
always @ ( posedge i_clk )
Ex: Counter begin
Sol’n f_answer = 0 ;
Clocked and $past f o r ( k=0; k<NA ; k=k+1)
k Induction begin
Bus Properties i f ( i_a [ k ] )
Free Variables f_answer = f_answer + ( i_b<<k ) ;
Abstraction end
Invariants

Multiple-Clocks a s s e r t ( o_result == f_answer ) ;

Cover end
Sequences

Quizzes

46 / 351
 Multiply
Welcome Let’s talk about that multiply some more . . .
Motivation
˝ The one thing formal solver’s don’t handle well is multiplies
Basics
Basics
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

47 / 351
 Multiply
Welcome Let’s talk about that multiply some more . . .
Motivation
˝ The one thing formal solver’s don’t handle well is multiplies
Basics
Basics Abstraction offers alternatives
General Rule
Assert
Assume
Ź BMC
Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

47 / 351
 Memory Management Unit
Welcome ˝ For a page result to be valid, it must match the TLB
Motivation
always @ ( ∗ )
Basics
Basics
i f ( last_page_valid )
General Rule begin
Assert
a s s e r t ( tlb_valid [ f_last_page ] ) ;
Assume
Ź BMC a s s e r t ( last_ppage ==
Ex: Counter tlb_pdata [ f_last_page ] ) ;
Sol’n
a s s e r t ( last_vpage ==
Clocked and $past
tlb_vdata [ f_last_page ] ) ;
k Induction
a s s e r t ( last_ro ==
Bus Properties
tlb_flags [ f_last_page ] [ ROFLAG ] ) ;
Free Variables
a s s e r t ( last_exe ==
Abstraction
tlb_flags [ f_last_page ] [ EXEFLG ] ) ;
Invariants a s s e r t ( r_context_word [ LGCTXT ´ 1 : 1 ]
Multiple-Clocks == tlb_cdata [ f_last_page ] ) ;
Cover end
Sequences

Quizzes

48 / 351
 SDRAM
Welcome ˝ Writing requires the right row of the right bank to be
Motivation activated
Basics
Basics always @ ( posedge i_clk )
General Rule i f ( ( f_past_valid )&&(! maintenance_mode ) )
Assert
Assume
case ( f_cmd )
Ź BMC // . . .
Ex: Counter
F_WRITE : begin
Sol’n
// R e s p o n s e t o a w r i t e r e q u e s t
Clocked and $past
a s s e r t ( f_we ) ;
k Induction
// Bank i n q u e s t i o n must be a c t i v e
Bus Properties
a s s e r t ( bank_active [ o_ram_bs ] == 3 ’ b111 ) ;
Free Variables
// A c t i v e row must be f o r t h i s a d d r e s s
Abstraction
a s s e r t ( bank_row [ o_ram_bs ]
Invariants
== f_addr [ 2 2 : 1 0 ] ) ;
Multiple-Clocks
// Must be s e l e c t i n g t h e r i g h t bank
Cover
a s s e r t ( o_ram_bs == f_addr [ 9 : 8 ] ) ;
Sequences
end
Quizzes
// . . .
49 / 351
 Ex: Counter
Welcome Let’s work through a counter as an example.
Motivation
exercise-01/ Contains two files
Basics
Basics counter.v This will be the source code for
General Rule
our demo.
Assert
Assume [Link] This is the SymbiYosys script
BMC
Ź Ex: Counter
for the demo
Sol’n
Our Objectives:
Clocked and $past

k Induction ˝ Walk through the steps in the tool-flow

Bus Properties ˝ Hands on experience with SymbiYosys
Free Variables ˝ Ensure everyone has a working version of SymbiYosys
Abstraction ˝ Find and fix a design bug
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

50 / 351
 Ex: Counter
Welcome parameter [15:0] MAX_AMOUNT = 2 2 ;
Motivation reg [15:0] counter ;
Basics
Basics
General Rule
always @ ( posedge i_clk )
Assert i f ( ( i_start_signal)&&(counter == 0 ) )
Assume counter <= MAX_AMOUNT ´1’b1 ;
BMC
Ź Ex: Counter e l s e i f ( counter != 0 )
Sol’n counter <= counter ´ 1 ’ b1 ;
Clocked and $past

k Induction always @ ( ∗ )
Bus Properties o_busy = ( counter != 0 ) ;
Free Variables

Abstraction ‘ifdef FORMAL

Invariants always @ ( ∗ )
Multiple-Clocks a s s e r t ( counter < MAX_AMOUNT ) ;
Cover ‘endif
Sequences

Quizzes

51 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc Bounded model checking mode
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc Run, using yosys-smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ] Yosys commands
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v Read file
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter Prepare the file for formal
Free Variables

Abstraction
[ files ]
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome In the file, exercise-01/[Link], you’ll find:
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule
Assert
[ engines ]
Assume
BMC smtbmc
Ź Ex: Counter
Sol’n
[ script ]
Clocked and $past
read ´formal counter . v
k Induction
# . . . o t h e r f i l e s would go h e r e
Bus Properties
prep ´top counter
Free Variables

Abstraction
[ files ] List of files to be used
Invariants counter . v
Multiple-Clocks

Cover

Sequences

Quizzes

52 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc Other modes: prove, cover, live
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20 # of Steps to examine
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices Yices theorem prover (default)
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r Other potential solvers
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all We’ll discusss this later
Invariants [ files ]
Multiple-Clocks counter . v
Cover

Sequences

Quizzes

53 / 351
 Example: SymbiYosys
Welcome Other usefull yosys commands
Motivation
[ options ]
Basics
Basics
mode bmc
General Rule depth 20
Assert
[ engines ]
Assume
BMC smtbmc yices
Ź Ex: Counter # smtbmc b o o l e c t o r
Sol’n
# smtbmc z3
Clocked and $past
[ script ]
k Induction
read ´formal counter . v
Bus Properties
# . . . o t h e r f i l e s would go h e r e
Free Variables
prep ´top counter
Abstraction
opt_merge ´share_all
Invariants [ files ]
Multiple-Clocks counter . v Full or relative pathnames go here
Cover

Sequences

Quizzes

53 / 351
 Running SymbiYosys
Welcome Run: % sby -f [Link]
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

54 / 351
 Running SymbiYosys
Welcome Run: % sby -f [Link]
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

54 / 351
 BMC Failed
Welcome Run: % sby -f [Link]
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

55 / 351
 Where Next
Welcome Look at source line 63, and fire up gtkwave
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

56 / 351
 GTKWave [Link]
Welcome Run: % gtkwave counter/engine 0/[Link]
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

57 / 351
 Examine the source
Welcome Run: % demo-rtl/counter.v
Motivation What did we do wrong?
Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

58 / 351
 Examine the source
Welcome Run: % demo-rtl/counter.v
Motivation What did we do wrong?
Basics
Basics
General Rule
Assert
Assume
BMC
Ź Ex: Counter
Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes
Did you notice the missing initial statement?

58 / 351
 Illegal Initial State
Welcome

Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ex: Counter
Ź Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Problem: No initial statement

Invariants
˝ Solver finds an invalid initial state
Multiple-Clocks
˝ Model fails
Cover

Sequences

Quizzes

59 / 351
 Exercise
Welcome Try adding in the initial statement, will it work?
Motivation

Basics
Basics
General Rule
Assert
Assume
BMC
Ex: Counter
Ź Sol’n

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

60 / 351
Welcome

Motivation

Basics
Clocked and
Ź $past
Past
$past Rule

Clocked and $past

Past Assertions
Past Valid
Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

61 / 351
 Lesson Overview
Welcome Our Objective:
Motivation
˝ To learn how to make assertions crossing time intervals
Basics

Clocked and $past – $past()

Ź Past
$past Rule ˝ Before the beginning of time
Past Assertions
Past Valid – Assumptions always hold
Examples
Ex: Busy Counter – Assertions rarely hold
k Induction
˝ How to get around this with f_past_valid
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

62 / 351
 The $past operator
Welcome ˝ $past(X) Returns the value of X one clock ago.
Motivation ˝ $past(X,N) Returns the value of X N clocks ago.
Basics ˝ Depends upon a clock
Clocked and $past
Ź Past – This is illegal
$past Rule
Past Assertions
Past Valid
always @ ( ∗ )
Examples i f (X)
Ex: Busy Counter a s s e r t ( Y == $past ( Y ) ) ;
k Induction

Bus Properties No clock is associated with the $past operator.

Free Variables – But you can do this
Abstraction

Invariants
always @ ( posedge clk )
Multiple-Clocks
i f (X)
Cover
a s s e r t ( Y == $past ( Y ) ) ;
Sequences

Quizzes

63 / 351
 $past Rule
Welcome

Motivation

Basics

Clocked and $past

Past
Ź $past Rule
Past Assertions
Past Valid
Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

64 / 351
 Past Assertions
Welcome Let’s modify our counter, by creating some additional properties:
Motivation
always @ ( ∗ )
Basics
assume ( ! i_start_signal ) ;
Clocked and $past
Past
$past Rule always @ ( posedge clk )
Ź Past Assertions
a s s e r t ( $past ( counter == 0 ) ) ;
Past Valid
Examples
Ex: Busy Counter

k Induction
˝ i_start_signal is now never true, so the counter should
Bus Properties always be zero.
Free Variables ˝ assert(counter == 0);
Abstraction This should always be true, since counter starts at zero, and
Invariants is never changed from zero.
Multiple-Clocks ˝ Will assert($past(counter == 0)); succeed?
Cover

Sequences You can find this file in exercise-02/pastassert.v

Quizzes

65 / 351
 Past Assertions
Welcome ˝ This fails
Motivation
always @ ( ∗ )
Basics
assume ( ! i_start_signal ) ;
Clocked and $past
Past
$past Rule always @ ( ∗ )
Ź Past Assertions
a s s e r t ( $past ( counter == 0 ) ) ;
Past Valid
Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

66 / 351
 Past Assertions
Welcome ˝ This succeeds
Motivation
always @ ( ∗ )
Basics
assume ( ! i_start_signal ) ;
Clocked and $past
Past
$past Rule always @ ( ∗ )
Ź Past Assertions
a s s e r t ( counter == 0 ) ;
Past Valid
Examples
Ex: Busy Counter ˝ Before time, counter is unconstrained.
k Induction ˝ The solver can make it take on any value it wants in order to
Bus Properties make things fail
Free Variables
˝ This will not show in the VCD file
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

67 / 351
 Past Assertions
Welcome Let’s try again:
Motivation
always @ ( posedge clk )
Basics
i f ( $past ( i_start_signal ) )
Clocked and $past
Past
a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
$past Rule
Ź Past Assertions This should work, right?
Past Valid
Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

68 / 351
 Past Assertions
Welcome Let’s try again:
Motivation
always @ ( posedge clk )
Basics
i f ( $past ( i_start_signal ) )
Clocked and $past
Past
a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
$past Rule
Ź Past Assertions This should work, right? No, it fails.
Past Valid
Examples
Ex: Busy Counter ˝ i_start_signal is unconstrained before time
k Induction ˝ counter is initially constrained to zero
Bus Properties ˝ If i_start_signal is one before time,
Free Variables counter will still be zero when time begins
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

68 / 351
 f past valid
Welcome We can fix this with a register I call, f_past_valid:
Motivation
reg f_past_valid ;
Basics

Clocked and $past

Past
i n i t i a l f_past_valid = 1 ’ b0 ;
$past Rule always @ ( posedge clk )
Past Assertions
f_past_valid <= 1 ’ b1 ;
Ź Past Valid
Examples
Ex: Busy Counter always @ ( posedge clk )
k Induction i f ( ( f_past_valid)&&( $past ( i_start_signal ) ) )
Bus Properties a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
Free Variables

Abstraction Will this work?

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

69 / 351
 f past valid
Welcome We can fix this with a register I call, f_past_valid:
Motivation
reg f_past_valid ;
Basics

Clocked and $past

Past
i n i t i a l f_past_valid = 1 ’ b0 ;
$past Rule always @ ( posedge clk )
Past Assertions
f_past_valid <= 1 ’ b1 ;
Ź Past Valid
Examples
Ex: Busy Counter always @ ( posedge clk )
k Induction i f ( ( f_past_valid)&&( $past ( i_start_signal ) ) )
Bus Properties a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
Free Variables

Abstraction Will this work? Almost, but not yet.

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

69 / 351
 Fixing the counter
Welcome ˝ What about the case where i_start_signal is raised while
Motivation the counter isn’t zero?
Basics
reg f_past_valid ;
Clocked and $past
Past
$past Rule i n i t i a l f_past_valid = 1 ’ b0 ;
Past Assertions
Ź Past Valid
always @ ( posedge clk )
Examples f_past_valid <= 1 ’ b1 ;
Ex: Busy Counter

k Induction always @ ( posedge clk )

Bus Properties i f ( ( f_past_valid)&&( $past ( i_start_signal ) )
Free Variables &&($past ( counter == 0 ) ) )
Abstraction a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
Invariants

Multiple-Clocks ˝ Will this work?

Cover

Sequences

Quizzes

70 / 351
 Fixing the counter
Welcome ˝ What about the case where i_start_signal is raised while
Motivation the counter isn’t zero?
Basics
reg f_past_valid ;
Clocked and $past
Past
$past Rule i n i t i a l f_past_valid = 1 ’ b0 ;
Past Assertions
Ź Past Valid
always @ ( posedge clk )
Examples f_past_valid <= 1 ’ b1 ;
Ex: Busy Counter

k Induction always @ ( posedge clk )

Bus Properties i f ( ( f_past_valid)&&( $past ( i_start_signal ) )
Free Variables &&($past ( counter == 0 ) ) )
Abstraction a s s e r t ( counter == MAX_AMOUNT ´1’b1 ) ;
Invariants

Multiple-Clocks ˝ Will this work? Yes, now it will work

Cover ˝ You’ll find lots of references to f_past_valid in my own code.
Sequences

Quizzes

70 / 351
 Examples
Welcome Let’s look at some practical examples
Motivation

Basics

Clocked and $past

Past
$past Rule
Past Assertions
Past Valid
Ź Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

71 / 351
 Reset example, #1
Welcome The rule: Every design should start in the reset state.
Motivation
i n i t i a l assume ( i_RESET ) ;
Basics

Clocked and $past

Past
always @ ( ∗ )
$past Rule i f ( ! f_past_valid )
Past Assertions
assume ( i_RESET ) ;
Past Valid
Ź Examples
Ex: Busy Counter What would be the difference between these two properties?
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

72 / 351
 Reset example, #2
Welcome The rule: On the clock following a reset, there should be no
Motivation outstanding bus requests.
Basics
always @ ( posedge clk )
Clocked and $past
Past i f ( ( f_past_valid)&&( $past ( i_RESET ) ) )
$past Rule a s s e r t ( ! o_CYC ) ;
Past Assertions
Past Valid
Ź Examples
Ex: Busy Counter

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

73 / 351
 Reset example, #2
Welcome Two times registers must have their reset value
Motivation
˝ Initially
Basics
˝ Following a reset
Clocked and $past
Past
$past Rule always @ ( posedge clk )
Past Assertions
Past Valid
i f ( ( ! f_past_valid ) | | ( $past ( i_reset ) ) )
Ź Examples begin
Ex: Busy Counter a s s e r t ( ! o_CYC ) ;
k Induction a s s e r t ( ! o_STB ) ;
Bus Properties // e t c .
Free Variables end
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

74 / 351
 Bus example
Welcome The rule: while a request is being made, the request cannot
Motivation change until it is accepted.
Basics
always @ ( posedge clk )
Clocked and $past
Past i f ( ( f_past_valid )
$past Rule &&($past ( o_STB ))&&( $past ( i_STALL ) ) )
Past Assertions
Past Valid
begin
Ź Examples a s s e r t ( o_STB ) ;
Ex: Busy Counter a s s e r t ( o_REQ == $past ( o_REQ ) ) ;
k Induction end
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

75 / 351
 Ex: Busy Counter
Welcome Many of my projects include some type of “busy counter”
Motivation
˝ Serial port logic must wait for a baud clock
Basics
Transmit characters must wait for the port to be idle
Clocked and $past
Past ˝ I2C logic needs to slow the clock down
$past Rule
Past Assertions
˝ SPI logic may also need to slow the clock down
Past Valid
Examples Objectives:
Ex: Busy
Ź Counter ˝ Gain some confidence using formal methods to prove that
k Induction alternative designs are equivalent
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

76 / 351
 Exercise: Busy Counter
Welcome Here’s the basic code. It should look familiar.
Motivation
parameter [ 1 5 : 0 ] MAX_AMOUNT = 2 2 ;
Basics

Clocked and $past

Past
reg [15:0] counter ;
$past Rule
Past Assertions
i n i t i a l counter = 0 ;
Past Valid
Examples always @ ( posedge i_clk )
Ex: Busy i f ( i_reset )
Ź Counter
counter <= 0 ;
k Induction
e l s e i f ( ( i_start_signal)&&(counter == 0 ) )
Bus Properties
counter <= MAX_AMOUNT ´1’b1 ;
Free Variables
e l s e i f ( counter != 0 )
Abstraction
counter <= counter ´ 1 ;
Invariants

Multiple-Clocks
always @ ( ∗ )
Cover
o_busy = ( counter != 0 ) ;
Sequences

Quizzes

77 / 351
 Example: Busy Counter
Welcome You can find the code in exercise-03/busyctr.v.
Motivation Exercise: Create the following properties:
Basics
1. i_start_signal may be raised at any time
Clocked and $past
Past No property needed here
$past Rule
Past Assertions
2. Once raised, assume i_start_signal will remain high until
Past Valid it is high and the counter is no longer busy.
Examples
Ex: Busy 3. o_busy will always be true while the counter is non-zero
Ź Counter
This is an assertion
k Induction
4. If the counter is non-zero, it should always be counting down
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

78 / 351
 Busy Counter, Part two
Welcome Exercise:
Motivation
1. Make o_busy a clocked register
Basics

Clocked and $past always @ ( posedge i_clk )

Past o_busy <= /∗ y o u r l o g i c g o e s h e r e ∗/ ;
$past Rule
Past Assertions
Past Valid 2. Prove that o_busy is true if and only if the counter is
Examples
Ex: Busy non-zero
Ź Counter

k Induction ˝ You can use this approach to adjust your design to meet
Bus Properties timing
Free Variables

Abstraction
– Shuffle logic from one clock to another, then
Invariants
– Prove the new design remains valid
Multiple-Clocks

Cover

Sequences

Quizzes

79 / 351
Welcome

Motivation

Basics

Clocked and $past

Ź k Induction
Lesson Overview
vs BMC
General Rule
The Trap
Examples
k Induction
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

80 / 351
 Lesson Overview
Welcome If you want to formally verify your design, BMC is insufficient
Motivation
˝ Bounded Model Checking (BMC) will only prove that your
Basics
design is correct for the first N clocks.
Clocked and $past
˝ It cannot prove that the design won’t fail on the next clock,
k Induction
Ź Lesson Overview clock N ` 1
vs BMC
General Rule
˝ This is the purpose of the induction step: proving correctness
The Trap for all time
Examples

Bus Properties Our Goals

Free Variables
˝ Be able to explain what induction is
Abstraction
˝ Be able to explain why induction is valuable
Invariants

Multiple-Clocks
˝ Know how to run induction
Cover ˝ What are the unique problems associated with induction
Sequences

Quizzes

81 / 351
 From Pre-Calc
Welcome Proof by induction has two steps:
Motivation
1. Base case: Prove for N “ 0 (or one)
Basics
2. Inductive step: Assume true for N , prove true for N ` 1.
Clocked and $past
Nÿ
´1
k Induction 1 ´ xN
n
Ź Lesson Overview Example: Prove x “
vs BMC
n“0
1´x
General Rule
The Trap
Examples
˝ For N “ 1, the sum is x0 or one
Bus Properties Nÿ
´1
1´x
Free Variables
xn “ x0 “
Abstraction
n“0
1´x
Invariants

Multiple-Clocks So this is true (for x ‰ 1).

Cover ˝ For the inductive step, we’ll
Sequences

Quizzes
– Assume true for N , then prove for N ` 1

82 / 351
 Proof, continued
Nÿ
´1
Welcome
n 1 ´ xN
Motivation Prove x “ for all N
n“0
1 ´ x
Basics

Clocked and $past ˝ Assume true for N , prove for N ` 1

N Nÿ´1 N
k Induction
Ź
ÿ 1 ´ x
Lesson Overview xn “ xN ` xn “ xN `
vs BMC
n“0 n“0
1´x
General Rule
The Trap ˝ Prove for N ` 1
Examples
N
Bus Properties ÿ
n 1 ´ x N 1 ´ xN
Free Variables x “ x `
n“0
1´x 1´x
Abstraction

Invariants xN ´ xN `1 ` 1 ´ xN 1 ´ xN `1
“ “
Multiple-Clocks
1´x 1´x
Cover

Sequences This proves the inductive case.

Quizzes ˝ Hence this is true for all N (where N ą 0 and x ‰ 1)

83 / 351
 k Induction
Welcome Suppose @n : P rns is what we wish to prove
Motivation
˝ Traditional induction
Basics

Clocked and $past – Base case: show P r0s

k Induction
Ź Lesson Overview
– Inductive case: show P rns Ñ P rn ` 1s
vs BMC
General Rule ˝ k induction
The Trap
N ´1
Examples ľ
Bus Properties
– Base case: show P rks
Free Variables
k“0
˜ ¸
Abstraction n
ľ
Invariants – k-induction step: P rks Ñ P rn ` 1s
Multiple-Clocks k“n´N `1
Cover

Sequences

Quizzes

84 / 351
 k Induction
Welcome Suppose @n : P rns is what we wish to prove
Motivation
˝ Traditional induction
Basics

Clocked and $past – Base case: show P r0s

k Induction
Ź Lesson Overview
– Inductive case: show P rns Ñ P rn ` 1s
vs BMC
General Rule ˝ k induction
The Trap
N ´1
Examples ľ
Bus Properties
– Base case: show P rks
Free Variables
k“0
This is what we did
˜ with BMC ¸
Abstraction
ľn
Invariants – k-induction step: P rks Ñ P rn ` 1s
Multiple-Clocks k“n´N `1
Cover

Sequences

Quizzes

84 / 351
 k Induction
Welcome Suppose @n : P rns is what we wish to prove
Motivation
˝ Traditional induction
Basics

Clocked and $past – Base case: show P r0s

k Induction
Ź Lesson Overview
– Inductive case: show P rns Ñ P rn ` 1s
vs BMC
General Rule ˝ k induction
The Trap
N ´1
Examples ľ
Bus Properties
– Base case: show P rks
Free Variables
k“0
˜ ¸
Abstraction n
ľ
Invariants – k-induction step: P rks Ñ P rn ` 1s
Multiple-Clocks k“n´N `1
Cover This is our next step
Sequences

Quizzes

84 / 351
 k Induction
Welcome Suppose @n : P rns is what we wish to prove
Motivation
˝ Traditional induction
Basics

Clocked and $past – Base case: show P r0s

k Induction
Ź Lesson Overview
– Inductive case: show P rns Ñ P rn ` 1s
vs BMC
General Rule ˝ k induction
The Trap
N ´1
Examples ľ
Bus Properties
– Base case: show P rks
Free Variables
k“0
˜ ¸
Abstraction n
ľ
Invariants – k-induction step: P rks Ñ P rn ` 1s
Multiple-Clocks k“n´N `1
Cover

Sequences

Quizzes Why use k induction?

84 / 351
 Induction in Verification
Welcome Formal verification uses k induction
Motivation
˝ Base case:
Basics
Assume the first N steps do not violate any assumptions, . . .
Clocked and $past

k Induction
Prove that the first N steps do not violate any assertions.
Ź Lesson Overview The is the BMC pass we’ve already done.
vs BMC
General Rule
˝ Inductive Step:
The Trap Assume N steps exist that neither violate any assumptions
Examples

Bus Properties
nor any assertions, and
Free Variables
Assume the N ` 1 step violates no assumptions, . . .
Abstraction Prove that the N ` 1 step does not violate any assertions.
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

85 / 351
 BMC vs Induction
Welcome BMC and induction are very different.
Motivation
˝ BMC, the base case
Basics

Clocked and $past

k Induction
Lesson Overview
Ź vs BMC ˝ Induction step
General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction ˝ The number of BMC time-steps steps must be more than the
Invariants
number of inductive time-steps
Multiple-Clocks
˝ Register values at the beginning of the inductive step can be
Cover
anything allowed by your assertions and assumptions
Sequences
˝ This is where the work takes place.
Quizzes

86 / 351
 General Rule
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
Ź General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants The general rule hasn’t changed:

Multiple-Clocks
˝ assume inputs,
Cover
˝ assert internal states and any outputs.
Sequences

Quizzes If you assume too much, your design will pass formal verification
and still not work.

87 / 351
 Checkers
Welcome Some assertions:
Motivation
˝ Games are played on black squares
Basics
˝ Players will never have more than 12 pieces
Clocked and $past
˝ Only legal moves are possible
k Induction
Lesson Overview ˝ Game is over when one side can no longer move
vs BMC
Ź General Rule Where might the induction engine start?
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

88 / 351
 Checkers in the Library
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
Ź General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Black’s going to move and win
Quizzes

89 / 351
 Checkers in the Library
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
Ź General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
White’s going to move and win
Quizzes

89 / 351
 Checkers in the Library
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
Ź General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Black’s going to . . . , huh?
Quizzes

89 / 351
 Checkers in the Library
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
Ź General Rule
The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Would this pass our criteria?
Quizzes

89 / 351
 Checkers and Induction
Welcome What can we learn from Checkers?
Motivation
˝ Inductive step starts in the middle of the game
Basics
Only the assumptions and asserts are used to validate the
Clocked and $past

k Induction
game
Lesson Overview ˝ All of the FF’s (variables) start in arbitrary states
vs BMC
Ź General Rule
These states are only constrained by your assumptions and
The Trap assertions.
Examples
˝ Your formal constraints are required to limit the allowable
Bus Properties

Free Variables
states
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

90 / 351
 The Trap
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule
Ź The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
˝ If your formal properties are not strict enough,
Cover
Induction may start in an illegal state
Sequences ˝ This is a common problem!
Quizzes

91 / 351
 The Solution
Welcome

Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule
Ź The Trap
Examples

Bus Properties

Free Variables

Abstraction

Invariants To make induction work, you must . . .

Multiple-Clocks

Cover
˝ assume unrealistic inputs will never happen
Sequences ˝ assert any remaining unreachable states are illegal
Quizzes ˝ Induction often requires more properties than BMC alone

92 / 351
 Examples
Welcome ˝ Let’s look at some examples
Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

93 / 351
 Another Counter
Welcome This design would pass many steps of BMC
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
Lesson Overview
always @ ( posedge clk )
vs BMC counter <= counter + 1 ’ b1 ;
General Rule
The Trap
Ź Examples always @ ( ∗ )
Bus Properties a s s e r t ( counter < 1 6 ’ d65000 ) ;
Free Variables

Abstraction
It will not pass induction.
Invariants
Can you explain why not?
Multiple-Clocks

Cover

Sequences

Quizzes

94 / 351
 Another Counter
Welcome Here’s another counter that will pass BMC, but not induction
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
Lesson Overview
always @ ( posedge clk )
vs BMC i f ( counter == 1 6 ’ d22 )
General Rule counter <= 0 ;
The Trap
Ź Examples else
Bus Properties counter <= counter + 1 ’ b1 ;
Free Variables

Abstraction
always @ ( ∗ )
Invariants
a s s e r t ( counter != 1 6 ’ d500 ) ;
Multiple-Clocks

Cover
Can you explain why not?
Sequences

Quizzes

95 / 351
 Shift Register Comparison
Welcome These shift registers will be equal during BMC, but require at
Motivation least sixteen steps to pass induction
Basics
reg [ 1 5 : 0 ] sa , sb ;
Clocked and $past
i n i t i a l sa = 0 ;
k Induction
Lesson Overview i n i t i a l sb = 0 ;
vs BMC always @ ( posedge clk )
General Rule
The Trap
Ź Examples sa <= { sa [ 1 4 : 0 ] , i_bit } ;
Bus Properties

Free Variables always @ ( posedge clk )

Abstraction

Invariants sb <= { sb [ 1 4 : 0 ] , i_bit } ;

Multiple-Clocks

Cover always @ ( ∗ )
Sequences
a s s e r t ( sa [ 1 5 ] == sb [ 1 5 ] ) ;
Quizzes
Can you explain why it would take so long?

96 / 351
 Shift Register Comparison
Welcome This design is almost identical to the last one, yet fails induction.
Motivation The key difference is the if (i_ce).
Basics
reg [ 1 5 : 0 ] sa , sb ;
Clocked and $past
i n i t i a l sa = 0 ;
k Induction
Lesson Overview i n i t i a l sb = 0 ;
vs BMC always @ ( posedge clk )
General Rule
The Trap
i f ( i_ce )
Ź Examples sa <= { sa [ 1 4 : 0 ] , i_bit } ;
Bus Properties

Free Variables always @ ( posedge clk )

Abstraction i f ( i_ce )
Invariants sb <= { sb [ 1 4 : 0 ] , i_bit } ;
Multiple-Clocks

Cover always @ ( ∗ )
Sequences
a s s e r t ( sa [ 1 5 ] == sb [ 1 5 ] ) ;
Quizzes
Can you explain why this wouldn’t pass?

97 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview Works for some designs
vs BMC
General Rule
3. assert(sa == sb);
The Trap
Ź Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview Works for some designs
vs BMC
General Rule
3. assert(sa == sb);
The Trap Best, but only works when sa and sb are visible
Ź Examples

Bus Properties
4. Insist on no more than M clocks between i_ce’s
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview Works for some designs
vs BMC
General Rule
3. assert(sa == sb);
The Trap Best, but only works when sa and sb are visible
Ź Examples

Bus Properties
4. Insist on no more than M clocks between i_ce’s
Free Variables
5. Use a different prover, under the [engines] option
Abstraction ˝ smtbmc
Invariants
˝ abc pdr
Multiple-Clocks
˝ aiger avy
Cover
˝ aiger suprove
Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview Works for some designs
vs BMC
General Rule
3. assert(sa == sb);
The Trap Best, but only works when sa and sb are visible
Ź Examples

Bus Properties
4. Insist on no more than M clocks between i_ce’s
Free Variables
5. Use a different prover, under the [engines] option
Abstraction ˝ smtbmc Inconclusive Proof (Induction fails)
Invariants
˝ abc pdr Pass
Multiple-Clocks
˝ aiger avy Pass
Cover
˝ aiger suprove Pass
Sequences

Quizzes

98 / 351
 Fixing Shift Reg
Welcome Several approaches to fixing this:
Motivation
1. assume(i_ce);
Basics
Doesn’t really test the design
Clocked and $past

k Induction
2. opt_merge ´share_all, yosys option
Lesson Overview Works for some designs
vs BMC
General Rule
3. assert(sa == sb);
The Trap Best, but only works when sa and sb are visible
Ź Examples

Bus Properties
4. Insist on no more than M clocks between i_ce’s
Free Variables
5. Use a different prover, under the [engines] option
Abstraction ˝ smtbmc Inconclusive Proof (Induction fails)
Invariants
˝ abc pdr Pass
Multiple-Clocks
˝ aiger avy Pass
Cover
˝ aiger suprove Pass
Sequences

Quizzes
Most of these options work for some designs only

98 / 351
 SymbiYosys
Welcome Here’s how we’ll change our sby file:
Motivation
[ options ]
Basics
mode prove
Clocked and $past

k Induction
Lesson Overview
[ engines ]
vs BMC smtbmc
General Rule
The Trap
Ź Examples [ script ]
Bus Properties read ´formal module . v
Free Variables
# . . . o t h e r f i l e s would go h e r e
Abstraction
prep ´top module
Invariants
opt_merge ´share_all
Multiple-Clocks

Cover
[ files ]
Sequences
. . / path´to / module . v
Quizzes

99 / 351
 SymbiYosys
Welcome Here’s how we’ll change our sby file:
Motivation
[ options ]
Basics
mode prove Use BMC and k-induction
Clocked and $past

k Induction
Lesson Overview
[ engines ]
vs BMC smtbmc
General Rule
The Trap
Ź Examples [ script ]
Bus Properties read ´formal module . v
Free Variables
# . . . o t h e r f i l e s would go h e r e
Abstraction
prep ´top module
Invariants
opt_merge ´share_all
Multiple-Clocks

Cover
[ files ]
Sequences
. . / path´to / module . v
Quizzes

99 / 351
 SymbiYosys
Welcome Here’s how we’ll change our sby file:
Motivation
[ options ]
Basics
mode prove
Clocked and $past

k Induction
Lesson Overview
[ engines ]
vs BMC smtbmc Other potential engines would go here
General Rule
The Trap
Ź Examples [ script ]
Bus Properties read ´formal module . v
Free Variables
# . . . o t h e r f i l e s would go h e r e
Abstraction
prep ´top module
Invariants
opt_merge ´share_all
Multiple-Clocks

Cover
[ files ]
Sequences
. . / path´to / module . v
Quizzes

99 / 351
 SymbiYosys
Welcome Here’s how we’ll change our sby file:
Motivation
[ options ]
Basics
mode prove
Clocked and $past

k Induction
Lesson Overview
[ engines ]
vs BMC smtbmc
General Rule
The Trap
Ź Examples [ script ]
Bus Properties read ´formal module . v
Free Variables
# . . . o t h e r f i l e s would go h e r e
Abstraction
prep ´top module
Invariants
opt_merge ´share_all Here’s where opt merge would go
Multiple-Clocks

Cover
[ files ]
Sequences
. . / path´to / module . v
Quizzes

99 / 351
 Ex: DblPipe
Welcome Exercise #4: dblpipe.v
Motivation
module dblpipe ( i_clk ,
Basics
i_ce , i_data , o_data ) ;
Clocked and $past
// . . .
k Induction
Lesson Overview
vs BMC wire a_data , b_data ;
General Rule
The Trap
Ź Examples lfsr_fib one ( i_clk , 1 ’ b0 , i_ce ,
Bus Properties i_data , a_data ) ;
Free Variables
lfsr_fib two ( i_clk , 1 ’ b0 , i_ce ,
Abstraction
i_data , b_data ) ;
Invariants

Multiple-Clocks
i n i t i a l o_data = 1 ’ b0 ;
Cover
always @ ( posedge i_clk )
Sequences
o_data <= a_data ˆ b_data ;
endmodule
Quizzes

100 / 351
 Ex: DblPipe
Welcome Exercise #4: dblpipe.v
Motivation
˝ lfsr_fib just implements a Fibonacci linear feedback shift
Basics
register,
Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties
sreg [ ( LN ´ 2 ) : 0 ] <= sreg [ ( LN ´ 1 ) : 1 ] ;
Free Variables
sreg [ ( LN ´1)] <= ( ˆ ( sreg & TAPS ) ) ˆ i_in ;
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

101 / 351
 Ex: DblPipe
Welcome Exercise #4: dblpipe.v, lfsr fib.v
Motivation
reg [ ( LN ´ 1 ) : 0 ] sreg ;
Basics

Clocked and $past

i n i t i a l sreg = INITIAL_FILL ;
k Induction
Lesson Overview
always @ ( posedge i_clk )
vs BMC i f ( i_reset )
General Rule sreg <= INITIAL_FILL ;
The Trap
Ź Examples e l s e i f ( i_ce )
Bus Properties begin // B a s i c s h i f t r e g i s t e r u p d a t e o p e r a t i o n
Free Variables
sreg [ ( LN ´ 2 ) : 0 ] <= sreg [ ( LN ´ 1 ) : 1 ] ;
Abstraction
sreg [ ( LN ´1)] <= ( ˆ ( sreg & TAPS ) ) ˆ i_in ;
Invariants
end
Multiple-Clocks

Cover
assign o_bit = sreg [ 0 ] ;
Sequences

Quizzes ˝ Both registers one and two use the exact same logic

102 / 351
 Ex: DblPipe
Welcome Exercise #4:
Motivation
˝ Using dblpipe.v
Basics

Clocked and $past – Prove that the output, o_data, is zero

k Induction
Lesson Overview
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

103 / 351
 Ex: LFSRs
Welcome Galois and Fibonacci are supposedly identical
Motivation
˝ Galois
Basics

Clocked and $past

k Induction
Lesson Overview
˝ Fibonacci
vs BMC
General Rule
The Trap
Ź Examples

Bus Properties

Free Variables
˝ Exercise #5 will be to prove these two implementations are
Abstraction
identical
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

104 / 351
 Ex: LFSRs
Welcome Exercise #5:
Motivation
˝ exercise-05/ contains files lfsr equiv.v, lfsr gal.v,
Basics
and lfsr fib.v.
Clocked and $past
˝ lfsr gal.v contains a Galois version of an LFSR
k Induction
Lesson Overview ˝ lfsr fib.v contains a Fibonacci version of the same LFSR
vs BMC
General Rule
˝ lfsr equiv.v contains an assertion that these are equivalent
The Trap
Ź Examples Prove that these are truly equivalent shift registers.
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

105 / 351
 Where is the bug?
Welcome Following an induction failure, look over the trace
Motivation

Basics

Clocked and $past

k Induction
Lesson Overview
vs BMC
General Rule If you see a problem in section . . .
The Trap
Ź Examples A You have a missing one or more assertions
Bus Properties You’ll only have this problem with induction.
Free Variables
B You have a failing assert @(posedge clk)
Abstraction
C You have a failing assert @(∗)
Invariants
These latter two indicate a potential logic failure, but they
Multiple-Clocks

Cover
could still be caused by property failures.
Sequences

Quizzes

106 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Ź Bus Properties
Ex: WB Bus
AXI
Avalon
Bus Properties
Wishbone
WB Basics
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

107 / 351
 Ex: WB Bus
Welcome We have everything we need now to write formal properties for a
Motivation bus
Basics
˝ This lesson walks through an example the Wishbone Bus
Clocked and $past

k Induction Our Objectives:

Bus Properties
Ź Ex: WB Bus ˝ Learn to apply formal methods to something imminently
AXI
Avalon
practical
Wishbone ˝ Learn to build the formal description of a bus component
WB Basics
WB Basics
˝ Help lead up to a bus arbiter component
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

108 / 351
 AXI Channels
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
Ź AXI
Avalon
Wishbone
WB Basics
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

109 / 351
 Avalon Channels
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Ź Avalon
Wishbone
WB Basics
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

110 / 351
 Wishbone Channels
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI ˝ Why use the Wishbone? It’s simpler!
Avalon
Ź Wishbone
WB Basics
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

111 / 351
 WB Signals
Welcome From the master’s perspective:
Motivation Specification name My name
Basics CYC O o wb cyc
Clocked and $past STB O o wb stb
k Induction
WE O o wb we
Bus Properties
Ex: WB Bus
ADDR O o wb addr
AXI DATA O o wb data
Avalon
Wishbone SEL O o wb sel
Ź WB Basics
STALL I i wb stall
WB Basics

Free Variables ACK I i wb ack

Abstraction DATA I i wb data
Invariants
ERR I i wb err
Multiple-Clocks

Cover

Sequences

Quizzes

112 / 351
 WB Signals
Welcome From the slave’s perspective:
Motivation Specification name My name
Basics CYC I i wb cyc
Clocked and $past STB I i wb stb
k Induction
WE I i wb we
Bus Properties
Ex: WB Bus
ADDR I i wb addr
AXI DATA I i wb data
Avalon
Wishbone SEL I i wb sel
Ź WB Basics
STALL O o wb stall
WB Basics

Free Variables ACK O o wb ack

Abstraction DATA O o wb data
Invariants
ERR O o wb err
Multiple-Clocks
To swap perspectives from master to slave . . .
Cover

Sequences ˝ Swap the port direction

Quizzes ˝ Swap the assume() statements for assert() s

113 / 351
 Single Read
Welcome CLK
Motivation
o CYC
Basics
o STB
Clocked and $past

k Induction
o WE
Bus Properties o ADDR A0

Ex: WB Bus
AXI
o DATA
Avalon i STALL
Wishbone
Ź WB Basics i ACK
WB Basics
i DATA D0
Free Variables

Abstraction ˝ STB must be low when CYC is low

Invariants
˝ If CYC goes low mid-transaction, the transaction is aborted
Multiple-Clocks
˝ While STB and STALL are active, the request cannot change
Cover
˝ One request is made for every clock with STB and !STALL
Sequences

Quizzes

114 / 351
 Single Read
Welcome CLK
Motivation
o CYC
Basics
o STB
Clocked and $past

k Induction
o WE
Bus Properties o ADDR A0

Ex: WB Bus
AXI
o DATA
Avalon i STALL
Wishbone
Ź WB Basics i ACK
WB Basics
i DATA D0
Free Variables

Abstraction ˝ One ACK response per request

Invariants
˝ No ACKs allowed when the bus is idle
Multiple-Clocks
˝ No way to stall the ACK line
Cover
˝ The bus result is in i DATA when i ACK is true
Sequences

Quizzes

115 / 351
 Three Writes
Welcome CLK
Motivation
o CYC
Basics
o STB
Clocked and $past

k Induction
o WE
Bus Properties o ADDR A1 A2 A3

Ex: WB Bus
AXI
o DATA D1 D2 D3

Avalon i STALL
Wishbone
Ź WB Basics i ACK
WB Basics
i DATA
Free Variables

Abstraction Let’s start building some formal properties

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

116 / 351
 CYC and STB
Welcome ˝ The bus starts out idle, and returns to idle after a reset
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( ! f_past_valid ) | | ( $past ( i_reset ) ) )
Clocked and $past
begin
k Induction
assume ( ! i_wb_ack ) ;
Bus Properties
Ex: WB Bus
assume ( ! i_wb_err ) ;
AXI //
Avalon a s s e r t ( ! o_wb_cyc ) ;
Wishbone
Ź WB Basics a s s e r t ( ! o_wb_stb ) ;
WB Basics end
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

117 / 351
 CYC and STB
Welcome ˝ The bus starts out idle, and returns to idle after a reset
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( ! f_past_valid ) | | ( $past ( i_reset ) ) )
Clocked and $past
begin
k Induction
assume ( ! i_wb_ack ) ;
Bus Properties
Ex: WB Bus
assume ( ! i_wb_err ) ;
AXI //
Avalon a s s e r t ( ! o_wb_cyc ) ;
Wishbone
Ź WB Basics a s s e r t ( ! o_wb_stb ) ;
WB Basics end
Free Variables

Abstraction ˝ STB is low whenever CYC is low

Invariants
always @ ( ∗ )
Multiple-Clocks
i f ( ! o_wb_cyc )
Cover
a s s e r t ( ! o_wb_stb ) ;
Sequences

Quizzes

117 / 351
 The Master Waits
Welcome ˝ While STB and STALL are active, the request doesn’t change
Motivation
a s s i g n f_request = { o_stb , o_we , o_addr ,
Basics
o_data } ;
Clocked and $past
always @ ( posedge clk )
k Induction
i f ( $past ( o_wb_stb)&&( $past ( i_wb_stall ) ) )
Bus Properties
Ex: WB Bus
a s s e r t ( f_request == $past ( f_request ) ) ;
AXI
Avalon ˝ Did we get it?
Wishbone
Ź WB Basics
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

118 / 351
 The Master Waits
Welcome ˝ While STB and STALL are active, the request doesn’t change
Motivation
a s s i g n f_request = { o_stb , o_we , o_addr ,
Basics
o_data } ;
Clocked and $past
always @ ( posedge clk )
k Induction
i f ( $past ( o_wb_stb)&&( $past ( i_wb_stall ) ) )
Bus Properties
Ex: WB Bus
a s s e r t ( f_request == $past ( f_request ) ) ;
AXI
Avalon ˝ Did we get it? Well, not quite
Wishbone
Ź WB Basics o_data is a don’t care for any read request
WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

118 / 351
 The Master Waits
Welcome ˝ While STB and STALL are active, the request doesn’t change
Motivation
a s s i g n f_rd_request = { o_stb , o_we , o_addr } ;
Basics
a s s i g n f_wr_request = { f_rd_request , o_data } ;
Clocked and $past

k Induction
always @ ( posedge clk )
Bus Properties
Ex: WB Bus
i f ( ( f_past_valid )
AXI &&($past ( o_wb_stb ))&&( $past ( i_wb_stall ) ) )
Avalon begin
Wishbone
Ź WB Basics // F i r s t , f o r r e a d s ´´o d a t a i s a don ’ t c a r e
WB Basics i f ( $past ( ! i_wb_we ) )
Free Variables a s s e r t ( f_rd_request == $past ( f_rd_request ) ) ;
Abstraction // Second , f o r w r i t e s ´´o d a t a must n o t c h a n ge
Invariants i f ( $past ( i_wb_we ) )
Multiple-Clocks a s s e r t ( f_wr_request == $past ( f_wr_request ) ) ;
Cover end
Sequences

Quizzes

119 / 351
 CYC and STB
Welcome ˝ No acknowledgements without a request
Motivation ˝ No errors without a request
Basics ˝ Following any error, the bus cycle ends
Clocked and $past ˝ A bus cycle can be terminated early
k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

120 / 351
 Bus example
Welcome The rule: the slave (external) cannot stall the master more than
Motivation F_OPT_MAXSTALL counts:
Basics

Clocked and $past

i n i t i a l f_stall_count = 0 ;
always @ ( posedge i_clk )
k Induction
i f ( ( i_reset ) | | ( ! o_CYC ) | | ( ( o_STB )&&(! i_STALL ) ) )
Bus Properties
Ex: WB Bus f_stall_count <= 0 ;
AXI e l s e i f ( o_STB )
Avalon
Wishbone
f_stall_count <= f_stall_count + 1 ’ b1 ;
WB Basics
Ź WB Basics always @ ( posedge i_clk )
Free Variables i f ( o_CYC )
Abstraction assume ( f_stall_count < F_OPT_MAXSTALL ) ;
Invariants

Multiple-Clocks This solves the i_ce problem, this time with the i_STALL signal
Cover

Sequences

Quizzes

121 / 351
 Bus example
Welcome The rule: the slave can only respond to requests
Motivation
i n i t i a l f_nreqs = 0 ;
Basics
always @ ( posedge clk )
Clocked and $past
i f ( ( i_reset ) | | ( ! i_CYC ) )
k Induction
f_nreqs <= 1 ’ b0 ;
Bus Properties
Ex: WB Bus
e l s e i f ( ( i_STB )&&(! o_STALL ) )
AXI f_nreqs <= f_nreqs + 1 ’ b1 ;
Avalon // S i m i l a r c o u n t e r f o r a c k n o w l e d g e m e n t s
Wishbone
WB Basics always @ ( ∗ )
Ź WB Basics i f ( f_nreqs == f_nacks )
Free Variables a s s e r t ( ! o_ACK ) ;
Abstraction

Invariants The logic above almost works. Can any one spot the problems?
Multiple-Clocks

Cover

Sequences

Quizzes

122 / 351
 Two Exercises
Welcome Let’s build up to proving a WB arbiter
Motivation
˝ Let’s prove (BMC + k-Induction) . . .
Basics

Clocked and $past 1. Exercise #6: A simple arbiter

k Induction exercise-06/reqarb.v
Bus Properties 2. Exercise #7: Then a Wishbone bus arbiter
Ex: WB Bus
AXI exercise-07/wbpriarbiter.v
Avalon
Wishbone ˝ Given a set of bus properties: fwb slave.v
WB Basics
Ź WB Basics

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

123 / 351
 Simple Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics
The basics
Free Variables ˝ *_req requests a transaction
Abstraction ˝ *_data, the contents of the transaction
Invariants
˝ *_busy, true if the source must wait
Multiple-Clocks

Cover

Sequences

Quizzes

124 / 351
 Simple Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics ˝ If (∗_req)&&(!∗_busy),
Free Variables
the request is accepted
Abstraction
˝ If (∗_req)&&(∗_busy),
Invariants
the request may not change, except on reset
Multiple-Clocks

Cover

Sequences

Quizzes

125 / 351
 Simple Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics
To prove:
Free Variables ˝ No data will be lost, no requests will be dropped
Abstraction Assume all requests remain stable until accepted
Invariants
˝ Only one source ever gets access at a time
Multiple-Clocks
Assert one busy line is always high
Cover
˝ Therefore, all requests go through . . . eventually
Sequences

Quizzes

126 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction Shall we try this with Wishbone?

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

127 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction This request side is almost identical

Invariants
˝ If (STB)&&(!STALL)
Multiple-Clocks
the request is accepted
Cover
˝ If (STB)&&(STALL)
Sequences

Quizzes
the request must not change

128 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction The difference is the acknowledgements

Invariants
˝ The arbiter cannot change during an active transaction
Multiple-Clocks
˝ All requests get responses
Cover
˝ No response can be returned without a request
Sequences

Quizzes

129 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction Now, prove that exercise-07/wbpriarbiter.v works.

Invariants
˝ Use both BMC and k-induction (move prove)
Multiple-Clocks
˝ You’ll need to build fwb master.v properties
Cover

Sequences

Quizzes

130 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction The fwb slave.v properties will

Invariants
˝ Assume a behaving master
Multiple-Clocks
˝ Assert a behaving slave
Cover

Sequences

Quizzes

131 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction You’ll write the fwb master.v properties

Invariants
˝ Swapping inputs with outputs
Multiple-Clocks

Cover – Port names need not change

Sequences
˝ Swapping assumptions with assertions
Quizzes

132 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction The magic is in how the files are connected

Invariants
˝ If one interface is connected, both master and slave. . .
Multiple-Clocks

Cover – Should see the same number of requests

Sequences – Should see the same number of acknowledgements
Quizzes

133 / 351
 WB Arbiter
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction The magic is in how the files are connected

Invariants
˝ If one interface is connected, the other . . .
Multiple-Clocks

Cover – Should not have made any successful requests

Sequences – Should not have received any acknowledgements
Quizzes

134 / 351
 File Structure
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables
˝ Traditional test-bench file structure
Abstraction

Invariants
˝ Doesn’t work with yosys formal
Multiple-Clocks
˝ Why not?
Cover

Sequences

Quizzes

135 / 351
 Single File
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables
˝ Formal Properties can be placed at the bottom
Abstraction
˝ This works well for testing some modules
Invariants

Multiple-Clocks
˝ What’s the limitation?
Cover

Sequences

Quizzes

136 / 351
 Multiple Files
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics
˝ Design with multiple files
Free Variables
˝ They were each formally correct
Abstraction ˝ Problems?
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

137 / 351
 Multiple Files
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics
˝ Design with multiple files
Free Variables
˝ They were each formally correct
Abstraction ˝ Problems? Yes! In induction
Invariants ˝ State variables needed to be formally synchronized (assert() )
Multiple-Clocks

Cover

Sequences

Quizzes

137 / 351
 Multiple Files
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties
Ex: WB Bus
AXI
Avalon
Wishbone
WB Basics
Ź WB Basics

Free Variables

Abstraction

Invariants
Proving properties for many components together can quickly
Multiple-Clocks get out of hand!
Cover

Sequences

Quizzes

138 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Ź Free Variables
Lesson Overview
Formal
Free Variables
Memory
So what?
Rule
Discussion

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

139 / 351
 Lesson Overview
Welcome When dealing with memory, ...
Motivation
˝ Testing the entire memory is not required
Basics
˝ Testing an arbitrary value is
Clocked and $past

k Induction It’s time to discuss (∗ anyconst ∗) and (∗ anyseq ∗)

Bus Properties Objectives
Free Variables
Ź Lesson Overview ˝ Understand what a free variable is
Formal
Memory
˝ Understand how (∗ anyconst ∗) and (∗ anyseq ∗) can be
So what? used to create free variables
Rule
Discussion ˝ Learn how you can use free variables to validate memory and
Abstraction memory interfaces
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

140 / 351
 any*
Welcome ˝ (∗ anyconst ∗)
Motivation
( ∗ anyconst ∗ ) wire [ N ´ 1 : 0 ] cval ;
Basics

Clocked and $past

k Induction – Can be anything

Bus Properties – Defined at the beginning of time
Free Variables – Never changed
Lesson Overview
Ź Formal
Memory ˝ (∗ anyseq ∗)
So what?
Rule ( ∗ anyseq ∗ ) wire [ N ´ 1 : 0 ] sval ;
Discussion

Abstraction

Invariants – Can change from one timestep to the next

Multiple-Clocks
Both can still be constrained via assume() statements
Cover

Sequences

Quizzes

141 / 351
 Memory
Welcome How might you build a memory with this?
Motivation
( ∗ anyconst ∗ ) w i r e [ AW ´ 1 : 0 ] f_const_addr ;
Basics
reg [ AW ´ 1 : 0 ] f_mem_value ;
Clocked and $past

k Induction

Bus Properties
// Han d l e w r i t e s
Free Variables
always @ ( posedge i_clk )
Lesson Overview i f ( ( i_stb)&&(i_we)&&(i_addr == f_const_addr ) )
Formal
f_mem_value <= i_data ;
Ź Memory
So what?
Rule // Han d l e r e a d s
Discussion
always @ ( posedge i_clk )
Abstraction
i f ( ( f_past_valid)&&( $past ( i_stb ))&&(! $past ( i_we ) )
Invariants
&&($past ( i_addr == f_const_addr ) ) )
Multiple-Clocks
a s s e r t ( o_data == f_mem_value ) ;
Cover

Sequences

Quizzes

142 / 351
 So what?
Welcome Consider the specification of a prefetch
Motivation
˝ The contract
Basics

Clocked and $past ( ∗ anyconst ∗ ) wire [31:0] f_const_data ;

k Induction

Bus Properties always @ ( posedge i_clk )

Free Variables i f ( ( o_valid)&&(o_pc == f_const_addr ) )
Lesson Overview a s s e r t ( o_insn == f_const_data ) ;
Formal
Memory
Ź So what? ˝ You’ll also need to assume a bus input
Rule
Discussion always @ ( posedge i_clk )
Abstraction i f ( ( i_ack)&&(ackd_address == f_const_addr ) )
Invariants assume ( i_data == f_const_data ) ;
Multiple-Clocks

Cover

Sequences

Quizzes

143 / 351
 Rule of Free Variables
Welcome How would our general rule apply here?
Motivation
˝ Assume inputs, assert internal state and outputs
Basics
˝ You could have written
Clocked and $past

k Induction input w i r e i_value ;

Bus Properties

Free Variables always @ ( posedge i_clk )

Lesson Overview
assume ( i_value == $past ( i_value ) ) ;
Formal
Memory
So what? for the same effect as (∗ anyconst ∗)
Ź Rule
Discussion ˝ Both (∗ anyconst ∗) and (∗ anyseq ∗) act like inputs
Abstraction ˝ assume() them therefore, and not assert()
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

144 / 351
 Ex: Flash Controller
Welcome This works for a flash (or other ROM) controller too:
Motivation
( ∗ anyconst ∗ ) w i r e [ AW ´ 1 : 0 ] f_addr ;
Basics
( ∗ anyconst ∗ ) wire [ 3 1 : 0 ] f_data ;
Clocked and $past

k Induction
always @ ( ∗ )
Bus Properties
i f ( ( o_wb_ack)&&(f_request_addr == f_addr ) )
Free Variables
Lesson Overview
a s s e r t ( o_wb_data == f_data ) ;
Formal
Memory Don’t forget the corollary assumptions!
So what?
Ź Rule
always @ ( ∗ )
Discussion
i f ( f_request_addr == f_addr )
Abstraction
assume ( i_spi_data
Invariants
== f_data [ controller_state ] ) ;
Multiple-Clocks

Cover
. . . or something similar
Sequences

Quizzes

145 / 351
 Ex: Serial Port
Welcome You can use this to build a serial port transmitter
Motivation
( ∗ anyseq ∗ ) w i r e f_tx_start ;
Basics
( ∗ anyseq ∗ ) w i r e [ 7 : 0 ] f_tx_data ;
Clocked and $past
always @ ( ∗ )
k Induction
i f ( f_tx_busy )
Bus Properties
assume ( ! f_tx_start ) ;
Free Variables
Lesson Overview
Formal always @ ( posedge f_txclk )
Memory i f ( f_tx_busy )
So what?
Ź Rule
assume ( f_tx_data == $past ( f_tx_data ) ) ;
Discussion

Abstraction You can then

Invariants
˝ Tie assertions to partially received data
Multiple-Clocks
˝ . . . and pass induction
Cover

Sequences

Quizzes

146 / 351
 Discussion
Welcome How would you use free variables to verify a cache
Motivation implementation?
Basics

Clocked and $past

k Induction

Bus Properties

Free Variables
Lesson Overview
Formal
Memory
So what?
Rule
Ź Discussion

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

147 / 351
 Discussion
Welcome How would you use free variables to verify a cache
Motivation implementation?
Basics

Clocked and $past Hint: you only need three properties for the cache contract
k Induction

Bus Properties

Free Variables
Lesson Overview
Formal
Memory
So what?
Rule
Ź Discussion

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

147 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Ź Abstraction Abstraction
Lesson Overview
Formal
Proof
Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

148 / 351
 Lesson Overview
Welcome ˝ Proving simple modules is easy.
Motivation ˝ What about large and complex ones?
Basics

Clocked and $past It’s time to discus abstraction.

k Induction Objectives
Bus Properties
˝ Understand what abstraction is
Free Variables
˝ Gain confidence in the idea of abstraction
Abstraction
Ź Lesson Overview ˝ Understand how to reduce a design via abstraction
Formal
Proof
Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

149 / 351
 Abstraction Formally
Welcome Formally, if
Motivation

Basics AÑC
Clocked and $past

k Induction then we can also say that

Bus Properties

Free Variables pABq Ñ C

Abstraction
Lesson Overview
Ź Formal
Proof
Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

150 / 351
 Formal Proof
Welcome Shall we go over the proof?
Motivation

Basics AÑC ñ A _ C “ True

Clocked and $past
True or anything is still true, so
k Induction

Bus Properties
p A _ Cq _ B
Free Variables Rearranging terms
Abstraction
Lesson Overview
A_ B_C
Formal
pABq _ C
Ź Proof
Pictures Expressing as an implication
Examples
Exercise pABq Ñ C
Invariants

Multiple-Clocks Q.E.D.!
Cover

Sequences

Quizzes

151 / 351
 So what?
Welcome With every additional module,
Motivation
˝ Formal verification becomes more difficult
Basics
˝ Complexity increases exponentially
Clocked and $past
˝ You only have so many hours and dollars
k Induction

Bus Properties On the other hand,

Free Variables

Abstraction
˝ Anything you can simplify by abstraction . . .
Lesson Overview ˝ is one less thing you need to prove
Formal
Ź Proof
Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

152 / 351
 In Pictures
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Ź Pictures
Examples
Suppose your state space looked like this
Exercise

Invariants ˝ It takes many transitions required to get to interesting states

Multiple-Clocks

Cover

Sequences

Quizzes

153 / 351
 In Pictures
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Ź Pictures
Examples
Suppose we added to this design . . .
Exercise

Invariants ˝ Some additional states, and

Multiple-Clocks ˝ Additional transitions
Cover

Sequences
The real states and transitions must still remain
Quizzes

154 / 351
 In Pictures
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Ź Pictures
Examples
If this new design still passes, then . . .
Exercise

Invariants ˝ Since the original design is a subset . . .

Multiple-Clocks ˝ The original design must also still pass
Cover

Sequences
If done well, the new design will require less effort to prove
Quizzes

155 / 351
 A CPU
Welcome Where would you start?
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Ź Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

156 / 351
 A CPU
Welcome Where would you start?
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Ź Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover At the interfaces!

Sequences

Quizzes

156 / 351
 Prefetch
Welcome Let’s consider a prefetch module as an example.
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables
If you do this right,
Abstraction ˝ Any internally consistent Prefetch,
Lesson Overview
Formal ˝ that properly responds to the CPU, and
Proof ˝ interacts properly with the bus,
Ź Pictures
Examples ˝ must work!
Exercise

Invariants
Care to try a different prefetch approach?
Multiple-Clocks

Cover

Sequences

Quizzes

157 / 351
 Prefetch
Welcome Suppose the prefetch was just a shell
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables
It would still interact properly with
Abstraction ˝ The bus, and
Lesson Overview
Formal ˝ The CPU
Proof ˝ It just might not return values from the bus to the CPU
Ź Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

158 / 351
 Prefetch
Welcome Suppose the prefetch was just a shell
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables
If the CPU still acted “correctly”
Abstraction ˝ With either the right, or the wrong instructions, then
Lesson Overview
Formal ˝ The CPU must act correctly with the right instructions
Proof
Ź Pictures
Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

159 / 351
 Examples
Welcome Consider these statements:
Motivation
˝
Basics

Clocked and $past

k Induction
If
Bus Properties
And
Free Variables Then
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ Prefetch is bus master, interfaces w/CPU
Basics

Clocked and $past

k Induction
If (Prefetch responds to CPU insn requests)
Bus Properties
And (Prefetch produces the right instructions)
Free Variables Then (The prefetch works within the design)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ The CPU is just a wishbone master within a design
Basics

Clocked and $past

k Induction
If (The CPU is valid bus master)
Bus Properties
And (CPU properly executes instructions)
Free Variables Then (CPU works within a design)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ The ALU must return a calculated number
Basics

Clocked and $past

k Induction
If (ALU returns a value when requested)
Bus Properties
And (It is the right value)
Free Variables Then (The ALU works within the design)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ A flash device responds in 8-80 clocks
Basics

Clocked and $past

k Induction
If (Bus master reads/responds to a request)
Bus Properties
And (The response comes back in 8-80 clocks)
Free Variables Then (The CPU can interact with a flash memory)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ The divide must return a calculated number
Basics

Clocked and $past

k Induction
If (Divide returns a value when requested)
Bus Properties
And (It is the right value)
Free Variables Then (The divide works within the design)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Examples
Welcome Consider these statements:
Motivation
˝ Formal solvers break down when applied to multiplies
Basics

Clocked and $past

k Induction
If (Multiply unit returns an answer N clocks later)
Bus Properties
And (It is the right value)
Free Variables Then (The multiply works within the design)
Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

160 / 351
 Abstracted CPU components
Welcome Looking at the CPU again,
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover
˝ Replace all the components with abstract shells
Sequences
˝ . . . shells that might produce the same answers
Quizzes

161 / 351
 Back to the Counter
Welcome Let’s consider a fractional counter:
Motivation
reg [ 3 1 : 0 ] r_count ;
Basics
i n i t i a l r_count = 0 ;
Clocked and $past
i n i t i a l o_pps = 0;
k Induction
always @ ( posedge i_clk )
Bus Properties
{ o_pps , r_count } <= r_count + 3 2 ’ d43 ;
Free Variables

Abstraction The problem with this counter

Lesson Overview
Formal
Proof
˝ It will take 100 ˆ 106 clocks to roll over and set o_pps
Pictures ˝ Formally checking 100 ˆ 106 clocks is prohibitive
Ź Examples
Exercise We’ll need a better way, or we’ll never deal with this
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

162 / 351
 Back to the Counter
Welcome How might we build an abstract counter?
Motivation
˝ First, create an arbitrary counter increment
Basics

Clocked and $past ( ∗ anyseq ∗ ) w i r e [ 3 1 : 0 ] increment ;

k Induction a s s i g n rollover = ´ r_count ;
Bus Properties always @ ( ∗ )
Free Variables begin
Abstraction assume ( increment > 0 ) ;
Lesson Overview assume ( increment < { 2 ’ h1 , 3 0 ’ h0 } ) ;
Formal
Proof
i f ( rollover < 3 2 ’ d43 )
Pictures assume ( increment == 3 2 ’ d43 ) ;
Ź Examples
else
Exercise
assume ( increment < rollover ) ;
Invariants
end
Multiple-Clocks

Cover

Sequences The correct increment, 32’d43, must be a possibility

Quizzes

163 / 351
 Back to the Counter
Welcome We can now increment our counter by this arbitrary increment
Motivation
always @ ( posedge i_clk )
Basics
{ o_pps , r_count } <= r_count + increment ;
Clocked and $past

k Induction
Will this work?
Bus Properties

Free Variables ˝ Let’s try this to see!

Abstraction
Lesson Overview
always @ ( posedge i_clk )
Formal i f ( f_past_valid )
Proof a s s e r t ( r_count != $past ( r_count ) ) ;
Pictures
Ź Examples
Exercise always @ ( posedge i_clk )
Invariants i f ( ( f_past_valid)&&(r_count < $past ( r_count ) ) )
Multiple-Clocks a s s e r t ( o_pps ) ;
Cover

Sequences

Quizzes

164 / 351
 Other Possibilities
Welcome How else might you use this?
Motivation
˝ Bypassing the runup for an external peripheral
Basics
˝ Testing a real-time clock or date
Clocked and $past

k Induction Or . . . how about that CPU?

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Pictures
Ź Examples
Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

165 / 351
 Exercise
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables Let’s modify this abstract counter

Abstraction
Lesson Overview ˝ Increment by one, rather than fractionally
Formal
Proof Exercise Objectives:
Pictures
Examples
Ź Exercise
˝ Prove a design works both with and without abstraction
Invariants
˝ Gain some confidence using abstraction
Multiple-Clocks

Cover

Sequences

Quizzes

166 / 351
 Exercise #8
Welcome Your task:
Motivation
˝ Rebuild the counter
Basics
˝ Make it increment by one
Clocked and $past
˝ Build it so that . . .
k Induction

Bus Properties always @ ( ∗ )

Free Variables a s s e r t ( o_carry == ( r_count == 0 ) ) ;
Abstraction
Lesson Overview
Formal
// and
Proof
Pictures always @ ( posedge i_clk )
Examples
Ź Exercise i f ( ( f_past_valid )&&(! $past (&r_count ) ) )
Invariants a s s e r t ( ! o_carry ) ;
Multiple-Clocks

Cover
˝ Prove that this abstracted counter works
Sequences

Quizzes

167 / 351
 Exercise #8
Welcome Your task:
Motivation
˝ Rebuild the counter
Basics
˝ Make it increment by one
Clocked and $past
˝ Prove that this abstracted counter works
k Induction

Bus Properties

Free Variables

Abstraction
Lesson Overview
Formal
Proof
Pictures
Examples
Ź Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

168 / 351
 Exercise #8
Welcome Your task:
Motivation
˝ Rebuild the counter
Basics
˝ Make it increment by one
Clocked and $past
˝ Prove that this abstracted counter works
k Induction

Bus Properties Hints:

Free Variables

Abstraction
˝ &r_count must take place before r_count==0
Lesson Overview ˝ You cannot skip &r_count
Formal
Proof ˝ Neither can you skip r_count == 0
Pictures
Examples
Ź Exercise

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

168 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Invariants
Ź Invariants
Lesson Removed

Multiple-Clocks

Cover

Sequences

Quizzes

169 / 351
 Lesson Removed
Welcome This lesson is currently being revised, and will be released again
Motivation shortly
Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants
Ź Lesson Removed

Multiple-Clocks

Cover

Sequences

Quizzes

170 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Multiple-Clocks
Invariants

Ź Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

171 / 351
 Lesson Overview
Welcome The SymbiYosys option multiclock . . .
Motivation
˝ Used to process systems with dissimilar clocks
Basics
˝ Examples
Clocked and $past

k Induction – A serial port, with a formally generated transmitter

Bus Properties coming from a different clock domain
Free Variables
– A SPI controller that needs both high speed and low
Abstraction
speed logic
Invariants

Multiple-Clocks
Ź Basics
Our Objective:
SBY File
$global clock
˝ To learn how to handle multiple clocks within a design
$rose
$stable – $global clock
Examples – $stable, $changed
Exercises

Cover
– $rose, $fell
Sequences

Quizzes

172 / 351
 SymbiYosys config change
Welcome [ options ]
Motivation mode prove
Basics multiclock on
Clocked and $past

k Induction [ engines ]
Bus Properties smtbmc
Free Variables

Abstraction [ script ]
Invariants read ´formal module . v
Multiple-Clocks prep ´top module
Basics
Ź SBY File
[ files ]
$global clock
$rose # file list
$stable
Examples
Exercises

Cover

Sequences

Quizzes

173 / 351
 SymbiYosys config change
Welcome [ options ]
Motivation mode prove
Basics multiclock on Multiple clocks require this line
Clocked and $past

k Induction [ engines ]
Bus Properties smtbmc
Free Variables

Abstraction [ script ]
Invariants read ´formal module . v
Multiple-Clocks prep ´top module
Basics
Ź SBY File
[ files ]
$global clock
$rose # file list
$stable
Examples
Exercises

Cover

Sequences

Quizzes

173 / 351
 Five Tools
Welcome ˝ $global clock
Motivation A global simulation clock, updated on each time-step
Basics ˝ $stable
Clocked and $past True if a signal is stable (i.e. doesn’t change) with this clock.
k Induction
Equivalent to A == $past(A)
Bus Properties
˝ $changed
Free Variables
True if a signal has changed since the last clock tick.
Abstraction

Invariants
Equivalent to A != $past(A)
Multiple-Clocks
˝ $rose
Basics True if the signal rises on this simulation step
Ź SBY File
$global clock This is very useful for positive edged clocks transitions
$rose
$rose(A) is equivalent to (A[0])&&(!$past(A[0]))
$stable
Examples ˝ $fell
Exercises
True if a signal falls on this simulation step, creating a
Cover
negative edge
Sequences
$fell (A) is equivalent to (!A[0])&&($past(A[0]))
Quizzes

174 / 351
 $global clock
Welcome ˝ A global simulation clock, updated on each time-step
Motivation ˝ You can use this to describe clock properties
Basics
// Assume a s i n g l e c l o c k s i g n a l
Clocked and $past
//
k Induction
reg f_last_clk ;
Bus Properties

Free Variables
i n i t i a l f_last_clk = 0 ;
Abstraction
always @ ( $ g l o b a l c l o c k )
Invariants
begin
Multiple-Clocks
Basics
f_last_clk <= ! f_last_clk ;
SBY File assume ( i_clk == f_last_clk ) ;
Ź $global clock end
$rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

175 / 351
 $global clock
Welcome ˝ A global simulation clock, updated on each time-step
Motivation ˝ You can use this to describe clock properties
Basics
// Assume two r e l a t e d c l o c k s i g n a l s
Clocked and $past
//
k Induction
reg [3:0] f_clk_counter ;
Bus Properties

Free Variables
i n i t i a l f_clk_counter = 0 ;
Abstraction
always @ ( $ g l o b a l c l o c k )
Invariants
begin
Multiple-Clocks
Basics
f_clk_counter <= f_clk_counter + 1 ’ b1 ;
SBY File assume ( i_clk_fast == f_clk_counter [ 0 ] ) ;
Ź $global clock assume ( i_clk_slow == f_clk_counter [ 3 ] ) ;
$rose
$stable end
Examples
Exercises

Cover

Sequences

Quizzes

176 / 351
 $global clock
Welcome ˝ A global simulation clock, updated on each time-step
Motivation ˝ You can use this to describe clock properties
Basics
// Assume two c l o c k s , same sp eed ,
Clocked and $past
// unknown c o n s t a n t p h a s e o f f s e t
k Induction
// ...
Bus Properties
(∗ anyconst ∗ ) w i r e [ 3 : 0 ] f_clk_offset ;
Free Variables

Abstraction
i n i t i a l f_clk_counter= 0 ;
Invariants
always @ ( $ g l o b a l c l o c k )
Multiple-Clocks
Basics
begin
SBY File f_clk_counter <= f_clk_counter + 1 ’ b1 ;
Ź $global clock f_clk_two <= f_clk_counter
$rose
$stable + f_clk_offset ;
Examples assume ( i_clk_one == f_clk_counter [ 3 ] ) ;
Exercises
assume ( i_clk_two == f_clk_two [ 3 ] ) ;
Cover
end
Sequences

Quizzes

177 / 351
 $global clock
Welcome How might you describe two unrelated clocks?
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
Ź $global clock
$rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

178 / 351
 $global clock
Welcome How might you describe two unrelated clocks?
Motivation
( ∗ anyconst ∗ ) w i r e [ 7 : 0 ] f_a_step ;
Basics
always @ ( ∗ )
Clocked and $past
assume ( ( f_a_step > 0 )
k Induction
&&(f_a_step [ 7 ] == 1 ’ b0 ) ) ;
Bus Properties

Free Variables
always @ ( $ g l o b a l c l o c k )
Abstraction
begin
Invariants
f_a_counter <= f_a_counter + f_a_step ;
Multiple-Clocks
Basics
SBY File assume ( i_clk_a == f_a_counter [ 7 ] ) ;
Ź $global clock end
$rose
$stable
Examples
Exercises ˝ The (∗ anyconst ∗) will take on any arbitrary, but constant
Cover value
Sequences ˝ You can repeat this logic for the second clock.
Quizzes

178 / 351
 $rose
Welcome Synchronous logic has some requirements
Motivation
˝ Inputs should only change on a clock edge
Basics
They should be stable otherwise
Clocked and $past
˝ $rose(i_clk) can be used to express this
k Induction

Bus Properties Here’s an example using $rose(i_clk) . . .

Free Variables

Abstraction
always @ ( $ g l o b a l c l o c k )
Invariants
i f ( ! $ros e ( i_clk ) )
Multiple-Clocks
assume ( i_input == $past ( i_input ) ) ;
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

179 / 351
 $rose
Welcome Would this work?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $ros e ( i_clk ) )
Clocked and $past
a s s e r t ( i_input == $past ( i_input ) ) ;
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

180 / 351
 $rose
Welcome Would this work?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $ros e ( i_clk ) )
Clocked and $past
a s s e r t ( i_input == $past ( i_input ) ) ;
k Induction

Bus Properties

Free Variables ˝ No. The general rule hasn’t changed

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

180 / 351
 $rose
Welcome Could we do it this way?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( $ f e l l ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

181 / 351
 $rose
Welcome Could we do it this way?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( $ f e l l ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables ˝ No, this doesn’t work either

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

181 / 351
 $rose
Welcome Is this equivalent?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $past ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

182 / 351
 $rose
Welcome Is this equivalent?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $past ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables ˝ Why not?

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

182 / 351
 $rose
Welcome This fixes our problems. Will this work?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $ros e ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

183 / 351
 $rose
Welcome This fixes our problems. Will this work?
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ! $ros e ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties

Free Variables ˝ Not quite. Can you see the problem?

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

183 / 351
 $rose
Welcome ˝ State/outputs should be clock synchronous
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( ( f_past_valid )&&(! $ros e ( i_clk ) )
Clocked and $past
a s s e r t ( state == $past ( state ) ) ;
k Induction

Bus Properties
˝ With f_past_valid this works
Free Variables
˝ $rose requires a clock, such as
Abstraction
always @($global clock)
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
Ź $rose
$stable
Examples
Exercises

Cover

Sequences

Quizzes

184 / 351
 $stable
Welcome Describes a signal which has not changed
Motivation
˝ Requires a clock edge
Basics

Clocked and $past always @($global clock)

k Induction always @(posedge i_clk)
Bus Properties
˝ Caution: The value might still change between clock edges
Free Variables

Abstraction always @ ( $ g l o b a l c l o c k )
Invariants i f ( ( f_past_valid )&&(! $ros e ( i_clk ) ) )
Multiple-Clocks a s s e r t ( $ s t a b l e ( state ) ) ;
Basics
SBY File
$global clock ˝ This is basically the same as state == $past(state)
$rose
Ź $stable
Examples
Exercises

Cover

Sequences

Quizzes

185 / 351
 $fell
Welcome $fell is like $rose, only it describes a negative edge
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
Ź $stable
Examples
Exercises

Cover

Sequences

Quizzes

186 / 351
 Examples
Welcome ˝ Most logic doesn’t need the multiclock option
Motivation ˝ To help with logic that might need it, I use a parameter
Basics

Clocked and $past parameter [ 0 : 0 ] F_OPT_CLK2FFLOGIC = 1 ’ b0 ;

k Induction

Bus Properties generate i f ( F_OPT_CLK2FFLOGIC )

Free Variables begin
Abstraction always @ ( $ g l o b a l c l o c k )
Invariants i f ( ( f_past_valid )&&(! $ros e ( i_clk ) ) )
Multiple-Clocks begin
Basics
SBY File
assume ( $ s t a b l e ( i_axi_awready ) ) ;
$global clock assume ( $ s t a b l e ( i_axi_wready ) ) ;
$rose //
$stable
Ź Examples
a s s e r t ( $ s t a b l e ( o_axi_bid ) ) ;
Exercises // . . .
Cover end
Sequences end endgenerate
Quizzes

187 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you formally describe the o_SCK and o_CS_n
Abstraction relationship?
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

188 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you formally describe the o_SCK and o_CS_n
Abstraction relationship?
Invariants

Multiple-Clocks i n i t i a l a s s e r t ( o_CS_n ) ;
Basics
i n i t i a l a s s e r t ( o_SCK ) ;
SBY File
$global clock
$rose always @ ( ∗ )
$stable
Ź Examples
i f ( ! o_SCK )
Exercises a s s e r t ( ! o_CS_n ) ;
Cover

Sequences

Quizzes

188 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you formally describe the o_SCK and o_CS_n
Abstraction relationship?
Invariants

Multiple-Clocks always @ ( $ g l o b a l c l o c k )
Basics
i f ( ( f_past_valid )
SBY File
$global clock &&(( $ros e ( o_CS_n ) ) | | ( $ f e l l ( o_CS_n ) ) ) )
$rose a s s e r t ( ( o_SCK)&&( $ s t a b l e ( o_SCK ) ) ) ;
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

189 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you describe o_MOSI?
Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

190 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you describe o_MOSI?
Abstraction

Invariants always @ ( $ g l o b a l c l o c k )
Multiple-Clocks i f ( ( f_past_valid )&&(! o_CS_n )&&(! $ f e l l ( o_SCK ) ) )
Basics a s s e r t ( $ s t a b l e ( o_MOSI ) ) ;
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

190 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you describe i_MISO?
Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

191 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ How would you describe i_MISO?
Abstraction

Invariants always @ ( $ g l o b a l c l o c k )
Multiple-Clocks i f ( ( ! o_CS_n)&&(o_SCK ) )
Basics assume ( $ s t a b l e ( i_MISO ) ) ;
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

191 / 351
 Ex SPI Port
Welcome o CS n
Motivation
o SCK
Basics
o MOSI
Clocked and $past

k Induction
i MISO
Bus Properties

Free Variables
˝ Should the i_MISO be able to change more than once per
Abstraction clock?
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Ź Examples
Exercises

Cover

Sequences

Quizzes

192 / 351
 Ex SPI Port
Welcome ˝ A little logic will force i_MISO to have only one transition per
Motivation clock
Basics
always @ ( $ g l o b a l c l o c k )
Clocked and $past
i f ( ( o_CS_n ) | | ( o_SCK ) )
k Induction
f_chgd <= 1 ’ b0 ;
Bus Properties
e l s e i f ( i_MISO != $past ( i_MISO ) )
Free Variables
f_chgd <= 1 ’ b1 ;
Abstraction

Invariants
always @ ( $ g l o b a l c l o c k )
Multiple-Clocks
Basics
i f ( ( f_past_valid)&&(f_chgd ) )
SBY File assume ( $ s t a b l e ( i_MISO ) ) ;
$global clock
$rose
$stable
˝ How would we force exactly 8 o_SCK clocks?
Ź Examples
Exercises

Cover

Sequences

Quizzes

193 / 351
 Ex SPI Port
Welcome ˝ Forcing exactly 8 clocks
Motivation
always @ ( $ g l o b a l c l o c k )
Basics
i f ( o_CS_n )
Clocked and $past
f_spi_bits <= 0 ;
k Induction
e l s e i f ( $ros e ( o_SCK ) )
Bus Properties
f_spi_bits <= f_spi_bits + 1 ’ b1 ;
Free Variables

Abstraction
always @ ( $ g l o b a l c l o c k )
Invariants
i f ( ( f_past_valid)&&( $ros e ( o_CS_n ) ) )
Multiple-Clocks a s s e r t ( f_spi_bits == 8 ) ;
Basics
SBY File
$global clock ˝ Don’t forget the induction requirement
$rose
$stable always @ ( ∗ )
Ź Examples
a s s e r t ( f_spi_bits <= 8 ) ;
Exercises

Cover

Sequences

Quizzes

194 / 351
 Exercises
Welcome Three exercises, chose one to verify:
Motivation
1. Input serdes
Basics
exercises-09/iserdes.v
Clocked and $past

k Induction
2. Clock gate
Bus Properties
exercises-10/clkgate.v
Free Variables 3. Clock Switch
Abstraction exercises-11/clkswitch.v
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

195 / 351
 Ex: Input Serdes
Welcome Getting a SERDES right is a good example of multiple clocks
Motivation

Basics i fast clk

Clocked and $past
i pin
k Induction
i slow clk
Bus Properties

Free Variables
o word 0x0b

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

196 / 351
 Ex: Input Serdes
Welcome Getting a SERDES right is a good example of multiple clocks
Motivation
˝ Two clocks, one fast and one slow
Basics

Clocked and $past Clocks must be synchronous

k Induction $rose(slow_clk) implies $rose(fast_clk)
Bus Properties
˝ exercise-09/ Contains the file iserdes.v
Free Variables

Abstraction
˝ Can you formally verify that it works?
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

197 / 351
 Ex: Input Serdes
Welcome Be aware of the asynchronous reset signal!
Motivation

Basics i areset n
Clocked and $past
i fast clk
k Induction
i pin
Bus Properties

Free Variables
i slow clk
Abstraction o word Prior value RESET RESET

Invariants

Multiple-Clocks ˝ Can be asserted at any time

Basics
SBY File
˝ Can only be de-asserted on $rose(i_slow_clk)
$global clock ˝ assume() these properties, since the reset is an input
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

198 / 351
 Ex: Clock Gate
Welcome The goal: a clock that can be gated, that doesn’t glitch
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
˝ exercise-10/ Contains the file clkgate.v
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

199 / 351
 Ex: Clock Gate
Welcome The goal: a clock that can be gated, that doesn’t glitch
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants
i clk
Multiple-Clocks i en
Basics
SBY File
o clk
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

200 / 351
 Ex: Clock Gate
Welcome The goal: a clock that can be gated, that doesn’t glitch
Motivation
˝ One clock, one unrelated enable
Basics
˝ Prove that the output clock
Clocked and $past

k Induction – is always high for the full width, but

Bus Properties – . . . never longer.
Free Variables
– For any clock rate
Abstraction

Invariants See exercise-10/clkgate.v

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

201 / 351
 Ex: Clock Gate
Welcome Hints:
Motivation
˝ The output clock should only rise if the incoming clock rises
Basics
˝ The output clock should only fall if the incoming clock fall
Clocked and $past
˝ If the output clock is ever high, it should always fall with the
k Induction

Bus Properties
incoming clock
Free Variables
Be aware of the reset! The output clock might fall mid-clock
Abstraction
period due to the asynchronous reset.
Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

202 / 351
 Ex: Clock Switch
Welcome Goal: To safely switch from one clock frequency to another
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

203 / 351
 Ex: Clock Switch
Welcome Goal: To safely switch from one clock frequency to another
Motivation
˝ Inputs
Basics

Clocked and $past – Two arbitrary clocks

k Induction – One select line
Bus Properties

Free Variables Prove that the output clock

Abstraction
˝ Is always high (or low) for at least the duration of one of the
Invariants

Multiple-Clocks
clocks
Basics ˝ Doesn’t stop
SBY File
$global clock You may need to constrain the select line.
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

204 / 351
 Ex: Clock Switch
Welcome Hints:
Motivation
˝ You may assume the reset is only ever initially true
Basics
˝ Only one set of FF’s should ever change at any time
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
Basics
SBY File
$global clock
$rose
$stable
Examples
Ź Exercises

Cover

Sequences

Quizzes

205 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Cover
Invariants

Multiple-Clocks

Ź Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

206 / 351
 Lesson Overview
Welcome The cover element is used to make certain something remains
Motivation possible
Basics
˝ BMC and induction test safety properties
Clocked and $past

k Induction
They prove that something will not happen
Bus Properties
˝ Cover tests a liveness property
Free Variables It proves that something may happen
Abstraction
Objectives
Invariants

Multiple-Clocks ˝ Understand why cover is important

Cover ˝ Understand how to use cover
Ź Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

207 / 351
 Why Cover
Welcome Personal examples:
Motivation
˝ Forgot to set f_past_valid to one
Basics
Many assertions were ignored
Clocked and $past
˝ Av to WB bridge, passed FV, but couldn’t handle writes
k Induction

Bus Properties
˝ Error analysis
Free Variables The simulation trace doesn’t make sense. Can it be
Abstraction reproduced?
Invariants ˝ As an anti-assertion
Multiple-Clocks Can this situation actually happen?
Cover
Ź Lesson Overview What is cover good for? Catching the careless assumption!
BMC vs Cover
Cover in Verilog
What else? Ad hoc simulation traces!
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

208 / 351
 BMC vs Cover
Welcome Cover is more like BMC than Induction is
Motivation
˝ BMC
Basics

Clocked and $past

k Induction

Bus Properties ˝ Cover

Free Variables

Abstraction

Invariants

Multiple-Clocks ˝ BMC searches for failures

Cover ˝ Cover searches for a success
Lesson Overview
Ź BMC vs Cover Formally, we might say . . .
Cover in Verilog
State Space
SymbiYosys
˝ BMC + k-Induction: proof for all
Examples @assume()ñ @assert()
Counter
˝ Cover: there exists one
Sequences
@assume()ñ Dcover()
Quizzes

209 / 351
 Cover in Verilog
Welcome Just like an assumption or an assertion
Motivation
// Make s u r e a w r i t e i s p o s s i b l e
Basics
always @ ( posedge i_clk )
Clocked and $past
cover ( ( o_wb_stb )&&(! i_wb_stall)&&(o_wb_we ) ) ;
k Induction

Bus Properties
// Or
Free Variables

Abstraction
// What h a p p e n s when a bus c y c l e i s a b o r t e d ?
Invariants
always @ ( posedge i_clk )
Multiple-Clocks i f ( i_reset )
Cover cover ( ( o_wb_cyc)&&(f_wb_outstanding > 0 ) ) ;
Lesson Overview
BMC vs Cover
Ź Cover in Verilog Well, almost but not quite.
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

210 / 351
 Cover in Verilog
Welcome Assert and cover handle surrounding logic differently
Motivation
˝ Assert logic
Basics

Clocked and $past always @ ( posedge i_clk )

k Induction i f (A)
Bus Properties assert (B ) ;
Free Variables

Abstraction is equivalent to,

Invariants
always @ ( posedge i_clk )
Multiple-Clocks
assert ( (! A) | | (B) ) ;
Cover
Lesson Overview
BMC vs Cover This is not true of cover.
Ź Cover in Verilog
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

211 / 351
 Cover in Verilog
Welcome Assert and cover handle surrounding logic differently
Motivation
˝ Assert logic
Basics
˝ Cover logic
Clocked and $past

k Induction always @ ( posedge i_clk )

Bus Properties i f (A)
Free Variables cover ( B ) ;
Abstraction

Invariants is equivalent to,

Multiple-Clocks
always @ ( posedge i_clk )
Cover
Lesson Overview
cover ( ( A ) && ( B ) ) ;
BMC vs Cover // NOT t h e same a s
Ź Cover in Verilog // a s s e r t ( ( ! A) | | (B) ) ;
State Space
SymbiYosys
Examples
Counter

Sequences

Quizzes

212 / 351
 State Space
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog ˝ Goal is to prove certain state’s are reachable
Ź State Space
˝ Prover solves for example traces
SymbiYosys
Examples
Counter

Sequences

Quizzes

213 / 351
 SymbiYosys
Welcome The SymbiYosys script for cover needs to change as well
Motivation
˝ SymbiYosys needs the option: mode cover
Basics
˝ Produces one trace per cover statement
Clocked and $past

k Induction
. . . or fail
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
Ź SymbiYosys
Examples
Counter

Sequences

Quizzes

214 / 351
 SymbiYosys cover config
Welcome [ options ]
Motivation mode cover
Basics depth 40
Clocked and $past append 20
k Induction

Bus Properties [ engines ]

Free Variables smtbmc
Abstraction

Invariants [ script ]
Multiple-Clocks read ´formal module . v
Cover prep ´top module
Lesson Overview
BMC vs Cover
Cover in Verilog
[ files ]
State Space # file list
Ź SymbiYosys
Examples
Counter

Sequences

Quizzes

215 / 351
 SymbiYosys cover config
Welcome [ options ]
Motivation mode cover Run a coverage analysis
Basics depth 40
Clocked and $past append 20
k Induction

Bus Properties [ engines ]

Free Variables smtbmc
Abstraction

Invariants [ script ]
Multiple-Clocks read ´formal module . v
Cover prep ´top module
Lesson Overview
BMC vs Cover
Cover in Verilog
[ files ]
State Space # file list
Ź SymbiYosys
Examples
Counter

Sequences

Quizzes

215 / 351
 SymbiYosys cover config
Welcome [ options ]
Motivation mode cover
Basics depth 40 How far to look for a covered state
Clocked and $past append 20
k Induction

Bus Properties [ engines ]

Free Variables smtbmc
Abstraction

Invariants [ script ]
Multiple-Clocks read ´formal module . v
Cover prep ´top module
Lesson Overview
BMC vs Cover
Cover in Verilog
[ files ]
State Space # file list
Ź SymbiYosys
Examples
Counter

Sequences

Quizzes

215 / 351
 SymbiYosys cover config
Welcome [ options ]
Motivation mode cover
Basics depth 40
Clocked and $past append 20 Follow each trace with 20 extra clocks
k Induction

Bus Properties [ engines ]

Free Variables smtbmc
Abstraction

Invariants [ script ]
Multiple-Clocks read ´formal module . v
Cover prep ´top module
Lesson Overview
BMC vs Cover
Cover in Verilog
[ files ]
State Space # file list
Ź SymbiYosys
Examples
Counter

Sequences

Quizzes

215 / 351
 Cover Failures
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview Two basic types of cover failures
BMC vs Cover
Cover in Verilog 1. Covered state is unreachable
State Space
Ź SymbiYosys
No VCD file will be generated upon failure
Examples 2. Covered state is reachable, but only by breaking assertions
Counter

Sequences
VCD file will be generated
Quizzes

216 / 351
 Ex: I-Cache
Welcome Consider a CPU I-cache:
Motivation
always @ ( posedge i_clk )
Basics
cover ( o_valid ) ;
Clocked and $past

k Induction
With no other formal logic, what will this trace look like?
Bus Properties

Free Variables ˝ CPU must provide a PC address

Abstraction ˝ Design must fill the appropriate cache line
Invariants ˝ Design returns an item from that cache line
Multiple-Clocks
That’s a lot of trace for two lines of added code!
Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Ź Examples
Counter

Sequences

Quizzes

217 / 351
 Ex: Flash
Welcome Consider a Flash controller:
Motivation
always @ ( posedge i_clk )
Basics
cover ( o_wb_ack ) ;
Clocked and $past

k Induction
With no other formal logic, what will this trace look like?
Bus Properties
The controller must,
Free Variables

Abstraction ˝ Initialize the flash device

Invariants ˝ Accept a bus request
Multiple-Clocks ˝ Request a read from the flash
Cover ˝ Accumulate the result to return on the bus
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Ź Examples
Counter

Sequences

Quizzes

218 / 351
 Ex: MMU
Welcome Consider a Memory Management Unit (MMU):
Motivation
always @ ( posedge i_clk )
Basics
cover ( o_wb_ack ) ;
Clocked and $past

k Induction
The MMU must,
Bus Properties

Free Variables ˝ Be told a TLB entry

Abstraction ˝ Accept a bus request
Invariants ˝ Look the request up in the TLB
Multiple-Clocks ˝ Forward the modified request downstream
Cover
Lesson Overview
˝ Wait for a return
BMC vs Cover ˝ Forward the value returned upstream
Cover in Verilog
State Space
SymbiYosys
Ź Examples
Counter

Sequences

Quizzes

219 / 351
 Ex: SDRAM
Welcome How about an SDRAM controller?
Motivation
always @ ( posedge i_clk )
Basics
cover ( o_wb_ack ) ;
Clocked and $past

k Induction
The controller must,
Bus Properties

Free Variables ˝ Initialize the SDRAM

Abstraction ˝ Accept a bus request
Invariants ˝ Activate a row on a bank
Multiple-Clocks ˝ Issue a read (or write) command from that row
Cover ˝ Wait for a return value
Lesson Overview
BMC vs Cover ˝ Return the result
Cover in Verilog
State Space
SymbiYosys
Ź Examples
Counter

Sequences

Quizzes

220 / 351
 Counter
Welcome Remember our counter?
Motivation
i n i t i a l counter = 0 ;
Basics
always @ ( posedge i_clk )
Clocked and $past
i f ( ( i_start_signal)&&(counter == 0 ) )
k Induction
counter <= MAX_AMOUNT ´1’b1 ;
Bus Properties
e l s e i f ( counter != 0 )
Free Variables
counter <= counter ´ 1 ’ b1 ;
Abstraction

Invariants
always @ ( ∗ )
Multiple-Clocks o_busy = ( counter != 0 ) ;
Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

221 / 351
 Examples
Welcome Let’s add some cover statements. . .
Motivation
// T r a n s i t i o n t o b u s y
Basics
always @ ( posedge i_clk )
Clocked and $past
i f ( ( f_past_valid )&&(! $past ( o_busy ) ) )
k Induction
cover ( o_busy ) ;
Bus Properties

Free Variables
// T r a n s i t i o n back t o i d l e
Abstraction
always @ ( posedge i_clk )
Invariants
i f ( ( f_past_valid)&&( $past ( o_busy ) ) )
Multiple-Clocks cover ( ! o_busy ) ;
Cover
Lesson Overview
BMC vs Cover // Mid´c y c l e
Cover in Verilog always @ ( posedge i_clk )
State Space
SymbiYosys
cover ( counter == 3 ) ;
Examples
Ź Counter Will SymbiYosys find traces?
Sequences

Quizzes

222 / 351
 Examples
Welcome How about now?
Motivation
always @ ( posedge i_clk )
Basics
cover ( ( o_busy)&&(counter == 0 ) ) ;
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

223 / 351
 Examples
Welcome How about now?
Motivation
always @ ( posedge i_clk )
Basics
cover ( ( o_busy)&&(counter == 0 ) ) ;
Clocked and $past

k Induction
Or this one,
Bus Properties

Free Variables always @ ( posedge i_clk )

Abstraction cover ( counter == MAX_AMOUNT ) ;
Invariants

Multiple-Clocks
Will these succeed?
Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

223 / 351
 Examples
Welcome How about now?
Motivation
always @ ( posedge i_clk )
Basics
cover ( ( o_busy)&&(counter == 0 ) ) ;
Clocked and $past

k Induction
Or this one,
Bus Properties

Free Variables always @ ( posedge i_clk )

Abstraction cover ( counter == MAX_AMOUNT ) ;
Invariants

Multiple-Clocks
Will these succeed? No. Both will fail
Cover ˝ These are outside the reachable state space
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

223 / 351
 Examples
Welcome What if the state is unreachable?
Motivation
// Keep t h e c o u n t e r from e v e r s t a r t i n g
Basics
always @ ( ∗ )
Clocked and $past
assume ( ! i_start_signal ) ;
k Induction

Bus Properties
always @ ( posedge i_clk )
Free Variables
cover ( counter != 0 ) ;
Abstraction

Invariants Will this succeed?

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

224 / 351
 Examples
Welcome What if the state is unreachable?
Motivation
// Keep t h e c o u n t e r from e v e r s t a r t i n g
Basics
always @ ( ∗ )
Clocked and $past
assume ( ! i_start_signal ) ;
k Induction

Bus Properties
always @ ( posedge i_clk )
Free Variables
cover ( counter != 0 ) ;
Abstraction

Invariants Will this succeed? No. This will fail with no trace.
Multiple-Clocks

Cover
˝ If i_start_signal is never true, the cover cannot be reached
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

224 / 351
 Examples
Welcome What if an assertion needs to be violated?
Motivation
always @ ( ∗ )
Basics
a s s e r t ( counter != 1 0 ) ;
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
cover ( counter == 4 ) ;
Free Variables

Abstraction What will happen here?

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

225 / 351
 Examples
Welcome What if an assertion needs to be violated?
Motivation
always @ ( ∗ )
Basics
a s s e r t ( counter != 1 0 ) ;
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
cover ( counter == 4 ) ;
Free Variables

Abstraction What will happen here?

Invariants

Multiple-Clocks
˝ Cover statement is reachable
Cover ˝ But requires an assertion failure, so a trace is generated
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

225 / 351
 Clock Switch
Welcome Covering the clock switch
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants
˝ Shows the clock switching from fast to slow,
Multiple-Clocks

Cover
˝ and again from slow to fast
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

226 / 351
 Ex #8 Revisited
Welcome Return to your Wishbone arbiter. Let’s cover two cases:
Motivation
1. Cover both A and B receiving the bus
Basics
2. Cover how B will get the bus after A gets an
Clocked and $past

k Induction
acknowledgement
Bus Properties
3. Cover how A will get the bus after B gets an
Free Variables acknowledgement
Abstraction 4. Add to the last cover
Invariants
˝ B must request while A still holds the bus
Multiple-Clocks

Cover Plot and examine traces for both cases. Do they look right?
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

227 / 351
 Ex #8 Revisited
Welcome Notice what we just proved:
Motivation
1. The arbiter will allow both sources to master the bus
Basics
2. The arbiter will transition from one source to another
Clocked and $past

k Induction
3. The arbiter won’t starve A or B
Bus Properties This wasn’t possible with just the safety properties (assert
Free Variables
statements)
Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

228 / 351
 Discussion
Welcome When should you use cover?
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
Lesson Overview
BMC vs Cover
Cover in Verilog
State Space
SymbiYosys
Examples
Ź Counter

Sequences

Quizzes

229 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Sequences
Invariants

Multiple-Clocks

Cover

Ź Sequences
Overview
Clocking
Bind
Sequences
Questions?

Quizzes

230 / 351
 Lesson Overview
Welcome SystemVerilog has some amazing formal properties
Motivation
˝ property can be assumed or asserted
Basics
By rewriting our assert’s and assume’s as properties, we can
Clocked and $past

k Induction
then control when they are asserted or assumed better.
Bus Properties
˝ bind formal properties to a subset of your design
Free Variables Allows us to (finally) separate the properties from the module
Abstraction they support
Invariants ˝ sequence – A standard property description language
Multiple-Clocks
Objectives
Cover

Sequences ˝ Learn the basics of SystemVerilog Assertions

Ź Overview
Clocking ˝ Gain confidence with yosys+verific
Bind
Sequences
Questions?

Quizzes

231 / 351
 Building on the past
Welcome Much of what we’ve written can easily be rewritten in SVA
Motivation
always @ ( ∗ )
Basics
i f (A)
Clocked and $past
assert (B ) ;
k Induction

Bus Properties
can be rewritten as,
Free Variables

Abstraction always @ ( ∗ )
Invariants a s s e r t ( A |´> B ) ;
Multiple-Clocks

Cover

Sequences
Ź Overview
Clocking
Bind
Sequences
Questions?

Quizzes

232 / 351
 Building on the past
Welcome Much of what we’ve written can easily be rewritten in SVA
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( f_past_valid)&&( $past ( A ) ) )
Clocked and $past
assert (B ) ;
k Induction

Bus Properties
Can be rewritten as,
Free Variables

Abstraction always @ ( posedge i_clk )

Invariants a s s e r t ( A |=> B ) ;
Multiple-Clocks

Cover a s s e r t p r o p e r t y ( @ ( posedge i_clk ) A |=> B ) ;

Sequences
Ź Overview
Clocking
Bind
Sequences
Questions?

Quizzes

233 / 351
 Building on the past
Welcome Much of what we’ve written can easily be rewritten in SVA
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( f_past_valid)&&( $past ( A ) ) )
Clocked and $past
assert (B ) ;
k Induction

Bus Properties
Can be rewritten as,
Free Variables

Abstraction always @ ( posedge i_clk )

Invariants a s s e r t ( A |=> B ) ;
Multiple-Clocks

Cover a s s e r t p r o p e r t y ( @ ( posedge i_clk ) A |=> B ) ;

Sequences
Ź Overview
Clocking ˝ Read this as A implies B on the next clock tick.
Bind
Sequences ˝ No f_past_valid required anymore. This is a statement
Questions?
about the next clock tick, not the last one.
Quizzes

These equivalencies apply to assume() as well

233 / 351
 Properties
Welcome You can also declare properties:
Motivation
p r o p e r t y SIMPLE_PROPERTY ;
Basics
@ ( posedge i_clk ) a |=> b ;
Clocked and $past
endproperty
k Induction

Bus Properties
a s s e r t p r o p e r t y ( SIMPLE_PROPERTY ) ;
Free Variables

Abstraction This would be the same as

Invariants

Multiple-Clocks
always @ ( posedge i_clk )
Cover
i f ( ( f_past_valid)&&( $past ( a ) ) )
Sequences
assert (b ) ;
Ź Overview
Clocking
Bind
Sequences
Questions?

Quizzes

234 / 351
 Assume vs Assert
Welcome You could also do something like:
Motivation
parameter [ 0 : 0 ] SUBMODULE = 1 ’ b0 ;
Basics

Clocked and $past

generate i f ( SUBMODULE )
k Induction
begin
Bus Properties
assume p r o p e r t y ( INPUT_PROP ) ;
Free Variables
a s s e r t p r o p e r t y ( LOCAL_PROP ) ;
Abstraction
a s s e r t p r o p e r t y ( OUTPUT_PROP ) ;
Invariants
end e l s e begin
Multiple-Clocks a s s e r t p r o p e r t y ( INPUT_PROP ) ;
Cover assume p r o p e r t y ( LOCAL_PROP ) ;
Sequences assume p r o p e r t y ( OUTPUT_PROP ) ;
Ź Overview
Clocking
end endgenerate
Bind
Sequences Applications: Invariants, bus properties, etc.
Questions?

Quizzes

235 / 351
 Parameterized Properties
Welcome Properties can also accept parameters
Motivation
p r o p e r t y IMPLIES ( a , b ) ;
Basics
a |´> b ;
Clocked and $past
endproperty
k Induction

Bus Properties
a s s e r t p r o p e r t y ( IMPLIES ( x , y ) ) ;
Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Ź Overview
Clocking
Bind
Sequences
Questions?

Quizzes

236 / 351
 Parameterized Properties
Welcome Properties can also accept parameters
Motivation
p r o p e r t y IMPLIES_NEXT ( a , b ) ;
Basics
@ ( posedge i_clk ) a |=> b ;
Clocked and $past
endproperty
k Induction

Bus Properties
a s s e r t p r o p e r t y ( IMPLIES_NEXT ( x , y ) ) ;
Free Variables

Abstraction Remember, if you want to use |=>, $past, etc., you need to
Invariants
define a clock.
Multiple-Clocks

Cover

Sequences
Ź Overview
Clocking
Bind
Sequences
Questions?

Quizzes

237 / 351
 Clocking
Welcome Getting tired of writing @(posedge i_clk)?
Motivation
˝ You can set a default clock
Basics

Clocked and $past d e f a u l t c l o c k i n g @ ( posedge i_clk ) ;

k Induction endclocking
Bus Properties

Free Variables Assumes i_clk if no clock is given.

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Ź Clocking
Bind
Sequences
Questions?

Quizzes

238 / 351
 Clocking
Welcome Getting tired of writing @(posedge i_clk)?
Motivation
˝ You can set a default clock
Basics
˝ You can set a default clock within a given block
Clocked and $past

k Induction c l o c k i n g @ ( posedge i_clk ) ;

Bus Properties // Your p r o p e r t i e s can go h e r e
Free Variables // As w i t h a s s e r t , assume ,
Abstraction // s e q u e n c e , e t c .
Invariants endclocking
Multiple-Clocks

Cover Assumes i_clk for all of the properties within the clocking
Sequences block.
Overview
Ź Clocking
Bind
Sequences
Questions?

Quizzes

239 / 351
 Global Clocking
Welcome When using verific, $global clock must first be defined
Motivation
( ∗ gclk ∗ ) w i r e gbl_clk ;
Basics
g l o b a l c l o c k i n g @ ( posedge gbl_clk ) ; e n d c l o c k i n g
Clocked and $past

k Induction
This defines the $global clock . . .
Bus Properties

Free Variables ˝ as a positive edge transition of gbl_clk.

Abstraction ˝ The (∗ gclk ∗) attribute turns it into a formal timestep
Invariants

Multiple-Clocks

Cover

Sequences
Overview
Ź Clocking
Bind
Sequences
Questions?

Quizzes

240 / 351
 Bind
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Common bench testing works on black boxes

Invariants
˝ This doesn’t work well with formal methods
Multiple-Clocks

Cover

Sequences
Overview
Clocking
Ź Bind
Sequences
Questions?

Quizzes

241 / 351
 Bind
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Common bench testing works on black boxes

Invariants
˝ This doesn’t work well with formal methods
Multiple-Clocks
˝ Placing properties within a module doesn’t separate the two
Cover

Sequences
Overview
Clocking
Ź Bind
Sequences
Questions?

Quizzes

241 / 351
 Bind
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction ˝ Common bench testing works on black boxes

Invariants
˝ This doesn’t work well with formal methods
Multiple-Clocks
˝ Placing properties within a module doesn’t separate the two
Cover

Sequences Using the SVA bind command, we can

Overview
Clocking ˝ Separate properties from a design
Ź Bind
˝ Maintains the necessary “white box” perspective
Sequences
Questions?

Quizzes

241 / 351
 Bind
Welcome ˝ Can bind to specific named variables
Motivation
module mut ( i n p u t i , output o ) ;
Basics
reg r;
Clocked and $past
// Your l o g i c h e r e
k Induction
endmodule
Bus Properties

Free Variables
module mut_formal ( i n p u t a , i n p u t b , i n p u t r ) ;
Abstraction
// Your f o r m a l p r o p e r t i e s go h e r e
Invariants
endmodule
Multiple-Clocks

Cover bind mut mut_formal mut_instance (

Sequences // Bind i n p u t s t o g e t h e r
Overview
Clocking
. a(i) , . b(o) , . r(r)
Ź Bind // The g e n e r a l f o r m a t i s
Sequences
Questions?
. mut_formal_name ( mut_name ) ) ;
Quizzes
˝ Note all mut_formal ports must be inputs

242 / 351
 Bind
Welcome ˝ Can bind to specific named variables
Motivation ˝ Can also make all variables available to your properties
Basics
module mut ( i n p u t i , output o ) ;
Clocked and $past
reg r;
k Induction
// Your l o g i c h e r e
Bus Properties
endmodule
Free Variables

Abstraction
module mut_formal ( i n p u t i , i n p u t o , i n p u t r ) ;
Invariants
// Your f o r m a l p r o p e r t i e s go h e r e
Multiple-Clocks
endmodule
Cover

Sequences
Overview
// Make e v e r y mut v a r i a b l e a v a i l a b l e i n
Clocking // m u t f o r m a l w i t h a v a r i a b l e o f t h e same
Ź Bind // name
Sequences
Questions?
bind mut mut_formal mut_instance ( . ∗ ) ;
Quizzes
˝ In order to use .∗ , names must match

243 / 351
 Bind
Welcome ˝ Can bind to specific named variables
Motivation ˝ Can also make all variables available to your properties
Basics ˝ Can pass parameters through as well
Clocked and $past

k Induction
module mut ( i n p u t i , output o ) ;
Bus Properties
parameter ONE = 5 ;
Free Variables
// Your l o g i c h e r e
endmodule
Abstraction

Invariants
module mut_formal ( i n p u t i , i n p u t o , i n p u t r ) ;
Multiple-Clocks
parameter TWO = 1 4 ;
Cover
// Your f o r m a l p r o p e r t i e s go h e r e
Sequences
Overview
endmodule
Clocking
Ź Bind
bind mut mut_formal #(. TWO ( ONE ) )
Sequences
Questions? mut_instance ( . ∗ ) ;
Quizzes

244 / 351
 Sequences
Welcome So far with properties,
Motivation
˝ We haven’t done anything really all that new.
Basics
˝ We’ve just rewritten what we’ve done before in a new form.
Clocked and $past

k Induction Sequences are something new

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

245 / 351
 Sequence
Welcome With sequences, you can
Motivation
˝ Specify a series of actions
Basics

Clocked and $past sequence EXAMPLE ;

k Induction @ ( posedge i_clk ) a ##1 b ##1 c ##1 d ;
Bus Properties endsequence
Free Variables

Abstraction In this example, b always follows a by one clock, c follows b,

Invariants and d follows c
Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

246 / 351
 Sequence
Welcome With sequences, you can
Motivation
˝ Specify a series of actions, separated by some number of
Basics
clocks
Clocked and $past

k Induction sequence EXAMPLE ;

Bus Properties @ ( posedge i_clk ) a ##2 b ##5 c ;
Free Variables endsequence
Abstraction

Invariants In this example, b always follows a two clocks later, and c

Multiple-Clocks follows five clocks after b
Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

247 / 351
 Sequence
Welcome With sequences, you can
Motivation
˝ Specify a series of predicates, separated in time
Basics
˝ Can express range(s) of repeated values
Clocked and $past

k Induction sequence EXAMPLE ;

Bus Properties @ ( posedge i_clk ) b [ ∗ 2 : 3 ] ##1 c ;
Free Variables endsequence
Abstraction // i s e q u i v a l e n t t o . . .
Invariants sequence EXAMPLE_A_2x ; // 2 x
Multiple-Clocks @ ( posedge i_clk ) b ##1 b ##1 c ;
Cover endsequence
Sequences // o r
Overview sequence EXAMPLE_A_3x ; // 3 x
Clocking
Bind
@ ( posedge i_clk ) b ##1 b ##1 b ##1 c ;
Ź Sequences endsequence
Questions?

Quizzes

248 / 351
 Sequence
Welcome With sequences, you can
Motivation
˝ Specify a series of predicates, separated in time
Basics
˝ Can express range(s) of repeated values
Clocked and $past

k Induction – [∗0: M] Predicate may be skipped

Bus Properties – [∗N:M] specifies from N to M repeats
Free Variables
– [∗N:$] Repeats at least N times, with no maximum
Abstraction

Invariants
Ranges can include empty sequences, such as ##[∗0:4]
Multiple-Clocks ˝ Compose multiple sequences together
Cover
– AND, seq_1 and seq_2
Sequences
Overview – OR, seq_1 or seq_2
Clocking – NOT, not seq
Bind
Ź Sequences
Questions?

Quizzes

249 / 351
 And vs Intersect
Welcome The and and intersect operators are very similar
Motivation
˝ and is only true if both sequences are true
Basics
˝ intersect is only true if both sequences are true and have the
Clocked and $past

k Induction
same length
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

250 / 351
 Equivalences
Welcome ˝ Throughout
Motivation
sequence A ;
Basics
@ ( posedge i_clk )
Clocked and $past
( EXP ) [ ∗ 0 : $ ] i n t e r s e c t SEQ ;
k Induction
endsequence
Bus Properties

Free Variables
is equivalent to
Abstraction

Invariants sequence B ;
Multiple-Clocks
@ ( posedge i_clk )
Cover
( EXP ) throughout SEQ ;
Sequences
endsequence
Overview
Clocking The EXP expression must be true from now until SEQ ends
Bind
Ź Sequences
Questions?

Quizzes

251 / 351
 Equivalences
Welcome ˝ Throughout
Motivation ˝ Until
Basics
sequence A ;
Clocked and $past
@ ( posedge i_clk )
k Induction
( E1 ) [ ∗ 0 : $ ] ##1 ( E2 ) ;
Bus Properties
endsequence
Free Variables

Abstraction
is equivalent to
Invariants

Multiple-Clocks sequence B ;
Cover @ ( posedge i_clk )
Sequences ( E1 ) u n t i l E2 ;
Overview endsequence
Clocking
Bind
Ź Sequences
Questions?

Quizzes

252 / 351
 Equivalences
Welcome ˝ Throughout
Motivation ˝ Until
Basics
sequence A ;
Clocked and $past
@ ( posedge i_clk )
k Induction
( E1 ) [ ∗ 0 : $ ] ##1 ( E2 ) ;
Bus Properties
endsequence
Free Variables

Abstraction
is equivalent to
Invariants

Multiple-Clocks sequence B ;
Cover @ ( posedge i_clk )
Sequences ( E1 ) u n t i l E2 ;
Overview endsequence
Clocking
Bind
Ź Sequences ˝ There is an ugly subtlety here
Questions?

Quizzes

252 / 351
 Equivalences
Welcome ˝ Throughout
Motivation ˝ Until
Basics ˝ Within
Clocked and $past

k Induction
sequence A ;
Bus Properties
@ ( posedge i_clk )
Free Variables
( 1 [ ∗ 0 : $ ] ##1 S1 ##1 1 [ ∗ 0 : $ ] )
i n t e r s e c t S2 ;
Abstraction
endsequence
Invariants

Multiple-Clocks
is equivalent to
Cover

Sequences sequence B ;
Overview @ ( posedge i_clk )
Clocking
Bind ( S1 ) w i t h i n S2 ;
Ź Sequences endsequence
Questions?

Quizzes

253 / 351
 Returning to Properties
Welcome Properties can reference sequences
Motivation
˝ Directly
Basics

Clocked and $past a s s e r t p r o p e r t y ( seq ) ;

k Induction a s s e r t p r o p e r t y ( expr |´> seq ) ;
Bus Properties

Free Variables ˝ Implication: sequences can imply properties

Abstraction
a s s e r t p r o p e r t y ( seq |´> some_other_property ) ;
Invariants
a s s e r t p r o p e r t y ( seq |=> another_property ) ;
Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

254 / 351
 Returning to Properties
Welcome Properties can include . . .
Motivation
˝ if statements
Basics

Clocked and $past a s s e r t p r o p e r t y ( i f ( A ) P1 e l s e P2 ) ;

k Induction

Bus Properties ˝ not, and, or even or statements

Free Variables
a s s e r t p r o p e r t y ( not P1 ) ;
Abstraction
a s s e r t p r o p e r t y ( P1 and P2 ) ;
Invariants
a s s e r t p r o p e r t y ( P1 or P2 ) ;
Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

255 / 351
 Ex. Bus Request
Welcome A bus request will not change until it is accepted
Motivation
p r o p e r t y BUS_REQUEST_HOLD ;
Basics
@ ( posedge i_clk )
Clocked and $past
( STB)&&(STALL )
k Induction
|=> ( STB)&&( $ s t a b l e ( REQUEST ) ) ;
Bus Properties
endproperty
Free Variables

Abstraction
a s s e r t p r o p e r t y ( BUS_REQUEST_HOLD ) ;
Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

256 / 351
 Ex. Bus Request
Welcome A request persists until it is accepted
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
// R e p e a t up t o MAX STALL c l k s
k Induction
( STB)&&(STALL ) [ ∗ 0 : MAX_STALL ]
Bus Properties
##1 ( STB )&&(! STALL ) ;
Free Variables
endsequence
Abstraction

Invariants
a s s e r t p r o p e r t y ( STB |´> BUS_REQUEST ) ;
Multiple-Clocks

Cover You no longer need to count stalls yourself.

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

257 / 351
 Ex. Bus Request
Welcome A request persists until it is accepted
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
// R e p e a t up t o MAX STALL c l k s
k Induction
( STB)&&(STALL ) [ ∗ 0 : MAX_STALL ]
Bus Properties
##1 ( STB )&&(! STALL ) ;
Free Variables
endsequence
Abstraction

Invariants
a s s e r t p r o p e r t y ( STB |´> BUS_REQUEST ) ;
Multiple-Clocks

Cover You no longer need to count stalls yourself.

Sequences Could we do this with an until statement?
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

257 / 351
 Ex. Bus Request
Welcome A request persists until it is accepted
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
( STB)&&(STALL ) u n t i l ( STB )&&(! STALL ) ;
k Induction
endsequence
Bus Properties

Free Variables
a s s e r t p r o p e r t y ( STB |´> BUS_REQUEST ) ;
Abstraction

Invariants What is the difference?

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

258 / 351
 Ex. Bus Request
Welcome A request persists until it is accepted
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
( STB)&&(STALL ) u n t i l ( STB )&&(! STALL ) ;
k Induction
endsequence
Bus Properties

Free Variables
a s s e r t p r o p e r t y ( STB |´> BUS_REQUEST ) ;
Abstraction

Invariants What is the difference? The until statement goes forever, our
Multiple-Clocks
prior example was limited to MAX_STALL clock cycles.
Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

258 / 351
 Ex. Bus Request
Welcome A request persists until it is accepted
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
( STB)&&(STALL ) u n t i l ( STB )&&(! STALL ) ;
k Induction
endsequence
Bus Properties

Free Variables
a s s e r t p r o p e r t y ( STB |´> BUS_REQUEST ) ;
Abstraction

Invariants What is the difference?

Multiple-Clocks

Cover
But . . . what happens if RESET is asserted?
Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

258 / 351
 Bus Request
Welcome A property can be conditionally disabled
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
// R e p e a t up t o MAX STALL c l k s
k Induction
( STB)&&(STALL ) [ ∗ 0 : MAX_STALL ]
Bus Properties
##1 ( STB )&&(! STALL ) ;
Free Variables
endsequence
Abstraction

Invariants
assert property (
Multiple-Clocks @ ( posedge i_clk )
Cover d i s a b l e iff ( i_reset )
Sequences STB |´> BUS_REQUEST ) ;
Overview
Clocking
Bind The assertion will no longer fail if i_reset clears the request
Ź Sequences
What if the request is aborted?
Questions?

Quizzes

259 / 351
 Ex. Bus Request
Welcome A property can be conditionally disabled
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
// R e p e a t up t o MAX STALL c l k s
k Induction
( STB)&&(STALL ) [ ∗ 0 : MAX_STALL ]
Bus Properties
##1 ( STB )&&(! STALL ) ;
Free Variables
endsequence
Abstraction

Invariants
assert property (
Multiple-Clocks @ ( posedge i_clk )
Cover d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Sequences STB |´> BUS_REQUEST ) ;
Overview
Clocking
Bind Will this work?
Ź Sequences
Questions?

Quizzes

260 / 351
 Ex. Bus Request
Welcome A property can be conditionally disabled
Motivation
sequence BUS_REQUEST ;
Basics
@ ( posedge i_clk )
Clocked and $past
// R e p e a t up t o MAX STALL c l k s
k Induction
( STB)&&(STALL ) [ ∗ 0 : MAX_STALL ]
Bus Properties
##1 ( STB )&&(! STALL ) ;
Free Variables
endsequence
Abstraction

Invariants
assert property (
Multiple-Clocks @ ( posedge i_clk )
Cover d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Sequences STB |´> BUS_REQUEST ) ;
Overview
Clocking
Bind Will this work? Yes!
Ź Sequences
Questions?

Quizzes

260 / 351
 Ex. Bus ACKs
Welcome Some peripherals will only ever accept one request
Motivation
sequence SINGLE_ACK ( MAX_DELAY ) ;
Basics
@ ( posedge i_clk )
Clocked and $past
( ! ACK)&&(STALL ) [ ∗ 0 : MAX_DELAY ]
k Induction
##1 ( ACK )&&(! STALL ) ;
Bus Properties
endsequence
Free Variables

Abstraction
assert property (
Invariants
d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Multiple-Clocks ( STB )&&(! STALL ) |=> SINGLE_ACK ( 3 2 ) ;
Cover );
Sequences
Overview
Clocking
This peripheral will
Bind
Ź Sequences ˝ Stall up to 32 clocks following any accepted request, until it
Questions? ˝ Acknowledges the request, and
Quizzes
˝ Releases the bus on the same cycle

261 / 351
 Ex. Bus ACKs
Welcome Some peripherals will
Motivation
˝ Never stall the bus, and
Basics
˝ Acknowledge every request after a fixed number of clock ticks
Clocked and $past

k Induction p r o p e r t y NEVER_STALL ( DELAY ) ;

Bus Properties @ ( posedge i_clk )
Free Variables d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Abstraction ( STB ) |´> ##[∗DELAY ] ( ACK ) ;
Invariants endproperty
Multiple-Clocks

Cover a s s e r t p r o p e r t y ( NEVER_STALL ( DELAY )

Sequences and ( ! STALL ) ) ;
Overview
Clocking
Bind This is illegal. Can you spot the bug?
Ź Sequences
Questions?

Quizzes

262 / 351
 Ex. Bus ACKs
Welcome Some peripherals will
Motivation
˝ Never stall the bus, and
Basics
˝ Acknowledge every request after a fixed number of clock ticks
Clocked and $past

k Induction p r o p e r t y NEVER_STALL ( DELAY ) ;

Bus Properties @ ( posedge i_clk )
Free Variables d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Abstraction ( STB ) |´> ##[∗DELAY ] ( ACK ) ;
Invariants endproperty
Multiple-Clocks

Cover a s s e r t p r o p e r t y ( NEVER_STALL ( DELAY )

Sequences and ( ! STALL ) ) ;
Overview
Clocking
Bind This is illegal. Can you spot the bug? What logic does the
Ź Sequences
Questions? disable iff apply to?
Quizzes

262 / 351
 Ex. Bus ACKs
Welcome Some peripherals will
Motivation
˝ Never stall the bus, and
Basics
˝ Acknowledge every request after a fixed number of clock ticks
Clocked and $past

k Induction p r o p e r t y NEVER_STALL ( DELAY ) ;

Bus Properties @ ( posedge i_clk )
Free Variables d i s a b l e iff ( ( i_reset ) | | ( ! CYC ) )
Abstraction ( STB ) |´> ##[∗DELAY ] ( ACK ) ;
Invariants endproperty
Multiple-Clocks

Cover a s s e r t p r o p e r t y ( NEVER_STALL ( DELAY ) ) ;

Sequences a s s e r t p r o p e r t y ( ! STALL ) ;
Overview
Clocking
Bind This is valid
Ź Sequences
Questions?

Quizzes

263 / 351
 Ex. Bus ACKs
Welcome Cannot ACK or ERR when no request is pending
Motivation
a s s e r t p r o p e r t y ( @ ( posedge i_clk )
Basics
( ( ! i_CYC ) | | ( i_reset ) )
Clocked and $past
##1 ( ( ! i_CYC ) | | ( i_reset ) )
k Induction
|´> ( ( ! o_ACK )&&(! o_ERR ) ) ;
Bus Properties

Free Variables
Or as we did it before
Abstraction

Invariants always @ ( posedge i_clk )

Multiple-Clocks
i f ( ( f_past_valid )
Cover
&&(( $past ( i_reset ) ) | | ( ! $past ( i_CYC ) ) )
Sequences
&&((i_reset ) | | ( ! i_CYC ) )
Overview a s s e r t ( ( ! o_ACK )&&(! o_ERR ) ) ;
Clocking
Bind
Ź Sequences
Which is simpler to understand?
Questions?

Quizzes

264 / 351
 Ex. UART Tx
Welcome Let’s look at an serial port transmitter example.
Motivation A baud interval is CKS clocks . . .
Basics
˝ Output data is constant
Clocked and $past
˝ Logic doesn’t change state
k Induction

Bus Properties
˝ Internal shift register value is known
Free Variables ˝ Ends with zero_baud_counter
Abstraction

Invariants sequence BAUD_INTERVAL ( CKS , DAT , SR , ST ) ;

Multiple-Clocks
( ( o_uart_tx == DAT)&&(state == ST )
Cover
&&(lcl_data == SR )
Sequences
&&(! zero_baud_counter ) ) [ ∗ ( CKS ´1)]
Overview ##1 ( o_uart_tx == DAT)&&(state == ST )
Clocking &&(lcl_data == SR )
Bind
Ź Sequences &&(zero_baud_counter ) )
Questions? endsequence
Quizzes

265 / 351
 Ex. UART Tx
Welcome A byte consists of 10 Baud intervals
Motivation
sequence SEND ( CKS , DATA ) ;
Basics
BAUD_INTERVAL ( CKS , 1 ’ b0 , DATA , 4 ’ h0 )
Clocked and $past
##1 BAUD_INTERVAL ( CKS , DATA [ 0 ] ,
k Induction
{ { ( 1 ) { 1 ’ b1 } } , DATA [ 7 : 1 ] , 4 ’ h1 )
Bus Properties
##1 BAUD_INTERVAL ( CKS , DATA [ 1 ] ,
Free Variables
{ { ( 2 ) { 1 ’ b1 } } , DATA [ 7 : 2 ] , 4 ’ h2 )
Abstraction
//
Invariants
##1 BAUD_INTERVAL ( CKS , DATA [ 6 ] ,
Multiple-Clocks { { ( 7 ) { 1 ’ b1 } } , DATA [ 7 ] , 4 ’ h7 )
Cover ##1 BAUD_INTERVAL ( CKS , DATA [ 7 ] ,
Sequences 7 ’ hff , DATA [ 7 ] , 4 ’ h8 )
Overview
Clocking
##1 BAUD_INTERVAL ( CKS , 1 ’ b1 , 8 ’ hff , 4 ’ h9 ) ;
Bind endsequence
Ź Sequences
Questions?

Quizzes

266 / 351
 Ex. UART Tx
Welcome Transmitting a byte requires
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( i_wr )&&(! o_busy ) )
Clocked and $past
fsv_data <= i_data ;
k Induction

Bus Properties
a s s e r t p r o p e r t y ( @ ( posedge i_clk )
Free Variables
( i_wr )&&(! o_busy )
Abstraction
|=> ( ( o_busy ) throughout
Invariants
SEND ( CLOCKS_PER_BAUD , fsv_data ) )
Multiple-Clocks ##1 ( ( ! o_busy)&&(o_uart_tx )
Cover &&(zero_baud_counter ) ) ;
Sequences
Overview
Clocking
Bind
˝ A transmit request is received
Ź Sequences ˝ The data is sent
Questions?
˝ The controller returns to idle
Quizzes

267 / 351
 Ex. UART Tx
Welcome Transmitting a byte requires
Motivation
a s s e r t p r o p e r t y ( @ ( posedge i_clk )
Basics
( i_wr )&&(! o_busy )
Clocked and $past
|=> ( ( o_busy ) throughout
k Induction
SEND ( CLOCKS_PER_BAUD , fsv_data ) )
Bus Properties
##1 ( ( ! o_busy)&&(o_uart_tx )
Free Variables
&&(zero_baud_counter ) ) ;
Abstraction

Invariants Make sure . . .

Multiple-Clocks

Cover
˝ The sequence has a defined beginning
Sequences Only ever triggered once at a time
Overview ˝ Doesn’t reference changing data
Clocking
Bind ˝ throughout is within parenthesis
Ź Sequences
˝ You tie all relevant state information together
Questions?

Quizzes

268 / 351
 SymbiYosys
Welcome Using SystemVerilog Assertions with Yosys requires Verific
Motivation
[ options ]
Basics
mode prove
Clocked and $past
[ engines ]
k Induction
smtbmc
Bus Properties
[ script ]
Free Variables
#
Abstraction
#
Invariants
read ´formal module . v
Multiple-Clocks # . . . o t h e r f i l e s would go h e r e
Cover prep ´top module
Sequences opt_merge ´share_all
Overview
Clocking
Bind [ files ]
Ź Sequences
. . / demo´rtl / module . v
Questions?

Quizzes

269 / 351
 SymbiYosys
Welcome Using SystemVerilog Assertions with Yosys requires Verific
Motivation
[ options ]
Basics
mode prove
Clocked and $past
[ engines ]
k Induction
smtbmc
Bus Properties
[ script ]
Free Variables
# The read command works both with and without Verific
Abstraction
# SymbiYosys script doesn’t change therefore
Invariants
read ´formal module . v
Multiple-Clocks # . . . o t h e r f i l e s would go h e r e
Cover prep ´top module
Sequences opt_merge ´share_all
Overview
Clocking
Bind [ files ]
Ź Sequences
. . / demo´rtl / module . v
Questions?

Quizzes

269 / 351
 SysVerilog Conclusions
Welcome SystemVerilog Concurrent Assertions . . .
Motivation
˝ can be very powerful
Basics
˝ can be very confusing
Clocked and $past
˝ can be used with immediate assertions
k Induction

Bus Properties
You can keep using the simpler property form we’ve been
Free Variables using
Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

270 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation
module sfifo ( i_clk , i_reset ,
Basics
i_wr , i_data , o_full ,
Clocked and $past
i_rd , o_data , o_empty ,
k Induction
o_err ) ;
Bus Properties
// . . .
Free Variables
‘ i f d e f FORMAL
Abstraction
// P r o p e r t i e s u n d e r s t o o d by e i t h e r
Invariants
// Y o s y s o r V e r i f i c
Multiple-Clocks // . . . .
Cover ‘endif
Sequences ‘ i f d e f VERIFIC_SVA
Overview
Clocking
// V e r i f i c ´o n l y p r o p e r t i e s
Bind // . . . .
Ź Sequences
‘endif
Questions?
endmodule
Quizzes

271 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

272 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics
˝ Should never go from full to empty
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

272 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics
˝ Should never go from full to empty except on a reset
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

272 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics
˝ Should never go from full to empty except on a reset
Clocked and $past
˝ Should never go from empty to full
k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

272 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics
˝ Should never go from full to empty except on a reset
Clocked and $past
˝ Should never go from empty to full
k Induction

Bus Properties
˝ The two outputs, o_empty and o_full, should properly reflect
Free Variables the size of the FIFO
Abstraction
– o_empty means the FIFO is currently empty
Invariants
– o_full means the FIFO has 2N elements within it
Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Ź Sequences
Questions?

Quizzes

272 / 351
 Last Exercise
Welcome Let’s formally verify a synchronous FIFO
Motivation What properties do you think would be appropriate?
Basics
˝ Should never go from full to empty except on a reset
Clocked and $past
˝ Should never go from empty to full
k Induction

Bus Properties
˝ The two outputs, o_empty and o_full, should properly reflect
Free Variables the size of the FIFO
Abstraction
– o_empty means the FIFO is currently empty
Invariants
– o_full means the FIFO has 2N elements within it
Multiple-Clocks

Cover ˝ Challenge: Use sequences to prove that

Sequences
Overview – Given any two values written successfully
Clocking – Verify that those two values can (some time later) be read
Bind
Ź Sequences successfully, and in the right order
Questions?
(Unless a reset takes place in the meantime)
Quizzes

272 / 351
 Hint
Welcome When using sequences,. . .
Motivation
˝ It can be very difficult to figure out what part of the
Basics
sequence failed.
Clocked and $past

k Induction
The assertion that fails will reference the entire failing
Bus Properties
sequence.
Free Variables
Suggestions:
Abstraction

Invariants
˝ Sequences must be triggered
Multiple-Clocks Be aware of what triggers a sequence
Cover ˝ Use combinational logic to define wires that will then
Sequences represent steps in the sequence
Overview
Clocking ˝ Build the sequences out of these wires
Bind
Ź Sequences
Questions?

Quizzes

273 / 351
 Hint continued
Welcome Here’s an example:
Motivation
w i r e f_a , f_b , f_c ;
Basics
//
Clocked and $past
a s s i g n f_a = // y o u r l o g i c
k Induction
a s s i g n f_b = // y o u r l o g i c
Bus Properties
a s s i g n f_c = // y o u r l o g i c
Free Variables
//
Abstraction
sequence ARBITRARY_EXAMPLE_SEQUENCE
Invariants
f_a [ ∗ 0 : 4 ] ##1 f_b ##1 f_c [ ∗ 1 2 : 1 6 ] ;
Multiple-Clocks endsequence
Cover

Sequences If you use this approach

Overview
Clocking ˝ Interpreting the wave file will be much easier
Bind
Ź Sequences ˝ The f_a, etc., lines will be in the trace
Questions?

Quizzes

274 / 351
 Questions?
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences
Overview
Clocking
Bind
Sequences
Ź Questions?

Quizzes

275 / 351
Welcome

Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction
Quizzes
Invariants

Multiple-Clocks

Cover

Sequences

Ź Quizzes

276 / 351
 Quiz #1
Welcome Will the assertion below ever fail?
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
always @ ( posedge clk )
Bus Properties
counter <= counter + 1 ’ b1 ;
Free Variables

Abstraction
always @ ( ∗ )
Invariants
begin
Multiple-Clocks a s s e r t ( counter <= 1 0 0 ) ;
Cover assume ( counter <= 9 0 ) ;
Sequences end
Quizzes

277 / 351
 Answer #1
Welcome No, it will never fail.
Motivation The assumption will prohibit the assertion from being evaluated.
Basics
always @ ( ∗ )
Clocked and $past
begin
k Induction
a s s e r t ( counter <= 1 0 0 ) ;
Bus Properties
assume ( counter <= 9 0 ) ;
Free Variables
end
Abstraction

Invariants
This is an example of what I call a careless asumption.
Multiple-Clocks

Cover

Sequences

Quizzes

278 / 351
 Quiz #2
Welcome Will this simple counter ever pass formal verification?
Motivation
parameter [ 1 5 : 0 ] MAX_AMOUNT = 2 2 ;
Basics
reg [ 1 5 : 0 ] counter ;
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
i f ( ( i_start_signal)&&(counter == 0 ) )
Free Variables
counter <= MAX_AMOUNT ´1’b1 ;
Abstraction
e l s e i f ( counter != 0 )
Invariants
counter <= counter ´ 1 ;
Multiple-Clocks

Cover always @ ( ∗ )
Sequences o_busy = ( counter != 0 ) ;
Quizzes

‘ifdef FORMAL
always @ ( ∗ )
a s s e r t ( counter < MAX_AMOUNT ) ;
‘endif

279 / 351
 Answer #2
Welcome This design just needs an initial counter value to pass
Motivation
parameter [ 1 5 : 0 ] MAX_AMOUNT = 2 2 ;
Basics
reg [ 1 5 : 0 ] counter = 0 ;
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
i f ( ( i_start_signal)&&(counter == 0 ) )
Free Variables
counter <= MAX_AMOUNT ´1’b1 ;
Abstraction
e l s e i f ( counter != 0 )
Invariants
counter <= counter ´ 1 ;
Multiple-Clocks

Cover always @ ( ∗ )
Sequences o_busy = ( counter != 0 ) ;
Quizzes

‘ifdef FORMAL
always @ ( ∗ )
a s s e r t ( counter < MAX_AMOUNT ) ;
‘endif

280 / 351
 Quiz #3
Welcome Will the following design pass formal verification?
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
always @ ( posedge clk )
Bus Properties
i f ( counter == 1 6 ’ d22 )
Free Variables
counter <= 0 ;
Abstraction
else
Invariants
counter <= counter + 1 ’ b1 ;
Multiple-Clocks

Cover always @ ( ∗ )
Sequences a s s e r t ( counter != 1 6 ’ d500 ) ;
Quizzes

281 / 351
 Answer #3
Welcome The following approach will pass both BMC and induction.
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
always @ ( posedge i_clk )
Bus Properties
i f ( i_reset ) // Keep ASIC d e s i g n e r s happy
Free Variables
counter <= 0 ;
Abstraction
e l s e i f ( counter == 1 6 ’ d22 )
Invariants
counter <= 0 ;
Multiple-Clocks else
Cover counter <= counter + 1 ’ b1 ;
Sequences

Quizzes // The c o r r e c t a s s e r t i o n s h o u l d r e f e r e n c e
// a l l o f t h e u n r e a c h a b l e c o u n t e r v a l u e s
always @ ( ∗ )
a s s e r t ( counter <= 1 6 ’ d22 ) ;

282 / 351
 Quiz #4
Welcome Will the following design pass formal verification?
Motivation
i n i t i a l counter = 0 ;
Basics
always @ ( posedge i_clk )
Clocked and $past
i f ( ( i_start_signal)&&(counter == 0 ) )
k Induction
counter <= 2 3 ;
Bus Properties
e l s e i f ( counter != 0 )
Free Variables
counter <= counter ´ 1 ’ b1 ;
Abstraction

Invariants
always @ ( ∗ )
Multiple-Clocks a s s e r t ( counter < 2 4 ) ;
Cover always @ ( ∗ )
Sequences assume ( ! i_start_signal ) ;
Quizzes

always @ ( posedge i_clk )

a s s e r t ( $past ( counter == 0 ) ) ;

283 / 351
 Answer #4
Welcome If you replace assert($past(counter==0)); with
Motivation assert(counter==0);, then this design passes.
Basics
i n i t i a l counter = 0 ;
Clocked and $past
always @ ( posedge i_clk )
k Induction
i f ( ( i_start_signal)&&(counter == 0 ) )
Bus Properties
counter <= 2 3 ;
Free Variables
e l s e i f ( counter != 0 )
Abstraction
counter <= counter ´ 1 ’ b1 ;
Invariants

Multiple-Clocks
always @ ( ∗ )
Cover
a s s e r t ( counter < 2 4 ) ;
Sequences
always @ ( ∗ )
Quizzes
assume ( ! i_start_signal ) ;

always @ ( posedge i_clk )

a s s e r t ( counter == 0 ) ;

284 / 351
 Quiz #5
Welcome How are the following two assertions different?
Motivation
i n i t i a l f_past_valid = 1 ’ b0 ;
Basics
always @ ( posedge i_clk )
Clocked and $past
f_past_valid <= 1 ’ b1 ;
k Induction

Bus Properties
always @ ( posedge i_clk )
Free Variables
i f ( ( f_past_valid)&&( $past ( o_wb_stb ) )
Abstraction
&&($past ( i_wb_stall ) ) )
Invariants
a s s e r t ( ( o_wb_stb )
Multiple-Clocks &&($ s t a b l e ( { i_wb_addr , i_wb_we } ) ) ) ;
Cover

Sequences
a s s e r t p r o p e r t y ( @ ( posedge i_clk )
Quizzes
( o_wb_stb)&&(i_wb_stall )
|=> o_wb_stb
&&($ s t a b l e ( { i_wb_addr , i_wb_we } ) ) ) ;

285 / 351
 Answer #5
Welcome ˝ The first assertion was an “immediate” assertion, the second
Motivation a “concurrent assertion”.
Basics ˝ The free version of Yosys does not support concurrent
Clocked and $past assertions.
k Induction
˝ The second assertion is easier to read
Bus Properties

Free Variables
a s s e r t p r o p e r t y ( @ ( posedge i_clk )
Abstraction
( o_wb_stb)&&(i_wb_stall )
Invariants
|=> o_wb_stb
Multiple-Clocks
&&($ s t a b l e ( { i_wb_addr , i_wb_we } ) ) ) ;
Cover

Sequences
Functionally, the two assertions are identical!
Quizzes

286 / 351
 Quiz #6
Welcome When using multiclock techniques, which of the below
Motivation descriptions describes a signal that only changes on the positive
Basics edge of a clock?
Clocked and $past

k Induction
always @ ( $ g l o b a l c l o c k )
Bus Properties
i f ( $ f e l l ( i_clk ) )
Free Variables
a s s e r t ( $ s t a b l e ( signal ) ) ;
Abstraction

Invariants always @ ( $ g l o b a l c l o c k )
Multiple-Clocks i f ( ! $ros e ( i_clk ) )
Cover a s s e r t ( $ s t a b l e ( signal ) ) ;
Sequences

Quizzes always @ ( $ g l o b a l c l o c k )
i f ( ! $past ( i_clk ) )
a s s e r t ( $ s t a b l e ( signal ) ) ;

287 / 351
 Answer #6
Welcome The correct way to assert that a signal will only change on a
Motivation positive clock edge requires asserting that the signal will be
Basics stable in all other cases.
Clocked and $past

k Induction
always @ ( $ g l o b a l c l o c k )
Bus Properties
i f ( ( f_past_valid_gbl )&&(! $ros e ( i_clk ) ) )
Free Variables
a s s e r t ( $ s t a b l e ( signal ) ) ;
Abstraction
Be aware, $rose() depends upon the $past(), so don’t forget an
Invariants
f_past_valid signal!
Multiple-Clocks

Cover
With $global clock, I like to call it f_past_valid_gbl, and define
Sequences it as,
Quizzes
reg f_past_valid_gbl = 1 ’ b0 ;
always @ ( $ g l o b a l c l o c k )
f_past_valid_gbl <= 1 ’ b1 ;

288 / 351
 Quiz #7
Welcome Will this simple counter ever pass formal verification?
Motivation
reg [ 1 5 : 0 ] counter = 0 ;
Basics

Clocked and $past

always @ ( posedge i_clk )
k Induction
i f ( ( i_start_signal)&&(counter == 0 ) )
Bus Properties
counter <= 2 1 ;
Free Variables
e l s e i f ( counter != 0 )
Abstraction
counter <= counter ´ 1 ;
Invariants

Multiple-Clocks always @ ( ∗ )
Cover o_busy = ( counter != 0 ) ;
Sequences

Quizzes always @ ( posedge i_clk )

i f ( $past ( i_start_signal ) )
a s s e r t ( counter == 2 1 ) ;

289 / 351
 Answer #7
Welcome No, the assertion would not pass: it neither checked for the past
Motivation counter == 0, nor did it make sure $past() was valid.
Basics The modified assertion, below, will pass.
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
i f ( ( f_past_valid )
Free Variables
&&($past ( i_start_signal ) )
&&($past ( counter ) == 0 ) )
Abstraction
a s s e r t ( counter == 2 1 ) ;
Invariants

Multiple-Clocks
Alternatively, the following concurrent assertion would also work:
Cover

Sequences a s s e r t p r o p e r t y @ ( posedge i_clk )

Quizzes ( i_start_signal)&&(counter == 0 )
|=> ( counter == 2 1 ) ;

This exercise is a good example of how formal methods force you

to look just a little harder at a problem.

290 / 351
 Quiz #8
Welcome Will this design pass a Bounded Model Check (BMC)?
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
always @ ( posedge clk )
Bus Properties
counter <= counter + 1 ’ b1 ;
Free Variables

Abstraction
always @ ( ∗ )
Invariants
a s s e r t ( counter < 1 6 ’ d65000 ) ;
Multiple-Clocks

Cover

Sequences

Quizzes

291 / 351
 Answer #8
Welcome Will this design pass a Bounded Model Check (BMC)?
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

i n i t i a l counter = 0 ;
k Induction
always @ ( posedge clk )
Bus Properties
counter <= counter + 1 ’ b1 ;
Free Variables

Abstraction
always @ ( ∗ )
Invariants
a s s e r t ( counter < 1 6 ’ d65000 ) ;
Multiple-Clocks

Cover Not unless you prove it with a depth of over 65,000!

Sequences
This is a classic example of a proof that is easier to do with
Quizzes
induction. Less than five steps of induction would find this
problem.

292 / 351
 Quiz #9
Welcome Will the following design pass formal verification?
Motivation
reg [15:0] counter ;
Basics

Clocked and $past

always @ ( ∗ )
k Induction
begin
Bus Properties
counter = 2 ;
Free Variables
a s s e r t ( counter == 5 ) ;
Abstraction
counter = counter + 3 ;
Invariants
end
Multiple-Clocks

Cover

Sequences

Quizzes

293 / 351
 Answer #9
Welcome Will the following design pass formal verification?
Motivation
always @ ( ∗ )
Basics
begin
Clocked and $past
counter = 2 ;
k Induction
a s s e r t ( counter == 5 ) ;
Bus Properties
counter = counter + 3 ;
Free Variables
end
Abstraction

Invariants No, it will not pass.

Multiple-Clocks

Cover
˝ counter = 2 is a blocking statement. It is completed before
Sequences the assert() .
Quizzes ˝ counter==2 when the assert is applied
˝ Only after the assert is counter set to 5.
˝ Were the assert the last line of the block, it would’ve passed
˝ This is one reason why I separate my assertions from my logic

294 / 351
 Quiz #10
Welcome Goal: to prove that whenever a request is being made, the
Motivation request will stay stable until it is accepted.
Basics Will this assertion capture what we want?
Clocked and $past

k Induction
i f ( ( $past ( o_REQUEST ))&&( $past ( i_STALL ) ) )
Bus Properties
begin
Free Variables
a s s e r t ( o_REQUEST ) ;
a s s e r t ( $ s t a b l e ( o_REQUEST_DETAILS ) ) ;
Abstraction
end
Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

295 / 351
 Answer #10
Welcome Not quite, there’s a couple of things missing
Motivation Two examples would be i_reset and f_past_valid
Basics Here’s an updated assertion that should fix those lacks
Clocked and $past

k Induction
i f ( ( f_past_valid )&&(! $past ( i_reset ) )
Bus Properties
&&($past ( o_REQUEST ))&&( $past ( i_STALL ) ) )
Free Variables
begin
a s s e r t ( o_REQUEST ) ;
Abstraction
a s s e r t ( $ s t a b l e ( o_REQUEST_DETAILS ) ) ;
Invariants
end
Multiple-Clocks

Cover
Alternatively, we could have written,
Sequences

Quizzes a s s e r t p r o p e r t y @ ( posedge i_clk )

d i s a b l e iff ( i_reset )
( o_REQUEST)&&(i_STALL )
|=> ( o_REQUEST )
&&($ s t a b l e ( o_REQUEST_DETAILS ) ) ;

296 / 351
 Quiz #11
Welcome The following design fails induction. How would you adjust it so
Motivation that it would pass?
Basics
reg [15:0] sa = 0 , sb = 0 ;
Clocked and $past

k Induction
always @ ( posedge i_clk )
Bus Properties
i f ( i_ce )
Free Variables
begin
Abstraction
sa <= { sa [ 1 4 : 0 ] , i_bit } ;
Invariants
sb <= { i_bit , sb [ 1 5 : 1 ] } ;
Multiple-Clocks
end
Cover

Sequences
always @ ( ∗ )
Quizzes
a s s e r t ( sa [ 1 5 ] == sb [ 0 ] ) ;

297 / 351
 Answer #11
Welcome There are many solutions to this problem
Motivation
1. Use a non-smtbmc engine, such as abc pdr
Basics
2. Force i_ce
Clocked and $past

k Induction always @ ( posedge i_clk )

Bus Properties i f ( ! $past ( i_ce ) )
Free Variables assume ( i_ce )
Abstraction

Invariants 3. Assert all bits

Multiple-Clocks
always @ ( ∗ )
Cover
begin
Sequences
a s s e r t ( sa [ 1 4 ] == sb [ 1 ] ) ;
Quizzes
a s s e r t ( sa [ 1 3 ] == sb [ 2 ] ) ;
a s s e r t ( sa [ 1 2 ] == sb [ 3 ] ) ;
a s s e r t ( sa [ 1 1 ] == sb [ 4 ] ) ;
// . . . t h r o u g h a l l c o m b i n a t i o n s

298 / 351
 Quiz #12
Welcome The logic below is designed to ensure that the design will only
Motivation acknowledge requests and nothing more: one acknowledgment
Basics per request. It almost works. Can you spot any problem(s)?
Clocked and $past

k Induction
i n i t i a l f_nreqs = 0 ;
Bus Properties
always @ ( posedge i_clk )
Free Variables
i f ( ( i_reset ) | | ( ! i_wb_cyc ) )
f_nreqs <= 1 ’ b0 ;
Abstraction
e l s e i f ( ( i_wb_stb )&&(! o_wb_stall ) )
Invariants
f_nreqs <= f_nreqs + 1 ’ b1 ;
Multiple-Clocks
// f n a c k i s a s i m i l a r l y d e f i n e d c o u n t e r ,
Cover
// o n l y one t h a t c o u n t s a c k n o w l e d g m e n t s
Sequences
always @ ( ∗ )
Quizzes
i f ( f_nreqs == f_nacks )
a s s e r t ( ! o_wb_ack ) ;

Assume a sufficient number of bits in f_nreqs and f_nacks.

299 / 351
 Answer #12
Welcome No, it will not pass. The problem is that it may be possible to
Motivation ACK a request on the same clock it is received. The following
Basics updated assertion will fix this.
Clocked and $past

k Induction
always @ ( ∗ )
Bus Properties
i f ( ( f_nreqs == f_nacks )
Free Variables
&&((! i_wb_stb ) | | ( o_wb_stall ) ) )
a s s e r t ( ! o_wb_ack ) ;
Abstraction

Invariants
Originally, I disallowed ACK’s on the same clock as the STB.
Multiple-Clocks
Then I tried formally verifying someone else’s code. When it
Cover

Sequences
didn’t pass, I went back and re-read the WB-spec only to
Quizzes discover the error in my ways.

300 / 351
 Quiz #13
Welcome Given that X is defined somehow, which of the following
Motivation assertions will fail?
Basics
always @ ( posedge i_clk )
Clocked and $past
i f ( f_past_valid )
k Induction
begin
Bus Properties
assert ( $stable (X)
Free Variables
== ( X == $past ( X ) ) ) ;
Abstraction
a s s e r t ( $changed ( X )
Invariants
== ( X != $past ( X ) ) ) ;
Multiple-Clocks
a s s e r t ( $ros e ( X )
Cover
== ( ( X )&&(! $past ( X ) ) ) ) ;
Sequences
assert ( $ f e l l (X)
Quizzes
== ( ( ! X)&&( $past ( X ) ) ) ) ;
end

301 / 351
 Answer #13
Welcome Two of these assertions will fail if X is wider than one bit
Motivation
a s s e r t ( $ros e ( X ) == ( ( X )&&(! $past ( X ) ) ) ) ;
Basics
a s s e r t ( $ f e l l ( X ) == ( ( ! X)&&( $past ( X ) ) ) ) ;
Clocked and $past

k Induction
From the 2012 SystemVerilog standard,
Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks
These updated assertions will succeed,
Cover

Sequences a s s e r t ( $ros e ( X ) == ( ( X [ 0 ] ) & & ( ! $past ( X [ 0 ] ) ) ) ) ;

Quizzes a s s e r t ( $ f e l l ( X ) == ( ( ! X [ 0 ] ) & & ( $past ( X [ 0 ] ) ) ) ) ;

302 / 351
 Quiz #14
Welcome The following logic creates two clocks with nearly identical
Motivation frequencies. Can you spot any missing assumptions?
Basics
( ∗ anyconst ∗ ) reg [ 7 : 0 ] f_step_one , f_step_two ;
Clocked and $past
always @ ( ∗ )
k Induction
i f ( f_step_one > f_step_two )
Bus Properties
assume ( f_step_one ´ f_step_two < 8 ’ h2 )
Free Variables
else
Abstraction
assume ( f_step_two ´ f_step_one < 8 ’ h2 )
Invariants
always @ ( $ g l o b a l c l o c k )
Multiple-Clocks
begin
Cover
f_counter_one <= f_counter_one + f_step_one ;
Sequences
f_counter_two <= f_counter_two + f_step_two ;
Quizzes
//
assume ( i_clk_one == f_counter_one [ 7 ] ) ;
assume ( i_clk_two == f_counter_two [ 7 ] ) ;
end

303 / 351
 Answer #14
Welcome The step sizes cannot ever be zero, and steps greater than 8’h80
Motivation will alias.
Basics
always @ ( ∗ )
Clocked and $past
begin
k Induction
assume ( f_step_one != 0);
Bus Properties
assume ( f_step_two != 0);
Free Variables
assume ( f_step_one <= 8 ’ h80 ) ;
Abstraction
assume ( f_step_two <= 8 ’ h80 ) ;
Invariants
end
Multiple-Clocks

Cover
For performance reasons, you may choose to assume the speed
Sequences
of the fastest clock.
Quizzes
always @ ( ∗ )
assume ( ( f_step_one == 8 ’ h80 )
| | ( f_step_two == 8 ’ h80 ) ) ;

304 / 351
 Quiz #15
Welcome Will the following assertion pass?
Motivation
always @ ( posedge i_clk )
Basics
begin
Clocked and $past
i f ( i_write )
k Induction
mem [ i_waddr ] <= i_data ;
Bus Properties
i f ( i_read )
Free Variables
o_data <= mem [ i_raddr ] ;
Abstraction
end
Invariants

Multiple-Clocks always @ ( posedge i_clk )

Cover i f ( ( f_past_valid )
Sequences &&($past ( i_write ))&&( $past ( i_read ) )
Quizzes &&($past ( i_waddr)==$past ( i_raddr ) ) )
a s s e r t ( o_data == $past ( i_data ) ) ;

305 / 351
 Answer #15
Welcome Will the following assertion pass?
Motivation
always @ ( posedge i_clk )
Basics
begin
Clocked and $past
i f ( i_write )
k Induction
mem [ i_waddr ] <= i_data ;
Bus Properties
i f ( i_read )
Free Variables
o_data <= mem [ i_raddr ] ;
Abstraction
end
Invariants

Multiple-Clocks always @ ( posedge i_clk )

Cover i f ( ( f_past_valid )
Sequences &&($past ( i_write ))&&( $past ( i_read ) )
Quizzes &&($past ( i_waddr)==$past ( i_raddr ) ) )
a s s e r t ( o_data == $past ( i_data ) ) ;

No.
How would you describe a write–through block RAM?

306 / 351
 Quiz #16
Welcome The formal property below was written for the case of a
Motivation synchronous reset. How would you adjust it so that it accurately
Basics reflects the behavior of the flip-flop under an asynchronous reset?
Clocked and $past

k Induction
always @ ( posedge i_clk , negedge i_areset_n )
Bus Properties
i f ( ! i_areset_n )
Free Variables
a <= 0 ;
else
Abstraction
a <= something ;
Invariants

Multiple-Clocks
always @ ( posedge i_clk )
Cover
i f ( ( f_past_valid)&&( $past ( i_areset_n ) )
Sequences
a s s e r t ( a == $past ( something ) ) ;
Quizzes

307 / 351
 Answer #16
Welcome The following assertion can be used to describe the response of
Motivation logic to a negative logic asynchronous reset.
Basics
always @ ( posedge i_clk , negedge i_areset_n )
Clocked and $past
i f ( ! i_areset_n )
k Induction
a <= 0 ;
Bus Properties
else
Free Variables
a <= something ;
Abstraction

Invariants
always @ ( posedge i_clk )
Multiple-Clocks
i f ( ! i_areset_n )
Cover
a s s e r t ( a == 0 ) ;
Sequences
e l s e i f ( ( f_past_valid)&&( $past ( i_areset_n ) )
Quizzes
a s s e r t ( a == $past ( something ) ) ;

Don’t forget to assume an initial reset!

i n i t i a l assume ( ! i_areset_n ) ;

308 / 351
 Quiz #17
Welcome Your design passes a bounded model check (BMC), but fails
Motivation during induction. Upon inspection, you find a failure in section A
Basics (below) of your trace.
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants
How should you address this problem?
Multiple-Clocks

Cover

Sequences

Quizzes

309 / 351
 Answer #17
Welcome Your design passes a bounded model check (BMC), but fails
Motivation during induction. Upon inspection, you find a failure in section A
Basics (below) of your trace.
Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants
How should you address this problem?
Multiple-Clocks
This is not a problem with your logic. Rather, the formal
Cover

Sequences
properties that are constraining your logic are insufficient
Quizzes ˝ You need more properties to keep the design from failing
˝ If an input is out of bounds, assume it will be within bounds
˝ If your design starts in an invalid state, assert such invalid
states will never happen
˝ initial statements will not help during induction

310 / 351
 Quiz #18
Welcome Your design fails in section C (below) of your trace.
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables Upon inspection, you discover an

Abstraction
always @(posedge i_clk) assume(X); property is not getting
Invariants
applied.
Multiple-Clocks
How would you fix this situation?
Cover

Sequences

Quizzes

311 / 351
 Quiz #18
Welcome An always @(posedge i_clk) assume(X); property is not getting
Motivation applied, causing your design to fail in section C of your trace
Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction The problem is that always @(posedge i_clk) properties are not
Invariants
applied until the the next clock edge (i.e. section B of the trace)
Multiple-Clocks

Cover ˝ This can cause an always @(∗) assert(Y); to fail in section C

Sequences
How would you fix this situation?
Quizzes
˝ You can make the always @(∗) property a clocked property
˝ You can evaluate the always @(posedge i_clk) assumption as
an always @(∗) assumption instead
– You might need to create your own $past value to do this

312 / 351
 Quiz #19
Welcome Will the following design pass formal verification?
Motivation
reg [ 1 5 : 0 ] counter = 0 ;
Basics
always @ ( posedge i_clk )
Clocked and $past
i f ( i_reset )
k Induction
counter <= 0 ;
Bus Properties
else
Free Variables
counter <= counter + 1 ;
Abstraction

Invariants
always @ ( ∗ )
Multiple-Clocks i f ( counter > 2 )
Cover assume ( i_reset ) ;
Sequences

Quizzes a s s e r t p r o p e r t y ( @ ( posedge i_clk )

d i s a b l e iff ( i_reset )
( counter < 2 ) ) ;
endproperty

313 / 351
 Answer #19
Welcome Much to my own surprise, this design will pass a formal check.
Motivation

Basics

Clocked and $past

k Induction

Bus Properties

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover
This is roughly equivalent to:
Sequences

Quizzes reg check = 1 ;

always @ ( posedge i_clk )
check <= ( counter < 2 ) | | ( i_reset ) ;
always @ ( ∗ )
i f ( ! i_reset ) a s s e r t ( check ) ;

314 / 351
 Quiz #20
Welcome Consider the following trace from an asynchronous context:
Motivation

Basics i clk
Clocked and $past f past valid
k Induction
o value
Bus Properties

Free Variables

Abstraction
Will this formal stability assertion pass or fail?
Invariants always @ ( posedge i_clk )
Multiple-Clocks i f ( f_past_valid )
Cover a s s e r t ( $ s t a b l e ( o_value ) ) ;
Sequences

Quizzes

315 / 351
 Answer #20
Welcome Yes, this stability assertion will hold.
Motivation

Basics
i clk
Clocked and $past f past valid
k Induction o value
Bus Properties

Free Variables ˝ Note that everytime $rose(i_clk) is true, $past(o_value) is

Abstraction
also true.
Invariants
˝ Since the check is only accomplished on the positive edge of
Multiple-Clocks
i_clk, o_value is only checked at this time.
Cover
˝ Since $past(o_value) is always true just prior to
Sequences

Quizzes
@(posedge i_clk), the assertion passes

always @ ( posedge i_clk )

i f ( f_past_valid )
a s s e r t ( $ s t a b l e ( o_value ) ) ;

316 / 351
 Quiz #21
Welcome Your design contains the following generate block:
Motivation
parameter [ 0 : 0 ] A = 1 ;
Basics
parameter [ 0 : 0 ] B = 1 ;
Clocked and $past
// . . .
k Induction
generate i f ( A )
Bus Properties
begin : A_BLOCK
Free Variables
// Some l o g i c
Abstraction
end e l s e i f ( B )
Invariants
begin : B_BLOCK
Multiple-Clocks // Some o t h e r l o g i c
Cover end e l s e begin : ELSE_BLOCK
Sequences // Some f i n a l s e t o f l o g i c
Quizzes end endgenerate

How should this impact the design of your SymbiYosys

configuration file?

317 / 351
 Answer #21
Welcome How should conditional generate blocks be handled?
Motivation
˝ By creating a separate task for each parameter set
Basics
˝ Each set of parameters can then be verified independently
Clocked and $past

k Induction
[ tasks ]
Bus Properties
A
Free Variables
B
Abstraction
Other
Invariants
[ script ]
Multiple-Clocks
# ...
Cover
read ´formal toplvl . v
Sequences
A : chparam ´set A 1 toplvl
Quizzes
˜A : chparam ´set A 0 toplvl
B : chparam ´set B 1 toplvl
˜B : chparam ´set B 0 toplvl
prep ´top toplvl
# ...

318 / 351
 Quiz #22
Welcome When working with cover(), how do you handle a failure?
Motivation
˝ On a cover() success a trace is generated.
Basics
No trace is generated on a cover() failure.
Clocked and $past
˝ At first glance, you have nothing to go with
k Induction

Bus Properties How do you debug your design in this situation?

Free Variables

Abstraction

Invariants

Multiple-Clocks

Cover

Sequences

Quizzes

319 / 351
 Answer #22
Welcome When working with cover(), how do you handle a failure?
Motivation
˝ Suppose your design needs to accomplish a sequence of steps,
Basics
and then cover the last one.
Clocked and $past

k Induction always @ ( ∗ )
Bus Properties cover ( step_24 ) ;
Free Variables

Abstraction ˝ How shall you debug this failure?

Invariants
Solution: cover the intermediate steps
Multiple-Clocks

Cover always @ ( ∗ )
Sequences begin
Quizzes cover ( step_01 ) ;
// . . .
cover ( step_23 ) ;
end

This will lead you to the failing clock cycle

320 / 351
 Quiz #23
Welcome Consider the following design:
Motivation
i n p u t w i r e [ 3 1 : 0 ] i_v ;
Basics
output w i r e o_v ;
Clocked and $past

k Induction
assign o_v = ( i_v == 3 2 ’ hdeadbeef ) ;
Bus Properties

Free Variables
always @ ( ∗ )
Abstraction
a s s e r t ( i_v != 3 2 ’ hdeadbeef ) ;
Invariants

Multiple-Clocks always @ ( ∗ )
Cover assume ( ! o_v ) ;
Sequences

Quizzes Given that the solver can pick any value for i_v, will the
assertion ever fail?

321 / 351
 Answer #23
Welcome Consider the following design:
Motivation
a s s i g n o_v = ( i_v == 3 2 ’ hdeadbeef ) ;
Basics
always @ ( ∗ )
Clocked and $past
a s s e r t ( i_v != 3 2 ’ hdeadbeef ) ;
k Induction
always @ ( ∗ )
Bus Properties
assume ( ! o_v ) ;
Free Variables

Abstraction

Invariants ˝ The assumption is forced to be true before evaluating any

Multiple-Clocks assertions
Cover ˝ !o_v will only ever be true if i_v != 32’hdeadbeef
Sequences ˝ Therefore, the solver will never even consider the case where
Quizzes
i_v == 32’hdeadbeef
˝ The assertion can never fail

322 / 351
 Quiz #24
Welcome Consider the following trace from an AXI read interaction:
Motivation

Basics S AXI ACLK

Clocked and $past S AXI ARESETN
k Induction
S AXI ARVALID
Bus Properties

Free Variables S AXI ARID

Abstraction S AXI RVALID
Invariants

Multiple-Clocks
S AXI RID
Cover

Sequences
˝ Assume all of the relevant xREADY lines are high
Quizzes
Can you spot the bug?

323 / 351
 Answer #24
Welcome Can you spot the bug?
Motivation

Basics S AXI ACLK

Clocked and $past S AXI ARESETN
k Induction
S AXI ARVALID
Bus Properties

Free Variables S AXI ARID

Abstraction S AXI RVALID
Invariants

Multiple-Clocks
S AXI RID
Cover

Sequences
The request response has the wrong ID
Quizzes ˝ Request was made for ID=1, response has ID=0
˝ The cause? Xilinx’s example core doesn’t register the ID

The trace above was found by applying the Symbiotic EDA Suite
to Xilinx’s example AXI4 core

324 / 351
 Quiz #25
Welcome Consider the following trace from an AXI write interaction,
Motivation ending in a steady state
Basics

Clocked and $past S AXI ACLK

k Induction
S AXI ARESETN
Bus Properties

Free Variables
S AXI AWVALID
Abstraction S AXI AWREADY
Invariants
S AXI WVALID
Multiple-Clocks

Cover
S AXI WREADY
Sequences S AXI WLAST
Quizzes
S AXI BVALID
S AXI BREADY

What sort of formal property would catch this bug?

325 / 351
 Answer #25
Welcome A transaction timeout can find this bug
Motivation
always @ ( posedge i_clk )
Basics
i f ( ( ! i_axi_reset_n ) | | ( ! i_axi_awvalid )
Clocked and $past
| | ( i_axi_awready )
k Induction
| | ( f_axi_wr_pending > 0 ) )
Bus Properties
f_axi_awstall <= 0 ;
Free Variables
e l s e i f ( ( ! i_axi_bvalid ) | | ( i_axi_bready ) )
Abstraction
f_axi_awstall <= f_axi_awstall + 1 ’ b1 ;
Invariants

Multiple-Clocks always @ ( ∗ )
Cover a s s e r t ( f_axi_awstall < F_AXI_MAXWAIT ) ;
Sequences

Quizzes where f_axi_wr_pending is a reference to the number of

remaining write data transactions in this burst
The bug in this question was found by applying the Symbiotic
EDA Suite to Xilinx’s example AXI4 core

326 / 351
 Answer #25b
Welcome Oops, the last timeout logic captured when the incoming write
Motivation address channel was stalled, not the delay on the write response
Basics channel.
Clocked and $past

k Induction
˝ Here’s the timeout logic that actually found this bug.
Bus Properties
always @ ( posedge i_clk )
Free Variables
i f ( ( ! i_reset_n ) | | ( i_bvalid ) | | ( i_wvalid )
Abstraction
| | ( ( f_awr_nbursts == 1 )
Invariants
&&(f_wr_pending >0))
Multiple-Clocks
| | ( f_awr_nbursts == 0 ) )
Cover
f_awr_ack_delay <= 0 ;
Sequences
else
Quizzes
f_awr_ack_delay <= f_awr_ack_delay + 1 ’ b1 ;

always @ ( posedge i_clk )

a s s e r t ( f_awr_ack_delay < F_AXI_MAXDELAY ) ;

327 / 351
 Quiz #26
Welcome Consider the following trace drawn from an AXI interconnect I
Motivation had the opportunity to verify. It had never seen a formal check
Basics before.
Clocked and $past

k Induction S AXI ACLK

Bus Properties S AXI ARESETN
Free Variables

Abstraction
S AXI AWVALID
3
Invariants S AXI AWLEN
Multiple-Clocks
S AXI WVALID
Cover

Sequences
S AXI WLAST
Quizzes S AXI BVALID

Assume all ∗READY signals are true

Can anyone see the bug? What formal property would catch this
bug?

328 / 351
 Answer #26
Welcome Correctly identifying the bug is important, otherwise you’ll “fix”
Motivation the wrong “bug”
Basics

Clocked and $past S AXI ACLK

k Induction
S AXI ARESETN
Bus Properties

Free Variables
S AXI AWVALID
3
Abstraction S AXI AWLEN
Invariants
S AXI WVALID
Multiple-Clocks

Cover
S AXI WLAST
Sequences S AXI BVALID
Quizzes

In this case, there is no missing S_AXI_WLAST signal. According

to spec, the burst is S_AXI_AWLEN+1 beats long, so there’s still a
missing write beat. The bus master just hasn’t sent the final
beat yet.

329 / 351
 Answer #26b
Welcome The bug? You can’t return a BVALID response until the first
Motivation write burst has completed.
Basics To verify this, you need to count items remaining in the burst, I
Clocked and $past use f_wr_pending, as well as the number of bursts outstanding,
k Induction
something I call f_awr_nbursts. You can then check,
Bus Properties

Free Variables always @ ( ∗ )

Abstraction i f ( f_awr_nbursts == 0 )
Invariants // I f t h e r e a r e no b u r s t s o u t s t a n d i n g
Multiple-Clocks // t h e n no BVALID can be r e t u r n e d
Cover
a s s e r t ( ! S_AXI_BVALID ) ;
Sequences
e l s e i f ( f_awr_nbursts == 1 )
Quizzes
// I f t h e w r i t e c h a n n e l i s s t i l l s e n d i n g
// data , t h e n t h e BVALID c a n n o t ( y e t ) be
// r e t u r n e d .
a s s e r t ( ( f_wr_pending == 0 )
| | ! S_AXI_BVALID ) ;

330 / 351
 Quiz #27
Welcome Can you explain why the following cover statement fails?
Motivation
reg read_counter ;
Basics
i n i t i a l read_counter = 0 ;
Clocked and $past
always @ ( posedge i_clk )
k Induction
i f ( i_reset )
Bus Properties
read_counter <= 0 ;
Free Variables
e l s e i f ( some_event )
Abstraction
read_counter <= read_counter + 1 ;
Invariants

Multiple-Clocks always @ ( ∗ )
Cover cover ( read_counter > 4 ) ;
Sequences

Quizzes

331 / 351
 Answer #27
Welcome Can you explain why the following cover statement fails?
Motivation
reg read_counter ;
Basics
i n i t i a l read_counter = 0 ;
Clocked and $past
always @ ( posedge i_clk )
k Induction
i f ( i_reset )
Bus Properties
read_counter <= 0 ;
Free Variables
e l s e i f ( some_event )
Abstraction
read_counter <= read_counter + 1 ;
Invariants

Multiple-Clocks always @ ( ∗ )
Cover cover ( read_counter > 4 ) ;
Sequences

Quizzes Did you notice the number of bits in the read_counter? At only
one bit, read_counter can never be more than one.

332 / 351
 Quiz #28
Welcome Let NM be the number of masters, and NS the number of slaves.
Motivation You want to cover a full set of write grants.
Basics
reg cvr_property ;
Clocked and $past
always @ ( ∗ )
k Induction
begin
Bus Properties
cvr_property = 1 ;
Free Variables
f o r ( iN =0; iN < ( NM > NS ) ? NS : NM ; iN=iN+1)
Abstraction
i f ( ! write_grant [ iN ] )
Invariants
cvr_property = 0 ;
Multiple-Clocks
end
Cover

Sequences
always @ ( ∗ )
Quizzes
cover ( cvr_property ) ;

Much to my surprise, yosys ran out of memory while elaborating

this code.
Can anyone see why?

333 / 351
 Answer #28
Welcome This is an order of operations issue. The example design is
Motivation equivalent to
Basics
always @ ( ∗ )
Clocked and $past
begin
k Induction
cvr_property = 1 ;
Bus Properties
f o r ( iN =0; ( iN < ( NM > NS ) ) ? NS : NM ;
Free Variables
iN=iN+1)
Abstraction
i f ( ! write_grant [ iN ] )
Invariants
cvr_property = 0 ;
Multiple-Clocks
end
Cover

Sequences The end condition will therefore elaborate to either NM or NS,

Quizzes
both of which are non-zero and therefore “true”.
As for the out-of-memory error, remember this is hardware.
Yosys is elaborating new hardware circuits every time through
the loop, and the loop doesn’t have an end.

334 / 351
 Quiz #29
Welcome There are three steps required to verify an AXI-lite interface:
Motivation
1. First, attach the formal interface property file
Basics

Clocked and $past ‘ i f d e f FORMAL

k Induction faxil_slave #(
Bus Properties . C_AXI_ADDR_WIDTH ( C_S_AXI_ADDR_WIDTH ) )
Free Variables properties (
Abstraction . i_clk ( S_AXI_ACLK ) ,
Invariants . i_axi_reset_n ( S_AXI_ARESETN ) ,
Multiple-Clocks // . . .
Cover

Sequences
2. If using SymbiYosys, you’ll also need to create an SBY file
Quizzes What’s the missing step that’s required to formally verify an
AXI-lite slave interface matches bus requirements for all time?

335 / 351
 Answer #29
Welcome 3. Reference the state information from the property file,
Motivation
‘ i f d e f FORMAL
Basics
faxil_slave #(/∗ . . . ∗/ )
Clocked and $past
properties ( // . . .
k Induction
. f_axi_rd_outstanding ( rd_inproc ) ,
Bus Properties
// . . .
Free Variables

Abstraction and use it to assert() that the state maches your logic
Invariants

Multiple-Clocks
always @ ( ∗ )
Cover
a s s e r t ( rd_inproc == ( axi_rvalid ? 1 : 0 )
Sequences
+(axi_arready ? 0 : 1 ) ) ;
Quizzes
// . . .

The example above is from one of my own designs, as this step

can be very design dependent.

336 / 351
 Quiz #30
Welcome The following illustrates a common FIFO mistake
Motivation
always @ ( posedge i_clk )
Basics
i f ( i_reset )
Clocked and $past
{ rd_addr , wr_addr } <= 0 ;
k Induction
e l s e i f ( i_rd )
Bus Properties
rd_addr <= rd_addr + 1 ;
Free Variables
e l s e i f ( i_wr )
Abstraction
wr_addr <= wr_addr + 1 ;
Invariants

Multiple-Clocks Can you identify the bug, and suggest a way of fixing it?
Cover

Sequences

Quizzes

337 / 351
 Answer #30
Welcome The first bug is not setting the pointers initially
Motivation
i n i t i a l { rd_addr , wr_addr } = 0 ;
Basics

Clocked and $past

The next bug is not checking for underflow or overflow
k Induction

Bus Properties always @ ( posedge i_clk )

Free Variables i f ( i_reset )
Abstraction { rd_addr , wr_addr } <= 0 ;
Invariants e l s e i f ( i_rd && ! o_empty )
Multiple-Clocks
rd_addr <= rd_addr + 1 ;
Cover
e l s e i f ( i_wr && ! o_full )
Sequences
wr_addr <= wr_addr + 1 ;
Quizzes
That leaves at least one more bug

338 / 351
 Answer #30b
Welcome The real problem is that the whole structure is wrong.
Motivation
˝ This really needs ot be handled in either two logic blocks, or
Basics
˝ Using a case statement, as shown below
Clocked and $past

k Induction
i n i t i a l { rd_addr , wr_addr } = 0 ;
Bus Properties
always @ ( posedge i_clk )
Free Variables
i f ( i_reset )
Abstraction
{ rd_addr , wr_addr } <= 0 ;
Invariants
e l s e case ( { i_rd & ! o_empty , i_wr && ! o_full } )
Multiple-Clocks
2 ’ b10 : rd_addr <= rd_addr + 1 ;
Cover
2 ’ b01 : wr_addr <= wr_addr + 1 ;
Sequences
2 ’ b11 : begin
Quizzes
rd_addr <= rd_addr + 1 ;
wr_addr <= wr_addr + 1 ;
end
endcase

339 / 351
 Quiz #31
Welcome The following proof passes.
Motivation
reg f_past_valid = 0 ;
Basics
always @ ( posedge i_clk )
Clocked and $past
f_past_valid <= 1 ;
k Induction

Bus Properties
always @ ( ∗ )
Free Variables
i f ( f_past_valid )
Abstraction
assume ( i_reset ) ;
Invariants

Multiple-Clocks always @ ( posedge i_clk )

Cover counter <= really_complex_logic ;
Sequences

Quizzes always @ ( ∗ )
i f ( f_past_valid && ! i_reset )
a s s e r t ( counter == counter + 1 ) ;

Can you spot the bug?

340 / 351
 Answer #31
Welcome Did you notice the assumption that i_reset is held high?
Motivation
always @ ( ∗ )
Basics
i f ( f_past_valid )
Clocked and $past
assume ( i_reset ) ;
k Induction

Bus Properties
The assertion never got checked!
Free Variables

Abstraction always @ ( ∗ )
Invariants i f ( f_past_valid && ! i_reset )
Multiple-Clocks
a s s e r t ( counter == counter + 1 ) ;
Cover

Sequences
A basic cover test would find this problem
Quizzes always @ ( ∗ )
cover ( f_past_valid && ! i_reset ) ;
// o r e v e n
always @ ( ∗ )
cover ( counter == counter + 1 ) ;

341 / 351
 Quiz #32
Welcome How would you verify the o_empty and o_full properties of a
Motivation FIFO, given the read and write addresses?
Basics
˝ The o_empty flag
Clocked and $past

k Induction a s s i g n fill = wr_addr ´ rd_addr ;

Bus Properties always @ ( ∗ )
Free Variables begin
Abstraction a s s e r t ( o_empty == ( fill == 0 ) ) ;
Invariants

Multiple-Clocks ˝ The o_full flag, given a FIFO with FIFO_SIZE elements

Cover
a s s e r t ( o_full == ( fill >= FIFO_SIZE ) ) ;
Sequences
// . . .
Quizzes
end

What property is missing?

342 / 351
 Answer #32
Welcome The missing property?
Motivation
˝ We checked the o_empty flag
Basics
˝ We checked the o_full flag
Clocked and $past
˝ Don’t forget to check that the fill never exceeds the capacity
k Induction

Bus Properties
of the FIFO
Free Variables
a s s e r t ( fill <= FIFO_SIZE ) ;
Abstraction

Invariants
Checking the data content of the FIFO still requires the twin
Multiple-Clocks

Cover
write followed by twin read test. You can read more about that
Sequences
in my on-line tutorial.
Quizzes

343 / 351
 Quiz #33
Welcome Formally verifying a cache requires three properties
Motivation
First, let the solver to pick an arbitrary address and value
Basics

Clocked and $past ( ∗ anyconst ∗ ) reg [ AW ´ 1 : 0 ] f_const_addr ;

k Induction ( ∗ anyconst ∗ ) reg [ DW ´ 1 : 0 ] f_const_data ;
Bus Properties

Free Variables 1. Then when the bus returns a value for the given address,
Abstraction assume the known value.
Invariants
i f ( i_wb_ack && ackd_address == f_const_addr )
Multiple-Clocks
assume ( i_wb_data == f_const_data ) ;
Cover

Sequences
2. Whenever the cache returns the value for the special
Quizzes
address, assert that the known value is returned
i f ( o_valid && o_address == f_const_addr )
a s s e r t ( o_value == f_const_data ) ;

3. What’s missing?
344 / 351
 Answer #33
Welcome Formally verifying a cache requires three properties
Motivation
First, allow the solver to pick an arbitrary address, and an
Basics
arbitrary data word at that address.
Clocked and $past

k Induction
1. assume a known bus response from the given address
Bus Properties
2. assert that same response from the cache when that same
Free Variables address is requested
Abstraction
The missing property?
Invariants

Multiple-Clocks 3. Assert that, if the known address is validly within the cache,
Cover that the value associated with that address matches the
Sequences solver chosen value
Quizzes
always @ ( ∗ )
i f ( cache_valid [ f_const_addr ] )
a s s e r t ( cache [ f_const_addr [ CW ´ 1 : 0 ] ]
== f_const_data ) ;

345 / 351
 Quiz #34
Welcome The following code illustrates a common AXI coding mistake:
Motivation
always @ ( posedge S_AXI_ACLK )
Basics
i f ( ! S_AXI_ARESETN )
Clocked and $past
// Do s o m e t h i n g
k Induction
e l s e i f ( S_AXI_AWVALID && S_AXI_AWREADY
Bus Properties
&& something_else )
Free Variables
// W r i t e l o g i c
Abstraction
e l s e i f ( S_AXI_BREADY )
Invariants
// L a s t c o n d i t i o n
Multiple-Clocks // . . . .
Cover

Sequences Can you identify the bug, and suggest one or two fixes?
Quizzes

346 / 351
 Answer #34
Welcome The following code illustrates a common AXI coding mistake:
Motivation
always @ ( posedge S_AXI_ACLK )
Basics
// . . .
Clocked and $past
i f ( S_AXI_AWVALID && S_AXI_AWREADY
k Induction
&& something_else )
Bus Properties
// . . .
Free Variables

Abstraction The mistake? Checking for something_else when processing

Invariants
information from the bus. To fix it,
Multiple-Clocks

Cover 1. Adjust the logic for S_AXI_AWREADY

Sequences 2. Prove that every time something_else is false, then
Quizzes S_AXI_AWREADY is will also be false
a s s e r t p r o p e r t y ( @ ( posedge S_AXI_ACLK )
! something_else |´> ! S_AXI_AWREADY ) ;

347 / 351
 Quiz #35
Welcome Will the following logic pass formal verification?
Motivation
reg [15:0] counter , last ;
Basics

Clocked and $past

i n i t i a l counter = 1 ;
k Induction
i n i t i a l last = 0;
Bus Properties

Free Variables
always @ ( posedge i_clk )
Abstraction
begin
Invariants
counter <= counter + 1 ;
Multiple-Clocks last <= counter ;
Cover end
Sequences

Quizzes always @ ( ∗ )
a s s e r t ( last + 1 == counter ) ;

348 / 351
 Answer #35
Welcome The problem is that last+1 is a 32-bit value, whereas counter is
Motivation a 16-bit unsigned value. This assertion will always fail when
Basics counter rolls over.
Clocked and $past

k Induction i clk
Bus Properties 16’hfffd 16’hfffe 16’hffff 16’h0000
counter
Free Variables
16’hfffc 16’hfffd 16’hfffe 16’hffff
Abstraction last
32’h0fffd 32’hfffe 32’h0ffff 32’h10000
Invariants last`1
Multiple-Clocks
failing timestep
Cover

Sequences

Quizzes If you map last+1 to a 16-bit value, the assetion will pass
wire [ 1 5 : 0 ] last_plus_one = last + 1 ;
always @ ( ∗ )
a s s e r t ( last_plus_one == counter ) ;

349 / 351
 Quiz #36
Welcome The following code generates a warmup failure.
Motivation
input wire [31:0] i_a , i_b , i_c ;
Basics

Clocked and $past

always @ ( ∗ )
k Induction
begin
Bus Properties
assume ( i_a+ i_b == 3 2 ’ h4 ) ;
Free Variables
assume ( i_b +i_c == 3 2 ’ h8 ) ;
Abstraction
assume ( i_a+{ i_b , 1 ’ b0}+i_c == 3 2 ’ h7 ) ;
Invariants
end
Multiple-Clocks

Cover Which assumption is at fault?

Sequences

Quizzes

350 / 351
 Answer #36
Welcome Which assumption is at fault?
Motivation
input wire [31:0] i_a , i_b , i_c ;
Basics

Clocked and $past

always @ ( ∗ )
k Induction
begin
Bus Properties
assume ( i_a+ i_b == 3 2 ’ h4 ) ;
Free Variables
assume ( i_b +i_c == 3 2 ’ h8 ) ;
Abstraction
assume ( i_a+{ i_b , 1 ’ b0}+i_c == 3 2 ’ h7 ) ;
Invariants
end
Multiple-Clocks

Cover Removing any one of these assumptions will resolve the warmup
Sequences failure.
Quizzes
˝ This illustrates one of the fundamental problems of warmup
failures: Since any one of several assumptions might cause
the design to fail, there’s no way for the solver to tell which
assumption was truly at fault.

351 / 351