In reply to ben@SystemVerilog.us:
//`include "i2c_config.sv"
import CONFIG::*;
module i2c_assertions();
time Tsda_rise,Tscl_rise;
time Tscl_fall,Tsda_fall;
logic scl;
bit slave_addr_tran;
bit mem_addr_tran;
bit data_tran_WR;
bit data_tran_RD;
i2c_if I2C_INTERFACE(.scl(scl));
initial
begin
i2c_config cfg;
//cfg = new();
end
/*
always @(posedge I2C_INTERFACE.scl)
begin
slave_addr_tran = cfg.slave_addr_tran;
mem_addr_tran = cfg.mem_addr_tran;
data_tran_WR = cfg.data_tran_WR;
data_tran_RD = cfg.data_tran_RD;
end
*/
//Config class
//*******************************************************PROPERTIES and SEQUENCES*****************************************************//
//typedef class i2c_config;// cfg;
//cfg = new();
/*
initial
begin
cfg = new();
end
*/
//START condition
//Detects START condition
sequence s1;
@(negedge I2C_INTERFACE.sda) (I2C_INTERFACE.scl==1);
endsequence
task posedge_delay();
@(posedge I2C_INTERFACE.scl);
endtask
property p1;
@(negedge I2C_INTERFACE.sda) s1;
endproperty
//Detects STOP condition
sequence s2;
@(posedge I2C_INTERFACE.sda) (I2C_INTERFACE.scl==1);
endsequence
property p2;
@(negedge I2C_INTERFACE.sda) s2;
endproperty
//BUS IDLE
/*
property p4;
@(I2C_INTERFACE.scl) s2|=>(I2C_INTERFACE.sda && I2C_INTERFACE.scl)|=>s1;
endproperty
*/
//SLAVE ADDRESS TRANSFER & ACK
//SLAVE ADDRESS trasnfer starts
property p5;
@ (posedge I2C_INTERFACE.scl) s1|->(1'b1,posedge_delay)|->(slave_addr_tran==1'b1);
endproperty
//SLAVE ADDRESS transfer ends
property p6;
@(posedge I2C_INTERFACE.scl) s1|=> ##8 (slave_addr_tran==1'b0);
endproperty
//SLAVE ADDRESS ACK
property p7;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe));
endproperty
//MEMORY ADDRESS TRANSFER & ACK
//MEMORY ADDRESS transfer starts
property p8;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9 !(I2C_INTERFACE.sda_oe)|=>(mem_addr_tran==1'b1);
endproperty
//MEMORY ADDRESS transfer ends
property p9;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=> ##8 (mem_addr_tran==1'b0);
endproperty
//MEMORY ADDRESS ACK
property p10;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe));
endproperty
//DATA TRANSFER & ACK (WRITE operation)
//DATA TRANSFER starts
property p11;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|=>(data_tran_WR==1'b1);
endproperty
//DATA TRANSFER ends
/*
property p12;
@(posedge I2C_INTERFACE.scl) s1|=> (cfg.slave_addr_tran_WR==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|=>##8 (cfg.data_tran_WR==1'b0);
endproperty
*/
//DATA TRANSFER ACK (by Slave)
property p13;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|->##9 (!(I2C_INTERFACE.sda_oe));
endproperty
//DATA TRANSFER & ACK (READ operation)
//DATA TRANSFER starts
property p14;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|=>(data_tran_RD==1'b1);
endproperty
//DATA TRANSFER ends
/*
property p15;
@(posedge I2C_INTERFACE.scl) s1|=> (cfg.slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|=>##8 (cfg.data_tran_RD==1'b0);
endproperty
*/
//DATA TRANSFER ACK (by Master)
property p16;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|->##9(!(I2C_INTERFACE.sda_oe))|=>##9 (!(I2C_INTERFACE.sda_oe))|->##9 !(I2C_INTERFACE.sda);
endproperty
//RepStart condition
//When slave didn't respond during slave address transfer
property p17;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//When NACK sent during memory address transfer
property p18;
@(posedge I2C_INTERFACE.scl) s1|=> (mem_addr_tran==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//When NACK sent during data transfer
//WRITE to slave
property p19;
@(posedge I2C_INTERFACE.scl) s1|=> (data_tran_WR==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//READ from slave
property p20;
@(posedge I2C_INTERFACE.scl) s1|=> (data_tran_RD==1'b1)|=>##9 (I2C_INTERFACE.sda);
endproperty
//WRITE operation DETECT
property p21;
@(posedge I2C_INTERFACE.scl) s1|=> ##8(!(I2C_INTERFACE.sda));
endproperty
//READ operation detect
property p22;
@(posedge I2C_INTERFACE.scl) s1|=> ##8 I2C_INTERFACE.sda;
endproperty
//When slave didn't respond during slave address transfer
property p23;
@(posedge I2C_INTERFACE.scl) s1|=> (slave_addr_tran==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//NACK sent by slave when master sends memory address
property p24;
@(posedge I2C_INTERFACE.scl) s1|=> (mem_addr_tran==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//NACK sent by slave after sending data to slave
property p25;
@(posedge I2C_INTERFACE.scl) s1|=> (data_tran_WR==1'b1)|=>##9 (I2C_INTERFACE.sda_oe);
endproperty
//NACK sent by master after recieving data from slave
property p26;
@(posedge I2C_INTERFACE.scl) s1|=> (data_tran_RD==1'b1)|=>##9 (I2C_INTERFACE.sda);
endproperty
//Illegal Format (START followed by STOP in the next cycle)
property p27;
@(posedge I2C_INTERFACE.scl) s1 |=> s2;
endproperty
/////////////*****************************************************************ASSERTIONS*******************************************************************/////////////
START : assert property (p1) $display (" START condition detected at %0t ",$time); else $display("START NOT DETECTED") ;
STOP : assert property (p2) $display (" STOP condition detected at %0t ",$time);
//VALID_DATA : assert property (p3) $display (" INVALID SDA TRANSITION "); else $display("Assertion Failed : INVALID DATA");
//BUS_IDLE : assert property (p4) $display (" I2C bus went to IDLE state ");
SLAVE_ADDR_TRANSFER_START : assert property (p5) $display (" SLAVE ADDRESS transfer started ");
SLAVE_ADDR_TRANSFER_END : assert property (p6) $display (" SLAVE ADDRESS transfer ended ");
SLAVE_ADDR_ACK : assert property (p7) $display (" SLAVE generated ACK ");
NO_RESPONSE_FROM_SLAVE : assert property (p23) $display (" SLAVE not responded for the slave address sent");
MEM_ADDR_TRANSFER_START : assert property (p8) $display (" MEMORY ADDRESS transfer started ");
MEM_ADDR_TRANSFER_END : assert property (p9) $display (" MEMORY ADDRESS transfer ended ");
WRITE_TO_SLAVE_DETECT : assert property (p21) $display (" MASTER WRITES TO SLAVE ");
READ_FROM_SLAVE_DETECT : assert property (p22) $display (" MASTER READS FROM SLAVE ");
MEM_ADDR_ACK : assert property (p10) $display (" SLAVE generated ACK after memory address has been sent by master ");
MEM_ADDR_NACK : assert property (p24) $display (" SLAVE generated NACK after memory address has been sent by master ");
WRITE_DATA_TRANSFER_START : assert property (p11) $display (" DATA TRANSFER STARTED ");
//WRITE_DATA_TRANSFER_END : assert property (p12) $display (" DATA TRANSFER ENDED ");
DATA_ACK_BY_SLAVE : assert property (p13) $display (" SLAVE generated ACK ");
DATA_NACK_BY_SLAVE : assert property (p25) $display (" SLAVE generated NACK after data has been sent by master ");
READ_DATA_TRANSFER_START : assert property (p14) $display (" DATA TRANSFER STARTED ");
//READ_DATA_TRANSFER_END : assert property (p15) $display (" DATA TRANSFER ENDED ");
DATA_ACK_BY_MASTER : assert property (p16) $display (" MASTER generated ACK after data has been sent by SLAVE ");
DATA_NACK_BY_MASTER : assert property (p26) $display (" MASTER generated NACK after data has been sent by SLAVE ");
REP_START_1 : assert property (p17) $display (" RPEATED START DETECTED (No response to the SLAVE ADDRESS sent) ");
REP_START_2 : assert property (p18) $display (" REPEATED START DETECTED (SLAVE generated NACK after the MEMORY ADDRESS has been sent by the MASTER) ");
REP_START_3 : assert property (p19) $display (" REPEATED START DETECTED (SLAVE generated NACK after the DATA has been sent by the MASTER) ");
REP_START_4 : assert property (p20) $display (" REPEATED START DETECTED (MASTER generated NACK after the DATA has been sent by the slave) ");
ILLEGAL_FORMAT : assert property (p27) $display (" ILLGEAL FORMAT:START followed by STOP in the next cycle ");
endmodule