//   ==================================================================
//   >>>>>>>>>>>>>>>>>>>>>>> COPYRIGHT NOTICE <<<<<<<<<<<<<<<<<<<<<<<<<
//   ------------------------------------------------------------------
//   Copyright (c) 2017 by Lattice Semiconductor Corporation
//   ALL RIGHTS RESERVED  
//   ------------------------------------------------------------------
//
//   Permission:
//
//      Lattice SG Pte. Ltd. grants permission to use this code
//      pursuant to the terms of the Lattice Reference Design License Agreement. 
//
//
//   Disclaimer:
//
//      This VHDL or Verilog source code is intended as a design reference
//      which illustrates how these types of functions can be implemented.
//      It is the user's responsibility to verify their design for
//      consistency and functionality through the use of formal
//      verification methods.  Lattice provides no warranty
//      regarding the use or functionality of this code.
//
//   --------------------------------------------------------------------
//
//                  Lattice SG Pte. Lt++++++++++++++++d.
//                  101 Thomson Road, United Square #07-02 
//                  Singapore 307591
//
//
//                  TEL: 1-800-Lattice (USA and Canada)
//                       +65-6631-2000 (Singapore)
//                       +1-503-268-8001 (other locations)
//
//                  web: http://www.latticesemi.com/
//                  email: techsupport@latticesemi.com
//
// --------------------------------------------------------------------
//
//  Project:           iCE5UP 5K RGB LED Tutorial 
//  File:              testbench.v
//  Title:             LED PWM control
//  Description:       Creates RGB PWM per control inputs
//                 
//
// --------------------------------------------------------------------
//
//------------------------------------------------------------
// Notes:
//
//
//------------------------------------------------------------
// Development History:
//
//   __DATE__ _BY_ _REV_ _DESCRIPTION___________________________
//   04/05/17  RK  1.0    Initial tutorial design for Lattice Radiant
//
//------------------------------------------------------------
// Dependencies:
//
// 
//
//------------------------------------------------------------



//------------------------------------------------------------
// 
//
//                     Testbench
//
//------------------------------------------------------------

class Rst_rnd;
	rand bit [1:0] data;
	constraint Rst_rnd
	{
	data dist {0:=70,1 :=30};
	}
endclass
class Data_valid_rnd;
	rand bit [1:0] data;
	constraint Data_valid_data
	{
	data dist {0:=10,1 :=90};
	}
endclass

class Data_input_rnd;
	rand bit [7:0] data;
endclass




`timescale 1ns/1ps
// inputs and outputs
module tb;
reg clk12M;
reg rst;
reg [7:0]data_input;
reg data_valid;
wire RED;
wire GRN;
wire alarm;
//random
Rst_rnd rst_rnd = new();
Data_valid_rnd data_valid_rnd = new();
Data_input_rnd data_input_rnd = new();
// connect module
led_top dut(.clk12M(clk12M),
			.rst(rst),
			.data_input(data_input),
			.data_valid(data_valid),
			.RED(RED),
			.GRN(GRN),
			.alarm(alarm)
			);     
//clock
initial
begin
    clk12M=1'b0;
end
always 
  #41.666666 clk12M=~clk12M;                             //clock generation
  int cycles = 0;
//random test
 initial begin       
	repeat (50) begin
		#50000
		cycles =cycles+1;
		rst_rnd.randomize();
		data_input_rnd.randomize();
		data_valid_rnd.randomize();
		rst = rst_rnd.data;
		data_input = data_input_rnd.data;
		data_valid = data_valid_rnd.data;
		// assertions
		// assert that reset resets
		assert property ( @(posedge clk12M) (##1 rst) |=> !alarm);
		// assert color green
		assert property(@(posedge clk12M) disable iff (rst | !data_valid| alarm) ((data_input < 100) |=> ##4 (!RED && GRN));
		
		//assert color yellow
		
		assert property(@(posedge clk12M) disable iff (rst | !data_valid| alarm) ((data_input >= 100) && (data_input <= 168))|=> ##4 (RED && GRN));
		
		//assert color red + alarm
		
		assert property(@(posedge clk12M) disable iff (rst | !data_valid) (data_input > 168) |=> ##4 (RED && !GRN && alarm));
		$monitor("time=%t,cycle%d, rst=%d, data_input=%d, data_valid = %d, RED=%d, GRN=%d, alarm=%d",$time,cycles,rst,data_input, data_valid, RED, GRN, alarm);
	end
	$stop;
end

endmodule