1.When $rose(sig1) it will check for
if(sig4==1) If yes.
then check should be $rose(sig5) then $fell(sig1) followed by $fell(sig5).
else
$rose(sig1)-> $rose(sig4)->$rose(sig5)-> $fell(sig1)-> $fell(sig4)-> $fell(sig5)-It should be error if sig1->
followed by sig5 asserted without sig1,
if(sig2 asserted)check $rose(sig4) followed by $rose(sig3)-> [*] it should be error sig2 asserted then sig3 asserted with out sig4.
Please help me with my requirement. I tried multiple ways I am always finding either assertion no attempt.
I was not able to upload URL, basically not sure about how to upload URL?
In reply to BhaRath@Intel:
You are trying to express your requirements using an SVA notation with so many implication operators that it is hard to really understand what you need.
You need to express your requirement in English. The implication opr has a very significant meaning. I attempted at making sense on what you wrote, but it does not make sense. I am posting my attempt, not as a solution, but as failed attempt because it is totally unclear.
property_statement ::= // 1800'2017
property_expr ;
| case ( expression_or_dist ) property_case_item
{ property_case_item } endcase
| if ( expression_or_dist ) property_expr
[ else property_expr ]
// ???
ap_very_ambiguous: assert property(@ (posedge clk) $rose(sig1) |->
if(sig4==1) $rose(sig5) ##1 $fell(sig1) ##1 $fell(sig5)
else $rose(sig1)-> $rose(sig4)->$rose(sig5)-> $fell(sig1)-> $fell(sig4)-> $fell(sig5)
// Way way too many |->.
// Also, all these 4rose at the same time? Can you use the && or the ##0?
// What is the English requirement
//????
// -It should be error if sig1->
// followed by sig5 asserted without sig1,
ap_ambiguous_Englis: assert property(@ (posedge clk) not sig5 && sig1 );
Sorry for mixing up the requirement in SVA and English description.
Now I will explain my requirement:
1.when clkreq asserted I should check for valid which needs to be get asserted within 500clocks, then clkack should get asserted.
2.If force_on asserted then validmust be asserted then force_on_ack must be asserted followed by force_on deassert, valid deassert, force_on_ack deassert.
3.In second case when force_on asserted it will check for valid, If valid already asserted due to clkreq it should go ahead and check for force_on_ack assertion followed we need to check for force_on deassertion and force_on_ack deassertion.
Thank you for your help…I tried to make all logic in single property but which is leading to nomatch case evethough signals are getting toggled.
In reply to BhaRath@Intel:
You still have some ambiguity in the English definition of the requirements, something that when translating the English into SVA clearly brings out. BTW, this is one of the nice things of SVA, it forces the user to clarify the requirements.
Specifically, you were ambiguous as to when the “then” means, SAME cycle or the NEXT cycle.
I made some assumptions for you, but you need to fix it according to your real requirements.
I also changed the name of clkreq to req.
module top;
timeunit 1ns/100ps;
bit clk, req, valid, force_on, force_on_ack, ack;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
// 1.when req asserted I should check for valid that needs to be get asserted within 500clocks,
// then ack should get asserted IN THE NEXT CYCLE.
ap_req_valid: assert property(@ (posedge clk) $rose(req) |->
first_match(##[1:500] valid) ##1 ack);
// first_match() is needed here
// --------------------
// If force_on asserted then valid must be asserted IN THE NEXT CYCLE(?)
// then (##0 or ##1 ?)force_on_ack must be asserted followed IN THE NEXT CYCLE by force_on deassert,
// valid deassert, force_on_ack deassert.
ap_force_on: assert property(@ (posedge clk) $rose(force_on) |->
##1 force_on_ack ##1 $fell(force_on) ##0 !valid ##0 !force_on_ack);
// ##0 or ##1 spec is poorly defined
// -----------------------
/* In second case when force_on asserted it will check for valid (NExt or same cycle?) ,
If valid already asserted due to clkreq it should go ahead
and check for force_on_ack assertion followed
we need to check for force_on deassertion and force_on_ack deassertion. */
ap_force_on_valid: assert property(@ (posedge clk) $rose(force_on) ##1 valid |->
##1 force_on_ack ##1 $fell(force_on) ##0 !force_on_ack);
endmodule
I need update in below assertion to make sure I check properly:
// 1.when req asserted I should check for valid that needs to be get asserted within 500clocks,
// then ack should get asserted IN THE NEXT CYCLE.
ap_req_valid: assert property(@ (posedge clk) $rose(req) |->
first_match(##[1:500] valid) ##[1:200000] ack);
How can I modify the above assertion to make sure valid between req and ack always asserted?
If req asserted followed by ack asserted and no valid asserted means an Error.
In the above check, it is checking for req first and if valid asserted then checking for ack.
In another way I want to check for valid must exist in between req and ack.
// valid must exist in between req and ack.
// The following is ILLEGAL
ap_desired_but_ILLEGAL : assert property(@ (posedge clk)
rose(valid) |-> $past(1:$, was_a_req)); //
// Instead, store the fact that a "req" occured. reset when valid
bit was_a_req;
always @(posedge clk) begin
if(req) was_a_req <= 1'b1;
if(valid) was_a_req <= 1'b0;
end
ap_valid_req: assert property(@ (posedge clk)
$rose(valid) |-> was_a_req);