In reply to sidmodi:
Looks to me like you are coming from the VHDL world.
In sequences, you have the following operators that are not equivalent than logical operators:
and or // sequential operators
&& || // expression logica operator
// thus, when you write
.. (reg_push and reg_alert_bit and (reg_addr == 32'h20000080 or reg_addr == 32'h20000088))
// You have 3 sequences, each 1-cycle wide
// Sice sequences can be 1-cycle wide the compiler does not complain.
// However, using 1-cycle "and" "or" have different connotaton than using the logical && ||
The following does read better and expresses the intent better.
.. (reg_push && reg_alert_bit && (reg_addr == 32'h20000080 || reg_addr == 32'h20000088))
// On
property rsp_not_empty_alert_high_p(empty, alert);
@(posedge clk) empty == 0 |=> alert == 1;
endproperty
rsp_not_empty_alert_check: assert property (rsp_not_empty_alert_high_p
(rsp.empty, raw_alert[27]) [*0:$] ##1
alert_bit_clear_p(reg.push,
reg.data[27],
reg.data[63:32],
raw_alert[27]));
The actual arguments being passed to property (rsp_not_empty_alert_high_p are not compatible with the formal arguments. In your case, formal argument
// If you are going to use formal arguments, If all formals are bits,
// I prefer to use untyped as the type.
// However, if you intend to use sequences, then declare the type as a sequence;
// it makes the code more readable.
sequence q_ab(z, y);
z ##2 y;
endsequence
property p_abc(x, sequence w);
x ##1 w;
endproperty
ap: assert property(@ (posedge clk) $rose(c) |=>
p_abc(d, q_ab(d, q_ab(a, b))));
// However, if those assertions are used once, why do you really bother with all these arguments? Just go straight for the kill
ap_better: assert property(@ (posedge clk) $rose(c) |=>
d ##1 a ##2 b); // p_abc(d, q_ab(d, q_ab(a, b))));
// Even better, Use the defaults clocking and disables
default disable iff (rst);
default clocking @(posedge clk);
endclocking
ap_better: assert property( $rose(c) |=>
d ##1 a ##2 b); // p_abc(d, q_ab(d, q_ab(a, b))));
To be honest, I’m coming from the firmware world. I am quite new to the hardware description world.
I understand what you mean about the difference between ‘and/or’ and ‘&& / ||’. It makes sense to use the logical operators in my case.
What I am still not clear about is your explanation regarding the arguments being passed to the property. I am defining the property with arguments because I intend to use the same property to verify the functionality of multiple signals. With arguments, I can verify all those signals using the same property. All the parameters to the ‘rsp_not_empty_alert_high_p’ and ‘alert_bit_clear_p’ properties are bits.
What I am trying to achieve in plain language is the following:
Once asserted, I want the property ‘rsp_not_empty_alert_high_p’ to be true until ‘alert_bit_clear_p’ gets asserted.
I tried to do this by declaring two separate properties and then inserting a property operator between them in the assertion. I am not quite sure what I’m doing wrong here…
// 'rsp_not_empty_alert_high_p' to be true until 'alert_bit_clear_p' gets asserted.
// Or, looking at you code
property rsp_not_empty_alert_high_p(empty, alert);
@(posedge clk) empty == 0 |=> alert == 1;
endproperty
property alert_bit_clear_p(reg_push, reg_alert_bit, reg_addr, raw_alert_bit);
@(posedge clk) (reg_push and reg_alert_bit and (reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) |-> ##3 $fell(raw_alert_bit);
endproperty
// And then breaking it down to the core:
// You want
(empty == 0 |=> raw_alert[27]) [*0:$]) until
(reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) |-> ##3 $fell(raw_alert_bit)
// In SVA, you do have the "until" operator
property_expr1 until property_expr2
/* "An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true" */
// To me, the "until operator is confusing and hard o understand for complex properties
// unless those properties are single bits. For example:
$rose(req) |=> busy until ready); // Enhanced readability, and Identical to
// $rose(req) |=> busy[*0:$] ##1 ready ; // equivalent property expression
// Perhaps what you need is the "intersect of 2 sequences", something like:
(empty == 0 ##1 raw_alert[27] |-> raw_alert[27]) [*1:$]) intersect
(reg_addr == 32'h20000080 || reg_addr == 32'h20000088) ##3 $fell(raw_alert_bit)
// Or in English, if (empty == 0 ##1 raw_alert[27] then
// raw_alert[27]) holds at all cycles While this sequence is true
// (reg_addr == 32'h20000080 || reg_addr == 32'h20000088) ##3 $fell(raw_alert_bit)