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

assert property with iff fails to compile #4848

Open
udif opened this issue Jan 21, 2024 · 1 comment
Open

assert property with iff fails to compile #4848

udif opened this issue Jan 21, 2024 · 1 comment
Labels
area: assertions Issue involves assertions status: ready Issue is ready for someone to fix; then goes to 'status: assigned' type: feature-IEEE Request to add new feature, described in IEEE 1800

Comments

@udif
Copy link
Contributor

udif commented Jan 21, 2024

Please see #4846 which just includes a test case but not a fix.

Thanks for taking the time to report this.

Can you attach an example that shows the issue? (Must be openly licensed, ideally in test_regress format.)

The following assert fails to compile:
a: assert property (disable iff(rst !== 1'b0) @(posedge clk) !x);

What 'verilator' command line do we use to run your example?

verilaotr --lint-only

What 'verilator --version' are you using? Did you try it with the git master version?

Verilator 5.021 devel rev v4.108-2463-g1a9250278

What OS and distribution are you using?

Ubuntu 22.04LTS

May we assist you in trying to fix this in Verilator yourself?

I have no experience with the Verilator code generator.
Getting this parsed is probably not be too hard, but I don't know to what extent does Verilator supports assertions at the moment, and what is expected from a full fix (is it just getting no error, or is the assertion supposed to work, honoring the iff() condition).

@udif udif added the new New issue not seen by maintainers label Jan 21, 2024
@wsnyder wsnyder added area: assertions Issue involves assertions status: ready Issue is ready for someone to fix; then goes to 'status: assigned' type: feature-IEEE Request to add new feature, described in IEEE 1800 and removed new New issue not seen by maintainers labels Jan 21, 2024
@wsnyder
Copy link
Member

wsnyder commented Jan 21, 2024

Based on your pull, here's a patch that is also self testing:

diff --git a/test_regress/t/t_assert_named_property.v b/test_regress/t/t_assert_named_property.v
index 7fed4f620..6c3035293 100644
--- a/test_regress/t/t_assert_named_property.v
+++ b/test_regress/t/t_assert_named_property.v
@@ -74,8 +78,14 @@ module t (/*AUTOARG*/
    assert property (prop_b) else $error($sformatf("property check failed :assert: (False)"));
    assert property (prop_b()) else $error($sformatf("property check failed :assert: (False)"));

+   bit got_diclk_fail;
+   diclk_ok: assert property (disable iff (cyc <= 5) @(posedge clk) cyc >= 5);
+   diclk_fail: assert property (disable iff (cyc < 5) @(posedge clk) cyc >= 5)
+     else got_diclk_fail = 1'b1;
+
    always @(posedge clk) begin
       if (expected_fails == 2) begin
          if (got_diclk_fail != 1'b1) $stop;
          $write("*-* All Finished *-*\n");
          $finish;
       end

I added a warning this is not supported. As to implementing the problem is that the disable needs to take effect BEFORE the edge is looked for, and there's no easy way to do represent this presently. I would recommend using the opposite flavor:

assert property (@(posedge clk) disable iff (cyc <= 5) cyc >= 5);

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area: assertions Issue involves assertions status: ready Issue is ready for someone to fix; then goes to 'status: assigned' type: feature-IEEE Request to add new feature, described in IEEE 1800
Projects
None yet
Development

No branches or pull requests

2 participants