module edge_detector(sign_i, // Input of the Edge Detector
rise_o, // Rising Edge Output of the Edge Detector
fall_o, // Falling Edge Output of the Edge Detector
clk, // clock
rst_b, // Synchronous Reset
);

//--------------------- Parameters Declaration ---------------------------------
parameter SIZE = 1;

//-------------------- Inputs Declaration --------------------------------------
input [SIZE-1:0]sign_i;
input clk;
input rst_b;


//---------------------- Outputs Declaration -----------------------------------
output [SIZE-1:0]rise_o;
output [SIZE-1:0]fall_o;

//------------------- Types Declaration ----------------------------------------
wire clk;
wire rst_b;
wire [SIZE-1:0]sign_i;
wire [SIZE-1:0]rise_o;
wire [SIZE-1:0]fall_o;
reg [SIZE-1:0]sign_i_syn;
reg [SIZE-1:0]out_ff2;
wire [SIZE-1:0]out_xor;

genvar i; // auxiliar variable to generate

generate for(i=0;i begin
//------------------------ Sequential Part ------------------------------------ 

always @(posedge clk)
begin
if (!rst_b)
begin

sign_i_syn[i]<=1'b0; //If reset occured clear flip flops

out_ff2<=1'b0; 

end //if(!rst) 

else 
begin 

sign_i_syn[i]<= sign_i[i]
//Transform the entering signal in synchronous 

out_ff2 [i] <= sign_i_syn[i]
//Update the second ff output value

end //else 
end //always @(posedge clk)


//-------------------------------- Combinational Part ------------------------ 

assign out_xor[i] = (sign_i_syn[i] ^ out_ff2[i]); 
// keeps the output from the xor in 1 for 1 period of clock in the rise or fall

assign rise_o[i] = (sign_i_syn[i] & out_xor[i]); 
// if the entering sinal has high level and the pulse in the xor output 
// represents a rising edge

assign fall_o[i] = ~(sign_i_syn[i] | ~out_xor[i]); 
// if the entering sinal has low level and the pulse in the xor output 
// represents a falling edge

end // for (generate) 
endgenerate

for i in {0,1,2} generate
begin: check1
{// psl check_init: assert (!value[i]) @rose(resetn);
end
endgenerate;

for i in {0,1,2} generate
begin: check1
{//psl RISING: assert always ( rose(sign_iΎ]) -> next PULSE(rise_o) 
// abort !rst_b)
// report "Rising Edge Failed " severity warning;
//@fell(clk); 
end
endgenerate;

generate for(i=0;i begin: Rise
//psl RISING: assert always ( rose(sign_iΎ]) -> next PULSE(rise_o) 
// abort !rst_b)
// report "Rising Edge Failed " severity warning;
//@fell(clk); 
end
endgenerate

probe -create -assertions -transaction -waveform -name RISING edge_detector_tb.edge_detector.RiseΎ].RISING