apb_assertions.v

systemverilog是新出现的一种高级硬件描述和验证语言

// ________________________________________________________________ apb.v ___
//
// Interface model for ARM APB (AMBA Peripheral Bus),
// used as an example of inter-module communication
// with interfaces.
//
// The bus is quite simple and can have only one master.
// The master can perform read and write cycles to one location
// at a time (no burst transfers).  The bus is fully synchronous
// to the rising edges of an externally supplied clock.
//
// Note that APB doesn't specify a global reset signal, so any reset
// required by devices on the bus must be supplied separately and
// doesn't form part of this interface.
//
// The interface also offers procedural entry points so that
// a test fixture can perform read and write cycles without
// needing to create a bus functional model of the bus master.
// Unfortunately, VCS 7.1 doesn't yet allow us to pass these
// procedural entry points through a modport; we have to
// invoke them using hierarchical names, just as with a
// typical Verilog bus functional model (BFM).
//
//
// Revision information:
// =====================
//
// v0.0  19-Jan-2004  Jonathan Bromley
//    Modified from tci_bus.v
//
// v0.1  25-Jan-2004  Jonathan Bromley
//    Improved internal documentation
//
// v1.0  02-Feb-2004  Jonathan Bromley
//    Adding some SystemVerilog assertions.  This is now
//    the lead revision.
//
// v1.1  05-Feb-2004  Jonathan Bromley
//    * tidied-up the assertions;
//    * put back the TF_ modport's import task definitions
//    * got rid of task CheckLastClock and repackaged it as
//      ClockTcoSync with no arguments
//
// v1.2  17-Feb-2004  Jonathan Bromley
//    * more improvements to cosmetics of assertions
// __________________________________________________________________________



`timescale 1ns/100ps


// _________________________________________________________ GLOBAL STUFF ___

// Publicly visible typedefs for APB data and address types:
//
typedef logic [15:0] T_APB_d;
typedef logic [15:0] T_APB_a;

// __________________________________________________________________________



// _________________________________________________ INTERFACE DEFINITION ___

interface APB #(parameter master_Tco = 1);

  // See also modports and tasks:
  //
  // modport RTL_slave   -- connect any RTL slave model to one of these
  // modport RTL_master  -- connect an RTL master model to this (one only)
  // modport TF_master   -- Connect a behavioural master to this (one only)
  //   task read;          -- BFM entry point for behavioural tests
  //   task write;         -- BFM entry point for behavioural tests

// __________________________________________________________________________



// _________________________________________________ PHYSICAL BUS SIGNALS ___

  // Bus clock, generated by external master (typically AHB-APB bridge).
  //
  // NOTE: Even if there is no external master, but only a testbench using
  // the BFM read and write entry points, it is ESSENTIAL for the
  // environment to provide a suitable clock on this signal.
  // This can be done either directly or through the RTL_master modport.
  //
  logic  PCLK;

  // Select signal.  Each slave must qualify this signal
  // with the appropriate address, since we can't
  // parameterise the slave's modport.
  //
  logic    psel = 0;

  // Address signal from master
  //
  T_APB_a  PADDR;

  // Write data, from master
  //
  T_APB_d  PWDATA;

  // Write and enable signals from master
  //
  logic    PWRITE = 0;
  logic    PENABLE = 0;

  // Readback data signal, written by selected slave.  Non-selected
  // slaves must refrain from updating PRDATA on read cycles.
  //
  T_APB_d  PRDATA;

// __________________________________________________________________________



// _____________________________________________________________ MODPORTS ___

  // Any slave connects like this...
  //
  modport RTL_slave (
    input  PCLK,    // Slaves get their clock from the bus
    input  psel,    // Select signal - global for all slaves
    input  PWRITE,  // Active in the clock when address is sent
    input  PENABLE, // Direction control, sent with the address
    input  PADDR,
    input  PWDATA,
    output PRDATA
  ); // modport RTL_slave

  // The one and only master connects like this:
  //
  modport RTL_master (
    output PCLK,    // Master supplies clock to the bus
    output psel,    // Master asserts psel during active cycle
    output PWRITE,  // Active in the clock when address is sent
    output PENABLE, // Direction control, sent with the address
    output PADDR,
    output PWDATA,
    input  PRDATA
  );  // modport RTL_master

  // Alternatively you can connect a behavioural master
  // to this BFM-like modport:
  //
  modport TF_master (
    output PCLK,                 // Master supplies clock to the bus
    import task write(), read()  // Master calls these tasks to do cycles
  ); // modport TF_master

// __________________________________________________________________________



// _____________________________________________________ BFM ENTRY POINTS ___

  // Non-synthesisable task-call interface for a testbench master
  // so that it can exercise slaves on the bus without the need for
  // a fully-functional model of a master device.

  // Call these BFM tasks at the posedge of the clock right
  // at the beginning of the cycle. They return just after
  // the final posedge of the cycle.

  // _______________________________________________________ read() ___
  //
  task read (
    input  T_APB_a adrs,
    output T_APB_d data
  );

    // Get to Tco after the most recent possible clock
    ClockTcoSync;
      PADDR    = adrs;
      PWRITE   = 1'b0;
      psel     = 1'b1;

    @(posedge PCLK)
      PENABLE <= #master_Tco 1'b1;

    @(posedge PCLK)
      data     = PRDATA;
      PADDR   <= {$bits(PADDR){1'bx}};
      psel    <= 1'b0;
      PENABLE <= 1'b0;

  endtask // read

  // ______________________________________________________ write() ___
  //
  task write (
    input T_APB_a adrs,
    input T_APB_d data
  );

    // Get to Tco after the most recent possible clock
    ClockTcoSync;
      PADDR    = adrs;
      PWDATA   = data;
      PWRITE   = 1'b1;
      psel     = 1'b1;

    @(posedge PCLK)
      PENABLE <= #master_Tco 1'b1;

    @(posedge PCLK)
      PWDATA  <= {$bits(PADDR){1'bx}};
      PADDR   <= {$bits(PADDR){1'bx}};
      psel    <= 1'b0;
      PENABLE <= 1'b0;

  endtask // write

  // _______________________________________________________ idle() ___
  //
  task idle ( int n );

    if (n > 0 ) begin
      ClockTcoSync;
      repeat (n) @(posedge PCLK);
    end

  endtask


// __________________________________________________________________________



// ____________________________________________ HELPER CODE FOR BFM TASKS ___

  // As always with procedural entry points into a BFM, there is
  // an issue about synchronisation between the moment of task call
  // and the bus's clock.  If the task is called at some random time,
  // its activity must be resynchronised to the bus clock.  However,
  // if it's already synchronised, then we don't want a spurious
  // additional clock wait.  One possible solution to this problem is
  // offered here: the BFM read and write tasks can be called at any
  // time.  If called at or just after a clock edge, BFM activity can
  // proceed as from that clock edge (signals don't need to be set up
  // until one clock-to-valid delay after the clock edge).  If called
  // at any other time, the task is stalled until just after the next
  // clock edge.

  // In order to make this approach work, we need to keep track of
  // the time of the most recent active clock edge.
  //
  always @(posedge PCLK) begin : ClockEdgeLogger

    time LastClock;
    LastClock = $time;

  end // ClockEdgeLogger


  // Now, when a BFM task is called, it uses the time-of-last-clock
  // information to determine whether it can proceed immediately, or
  // must wait until the next clock.  Task checkLastClock() encapsulates
  // this behaviour;  it not only enforces the clock wait if necessary,
  // but also waits until the future time at which the BFM task must
  // apply its valid bus signals.
  //
  // Note that this task will still work correctly even if
  // parameter master_Tco is set to zero.
  //
  task ClockTcoSync;

    time t;

    // If this task was called as the result of a clock edge, we must
    // be sure that the LastClock value has already been updated.
    // That's why we need a #0 delay prefix here.
    //
    #0 t = $time - ClockEdgeLogger.LastClock;

    // Are we too late to start the bus cycle on the current clock?
    //
    if (t > master_Tco) begin

      // Yes, we're too late.  Wait for the next clock.
      @(posedge PCLK) t = master_Tco;

    end else begin

      // No, we're in time.  Calculate how long we need to wait
      // before applying the right signals.
      t = master_Tco - t;

    end

    // Finally, align to Tco after the chosen clock
    #(t);

  endtask

// _______________________________________________________ APB ASSERTIONS ___

  // Define the basics of a cycle
  //
  // A clock cycle in which nothing is happening...
  sequence APB_IDLE;
    !psel;
  endsequence

  // psel without PENABLE (first clock of cycle)
  sequence APB_PHASE_1;
    psel && !PENABLE;
  endsequence

  // psel with PENABLE (second clock of cycle)
  sequence APB_PHASE_2;
   psel && PENABLE;
  endsequence

  // A complete bus cycle
  sequence APB_CYCLE;
    APB_PHASE_1 ##1 APB_PHASE_2;
  endsequence

  // A read cycle
  sequence APB_READ_CYCLE;
    (!PWRITE) throughout APB_CYCLE;
  endsequence

  // A write cycle
  sequence APB_WRITE_CYCLE;
    PWRITE throughout APB_CYCLE;
  endsequence


  // Safety properties.  Note that some of these would be nicer
  // if we could write implications with a sequence as the antecedent.
  // Sadly VCS doesn't yet allow this.  See commented-out code.

  property APB_CYCLES_ARE_COMPLETE;
    // Once a cycle has started, it must complete
    //@(posedge PCLK) (APB_PHASE_1 |-> APB_CYCLE);
    @(posedge PCLK) ((psel && !PENABLE) |-> APB_CYCLE);
  endproperty

  property APB_NO_PENABLE_OUTSIDE_CYCLE2;
    // If we see PENABLE, it must be in the second clock of a cycle,
    // and it must then go away
    // ******* NB ********* Prefer to use APB_CYCLE.ended() instead of
    //                      $stable(psel), but it's not yet implemented
    @(posedge PCLK) (PENABLE |-> $stable(psel) ##1 (!PENABLE));
  endproperty

  property APB_WRITE_AND_ADDR_STABLE;
    // PWRITE and PADDR must be stable throughout the cycle
    //@(posedge PCLK) (APB_PHASE_2 |-> $stable({PWRITE, PADDR}));
    @(posedge PCLK) ((psel && PENABLE) |-> $stable({PWRITE, PADDR}));
  endproperty

  property APB_WRITE_AND_ADDR_VALID;
    // PWRITE and PADDR must be valid throughout the cycle (no X, Z)
    //@(posedge PCLK) (APB_PHASE_2 |-> ((!{PWRITE, PADDR}) !== 1'bx));
    @(posedge PCLK) ((psel && PENABLE) |-> ((!{PWRITE, PADDR}) !== 1'bx));
  endproperty

  property APB_WRITE_DATA_STABLE;
    // PWDATA must be stable throughout a write cycle
    @(posedge PCLK) ((PENABLE && PWRITE) |-> $stable(PWDATA));
  endproperty

  property APB_COMPLETE_CYCLES_WITH_VALID_ADDRESS;
    // PWRITE and PADDR must be valid throughout the cycle (no X, Z)
    // $isunknown isn't yet implemented, so use ((^A)===1'bx) instead
    @(posedge PCLK) ( (psel && !PENABLE) |->
                      ( ((^{PWRITE, PADDR}) !== 1'bx) throughout APB_CYCLE)
                    );
  endproperty


  // Assertions to check the safety properties

  cycles_complete   : assert property (APB_CYCLES_ARE_COMPLETE);
  PENABLE_valid     : assert property (APB_NO_PENABLE_OUTSIDE_CYCLE2);
  controls_stable   : assert property (APB_WRITE_AND_ADDR_STABLE);
  write_data_stable : assert property (APB_WRITE_DATA_STABLE);


  // Finally a few sequences to provide coverage points...

  // Two (or more) cycles back-to-back...
  sequence APB_BACK_TO_BACK;
    @(posedge PCLK) APB_CYCLE ##1 APB_CYCLE;
  endsequence

  // A bus cycle, preceded by an idle cycle...
  sequence APB_IDLE_THEN_CYCLE;
    @(posedge PCLK) APB_IDLE ##1 APB_CYCLE;
  endsequence


// __________________________________________________________________________


endinterface // APB