Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add properties to verify dst and we #10

Merged
merged 7 commits into from
Oct 27, 2024
Merged

Conversation

TWstinkytofu
Copy link
Collaborator

  1. Add properties to verify dst and we
  2. Try to use goto amd intersect to double check the coverage of jal

@TWstinkytofu TWstinkytofu force-pushed the a3012085/modified_jal_property branch from 331a5cd to 27a7e62 Compare October 23, 2024 16:23
a3012085 added 2 commits October 24, 2024 09:31
 - check_goto_meaning -> check_jal_coverage
property/isa.sv Outdated Show resolved Hide resolved
property/isa.sv Outdated Show resolved Hide resolved
property/isa.sv Outdated Show resolved Hide resolved
property/isa.sv Outdated
endproperty : E2E_JAL_RD

property E2E_JAL_WE1; // rd != 0 -> must enable write;
@(posedge clk) disable iff (rst) VALID_JAL |-> (|wb_inst_dc.rd |-> (core.wb_we == 1));
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

|wb_inst_dc.rd can be moved to precondition

Suggested change
@(posedge clk) disable iff (rst) VALID_JAL |-> (|wb_inst_dc.rd |-> (core.wb_we == 1));
@(posedge clk) disable iff (rst) VALID_JAL && (|wb_inst_dc.rd) |-> (core.wb_we == 1);

property/isa.sv Show resolved Hide resolved
property/isa.sv Show resolved Hide resolved
@fennecJ
Copy link
Owner

fennecJ commented Oct 27, 2024

LGTM: )

@fennecJ fennecJ merged commit 63e8edc into master Oct 27, 2024
2 checks passed
@fennecJ fennecJ deleted the a3012085/modified_jal_property branch December 28, 2024 06:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants