SVA : Assertion checking for multiple signals samipling on different of clocks

HI,

I have a question regarding writing an assertion.I need and idea for the following diagram

http://j61i.imgup.net/waveform782a.png

My requirement is to write assertion for the boot sequence wave form.
Observing the diagram,i dont know the no.of clock cycles required between two signals.

So I Coded in the following way :

sequence p_iopi_vccaopi_powergood();
@(posedge iopi_vccaopi_powergood)
((iopi_vcccore_powergood == 1’b1) && (iopi_vccasyncsb_powergood == 1’b1));
endsequence

sequence p_iopi_vccaopi_powergood_rst_b();
@(posedge iopi_vccaopi_powergood_rst_b)
(1==1);
endsequence

sequence p_iopi_pma_phy_pmctrl_vccaopig_en();
@(posedge iopi_pma_phy_pmctrl_vccaopig_en)
(1==1);
endsequence

sequence p_oopi_phy_pma_pmctrl_vccaopig_stable();
@(posedge oopi_phy_pma_pmctrl_vccaopig_stable)
(1==1);
endsequence

sequence p_iopi_pmc_sbwake();
@(posedge iopi_pmc_sbwake)
(1==1);
endsequence

I have declared all the sequences w.r.t to signals and included in the CLKEVENT sequence.
So based on the sequence triggering it can trigger CLKEVENT.

sequence CLKEVENT;@(
p_iopi_vccaopi_powergood or
p_iopi_vccaopi_powergood_rst_b or
p_iopi_pma_phy_pmctrl_vccaopig_en or
p_oopi_phy_pma_pmctrl_vccaopig_stable or
p_iopi_pmc_sbwake or
p_oopi_sb_side_clkreq or
p_iopi_sb_side_clkack or
p_oopi_pmc_sbpwr_stable or
p_iopi_pma_phy_pmctrl_en or
p_iopi_side_reset_b or
p_oopi_iosf_side_pok or
p_iopi_pll_en or
p_oopi_pllrefclk_clkreq or
p_iopi_pllrefclk_clkack or
p_oopi_pll_lock or
p_iopi_lane_reset_b or
p_oopi_strobelane0_acknowledge or
p_oopi_strobelane1_acknowledge or
p_iopi_cmln_reset_b or
ev_fusepullreq or
ev_fusepullcompletion or
ev_ipready or
ev_inaccessablemsg or
ev_flag
) (1==1); endsequence

always @(CLKEVENT
)begin

cp_RESET_BOOTUP1 : assert property (p_iopi_vccaopi_powergood |=> p_iopi_vccaopi_powergood_rst_b |=> p_iopi_pma_phy_pmctrl_vccaopig_en |=> p_oopi_phy_pma_pmctrl_vccaopig_stable |=> p_iopi_pmc_sbwake |=> p_oopi_sb_side_clkreq |=> p_iopi_sb_side_clkack);

end

  1. The problem assertion is not responding with fail or success.
  2. For my case it should FAIL.But assertion is not responding.
    3)I would like to know about the coding style.(Suggestion : Any other way of implementation / modification in it)

-Regards,
-Raja.

In reply to sraja:
The problem with your request for a solution are the following:

  • Your problem definition is too complex to explain and understand
  • You seem to be going form a solution (timing diagram or RTL) to an assertion. It is far better to go from requirements to a set of assertions. Translating RTL to assertions is meaningless.
  • If you want help from this forum, it is usually best to explain your requirements using simple terms (like “a”, “b”), and states the requirements, not the RTl
  • A set of smaller assertions s better than a single assertion.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

In reply to sraja:

Dear Sraja,

To simplify your task it is better to start from the specification, extract the properties and then write down your assertions.

As Ben said, In verification principle you don’t have to start from the design code, or RTL. You need the specification document( design requirements not the implementation document )

The diagram you mentioned seems to be complex, if you don’t have the specification document you are missing the starting point.