for/generate

Well, in my newbe condition in this forum I had problem posting the codes :)

The first code is :
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



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



The third:

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



The fourth:

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


The sixth:

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

Thanks and sorry about that,

I tried doing this using IUS 6.11 and everything seemed to work fine for me. I did have to interpolate a little since the code that I cut-and-pasted from this thread needed some massaging to compile.

Your original syntax problem appears to be because you put some PSL code into your HDL model without using the "// psl" comment prefix. So the Verilog parser was trying to parse the PSL as if it was Verilog. If the Cadence examples have code without the PSL prefix in them, then I think that they are wrong. Can you point me to the document you were referencing?

Secondly, using a Verilog loop-generate seems to work fine. If anyone can tell me how to upload a 'tar.gz' file to this forum, I could post an example that takes everything thru the process and displays the assertion as a transaction in a waveform window at the end. Personally, I think it is a little too much code to post in-line.

HI,

To attach a file do not use "Quick Reply" but click "Add Reply instead. 

You can use the "Message Attachments" field to attach files to upload.

Regards,

JB

Ok then. :-)

Here is a small example that, if you run it using IUS 6.11, should pop up a waveform window with your assertion displayed as a transaction.