SVA Generator

Overview

• Uses Chisel/Scala to generate RTL to describe the behavior of a finite state machine to setup and index an SDRAM memory module
• JSON files are inputted, representing SDRAM memory datasheets to include various timing parameters , into the Scala program

DRAM Indexing

Finite State Machine Diagram

Finite State Machine Specification

• Init State - Must stay here for 100 microseconds, can never return here unless reset is asserted, must transition to idle state after 100 microseconds and 3 cycles
• Idle State - Must transition to Active state if a read or write request is asserted on the next cycle
• Active State - Must transition to read or write state after the appropriate amount of cycles have passed
• Read State - Must assert read data valid after the appropriate amount of cas latency cycles have passed, must transition back to idle state after the appropriate amount of cas latency plus burst length cycles have passed
• Write State - Must transition to idle state after the appropriate amount of burst length cycles have passed

What is SVA

• An assertion is a statement about your design that you expect to be true always. - Formal Verification, Erik Seligman et al.
• Require formal verification tools to read - Yosys - SymbiYosys
• Used as targets for proofs rather than basic checks
• Two types: immediate and concurrent
  • Immediate - purely combinational logic, evaluated at any time step
  • Concurrent - evaluated at specific points in time, allow for strings of events across time

SymbiYosys

• Front-end for formal verification based off Yosys
• Interface with different SMT solvers - picked yices2
• Displays counterexamples on a .vcd file to be opened with GTKWave
• .sby scripts can be used for automation

.sby script example

[options]
mode bmc
depth 20

[engines]
smtbmc yices

[script]
read -formal SDRAMController.sv
prep -top SDRAMController

[files]
SDRAMController.sv

Active to Read or Write Example

• Take one of the provided specifications for the active state: Must transition to read or write state after the appropriate amount of cycles have passed
• Below is how one would compose that into SVA

assert property (@(posedge clock) disable iff (reset) io_state_out == 3 |=> ##5 (io_state_out == 6 | io_state_out== 7) )

Running the first assert

Why the first assert failed

Is my code wrong?

is(ControllerState.idle) {
  state := ControllerState.idle
  read_state_counter.reset()
  write_state_counter.reset()
  val go_to_active =
  io.read_start | io.write_start
  sdram_commands.NOP()
  io.read_data_valid := false.B
  io.write_data_valid := false.B
  when(refresh_outstanding) {
    sdram_commands.Refresh()
    refresh_outstanding := false.B
  }.elsewhen(go_to_active) {
    state := ControllerState.active
    val row_and_bank = io.read_row_address
    sdram_commands.Active(row_and_bank)
    cas_counter.reset()
    when(io.read_start) {
        started_read := true.B
    }.elsewhen(io.write_start) {
        started_write := true.B
    }
  }
}

SystemVerilog assume keyword

• Used to reduce cone of influence of the design
• Below is an example of an assume statement

assume property (@(posedge clock) disable iff (reset) (started_read | started_write))

Including Assumptions

Assumption created new counter-example: active to rw counter can be in the middle of counting

Another Assumption

assume property (@(posedge clock) disable iff (reset) (active_to_rw_counter_value == 0))

SystemVerilog Assertion Modifier Class

• Given this program is a hardware generator, assertions must be generated according to the provided parameters
• Created “SVA_Modifier” Scala package and class
• Takes in the same SDRAM Parameter case class used to define all parameters for state machine generation
• Writes in SV assertions and assumptions with basic file IO

Design Space Exploration

• Tested 8 different designs for ISSI IS42S81600 and Winbond W9825G6KH SDRAM memories
• Changed clock frequency, CAS latency (2 and 3), and burst lengths (1 to 8)
  • ISSI clocked at 100MHz for CAS2 and 166MHz for CAS3
  • Winbond clocked at 133MHz for CAS2 and 200Mhz for CAS3
• All assertions passed after cone of influence was correctly refined by assume statements
• Fixed bugs with read and write states not behaving according to spec
  • Read exited at cas latency being reached, write would only write one item regardless of burst length

Challenges

• Lack of good documentation of the open source tools
• Open Source Tools - they’re awful, but they are free :D
  • Don’t support esoteric SystemVerilog features - mainly bi-directional ports
• Licensing
• Learning to read counter-examples
• Failing assertions doesn’t necessarily mean your specification is wrong

Future Work

• Support Data Flow
  • Bidirectional ports are a Chisel experimental library feature
  • Bidirectional ports are also an experimental feature of most Yosys tools, outside of synthesis
• Different interface support
  • AXI is popular with Xilinx IPs