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

SVA properties (feature request) #120

Open
cliffordwolf opened this Issue Aug 20, 2016 · 8 comments

Comments

Projects
None yet
3 participants
@cliffordwolf
Contributor

cliffordwolf commented Aug 20, 2016

Hi,

I'm thinking about adding support for SVA properties to Yosys. However, it is pretty hard to do that without a simulator to test against. So I've tried all the free and free-as-in-free-beer Verilog simulators I could find, but none of them seem to support SVA properties. This is the test case I'm using right now:

module test (
  input clk, resetn, tvalid, tready,
  input [7:0] tdata
);
  property tvalid_reset;
    @(posedge clk)
      !(resetn) & !($isunknown(resetn))
      ##1 resetn
      |-> !tvalid;
  endproperty
  assert property (tvalid_reset) else $display("error: tvalid_reset");

  property tdata_stable;
    @(posedge clk)
      !($isunknown({tvalid,tready,tdata})) &
      resetn & tvalid & !tready
      ##1 resetn
      |-> $stable(tdata);
  endproperty
  assert property (tdata_stable) else $display("error: tdata_stable");
endmodule

(This code is derived from the ARM AXI4-Stream Protocol Assertions r0p1.)

Icarus Verilog (git head) doesn't really like that:

$ iverilog -g2012 test.sv 
test.sv:5: syntax error
test.sv:5: error: invalid module item.
test.sv:6: syntax error
test.sv:9: error: invalid module item.
test.sv:10: syntax error
test.sv:11: error: invalid module item.
test.sv:13: syntax error
test.sv:13: error: invalid module item.
test.sv:14: syntax error
test.sv:18: error: invalid module item.
test.sv:19: syntax error
test.sv:20: error: invalid module item.

However, I've seen that for example property and endproperty are at least supported by the lexer.

Are there any plans for supporting (a subset of) SVA properties in Icarus Verilog anytime soon?

@martinwhitaker

This comment has been minimized.

Show comment
Hide comment
@martinwhitaker

martinwhitaker Aug 24, 2016

Collaborator

Speaking for myself, I have no immediate plans to do so. I've never used SV assertions, but having had a quick flick through the relevant section of the standard, it looks like it's quite a big job. Supporting immediate assertions shouldn't be to hard - but that's not what you are interested in!

Do you actually need the simulator to check the assertions, or would it be enough to just parse the assertion statements and ignore them?

Collaborator

martinwhitaker commented Aug 24, 2016

Speaking for myself, I have no immediate plans to do so. I've never used SV assertions, but having had a quick flick through the relevant section of the standard, it looks like it's quite a big job. Supporting immediate assertions shouldn't be to hard - but that's not what you are interested in!

Do you actually need the simulator to check the assertions, or would it be enough to just parse the assertion statements and ignore them?

@cliffordwolf

This comment has been minimized.

Show comment
Hide comment
@cliffordwolf

cliffordwolf Aug 24, 2016

Contributor

Supporting immediate assertions shouldn't be to hard - but that's not what you are interested in!

This is also what Yosys currently supports. In module context:

assert property (<expression>);
assume property (<expression>);
restrict property (<expression>);

An within always and initial blocks:

assert (<expression>);
assume (<expression>);
restrict (<expression>);

It would already be helpful for some of my use cases if Icarus Verilog would support those, i.e. create an error if an assert or assume fails and simply ignore the restrict statement.

Do you actually need the simulator to check the assertions, or would it be enough to just parse the assertion statements and ignore them?

Well.. I'll take whatever I get. ;) Parsing and ignoring is certainly better than not parsing.

I also realize that implementing all of SVA is a huge effort. (And certainly not what I have in mind for Yosys anytime soon either.) Maybe we can start with just parsing the most important stuff in Icarus Verilog, and once I have a useful subset of SVA features implemented in Yosys I'll get in touch again with a feature request just for those things specifically.

Contributor

cliffordwolf commented Aug 24, 2016

Supporting immediate assertions shouldn't be to hard - but that's not what you are interested in!

This is also what Yosys currently supports. In module context:

assert property (<expression>);
assume property (<expression>);
restrict property (<expression>);

An within always and initial blocks:

assert (<expression>);
assume (<expression>);
restrict (<expression>);

It would already be helpful for some of my use cases if Icarus Verilog would support those, i.e. create an error if an assert or assume fails and simply ignore the restrict statement.

Do you actually need the simulator to check the assertions, or would it be enough to just parse the assertion statements and ignore them?

Well.. I'll take whatever I get. ;) Parsing and ignoring is certainly better than not parsing.

I also realize that implementing all of SVA is a huge effort. (And certainly not what I have in mind for Yosys anytime soon either.) Maybe we can start with just parsing the most important stuff in Icarus Verilog, and once I have a useful subset of SVA features implemented in Yosys I'll get in touch again with a feature request just for those things specifically.

@caryr

This comment has been minimized.

Show comment
Hide comment
@caryr

caryr Aug 27, 2016

Collaborator

Actually adding even basic support for concurrent SVAs is a fairly large task. I have read the various sections of the standard in the past and over the last half a year have had it as one of my work goals to learn SVAs in my free time. I have a fairly good understanding now. For Icarus here are the big things that I think are missing: parsing the SVAs, updating the timing model to match what is needed by the SVAs (preponed region, etc.), the various sampling functions, it looks like they also needs the concurrent expression rework I have been working on in the background for a few years now, adding support for the actual assertions, adding labels to statements (as I remember I tried this as a first step a while ago and ran into parsing issues with the current grammar) and probably a few other things. As I have been learning this I have been thinking about implementation, but I am certainly not ready to start adding them any time soon. I understand the need for and much about SVAs I just don't have time to work on them right now.

Collaborator

caryr commented Aug 27, 2016

Actually adding even basic support for concurrent SVAs is a fairly large task. I have read the various sections of the standard in the past and over the last half a year have had it as one of my work goals to learn SVAs in my free time. I have a fairly good understanding now. For Icarus here are the big things that I think are missing: parsing the SVAs, updating the timing model to match what is needed by the SVAs (preponed region, etc.), the various sampling functions, it looks like they also needs the concurrent expression rework I have been working on in the background for a few years now, adding support for the actual assertions, adding labels to statements (as I remember I tried this as a first step a while ago and ran into parsing issues with the current grammar) and probably a few other things. As I have been learning this I have been thinking about implementation, but I am certainly not ready to start adding them any time soon. I understand the need for and much about SVAs I just don't have time to work on them right now.

@cliffordwolf

This comment has been minimized.

Show comment
Hide comment
@cliffordwolf

cliffordwolf Aug 28, 2016

Contributor

[..] As I have been learning this I have been thinking about implementation, but I am certainly not ready to start adding them any time soon. I understand the need for and much about SVAs I just don't have time to work on them right now.

Sad, but perfectly understandable. Any chance we might get assert(...) and friends in always and initial blocks (aka immediate assertions) and assert property (...) in module context with ordinary expressions instead of properties, as described above?

(One could argue that everything else than immediate assertions is just "syntactic sugar" anyways, because with immediate assertions it's possible to check for any property simply by writing the corresponding checker state machines by hand.)

Contributor

cliffordwolf commented Aug 28, 2016

[..] As I have been learning this I have been thinking about implementation, but I am certainly not ready to start adding them any time soon. I understand the need for and much about SVAs I just don't have time to work on them right now.

Sad, but perfectly understandable. Any chance we might get assert(...) and friends in always and initial blocks (aka immediate assertions) and assert property (...) in module context with ordinary expressions instead of properties, as described above?

(One could argue that everything else than immediate assertions is just "syntactic sugar" anyways, because with immediate assertions it's possible to check for any property simply by writing the corresponding checker state machines by hand.)

@caryr

This comment has been minimized.

Show comment
Hide comment
@caryr

caryr Aug 29, 2016

Collaborator

To do asserts of any kind correctly we need statement labels. That was the primary issue i ran into when I looked at implementing immediate assertions earlier. Concurrent assertions are a bit more than just a state machine with immediate asserts since any value referenced except those in the clocking and disable parts of the assertion are sampled in the preponed phase. There's also the whole inherited clock from an always block, etc. that needs to be handled correctly.

Collaborator

caryr commented Aug 29, 2016

To do asserts of any kind correctly we need statement labels. That was the primary issue i ran into when I looked at implementing immediate assertions earlier. Concurrent assertions are a bit more than just a state machine with immediate asserts since any value referenced except those in the clocking and disable parts of the assertion are sampled in the preponed phase. There's also the whole inherited clock from an always block, etc. that needs to be handled correctly.

@cliffordwolf

This comment has been minimized.

Show comment
Hide comment
@cliffordwolf

cliffordwolf Aug 30, 2016

Contributor

[..] are sampled in the preponed phase.

Clearly you've had a deeper look into that topic than I. Also: I'm approaching this from the point of view of formal verification, which is essentially is synthesis as far as the verilog interface is concerned. So I have not really payed much attention to how this interfaces with the Verilog stratified event loop..

I still think that immediate assertions would be a useful addition that shouldn't be too hard to implement.

I also think that treating assert property (<expr>); like always @* assert (<expr>); (i.e. concurrent assertion with simple expression instead of sequence or property) could be useful, but I agree that it should be avoided if that results in any observable differences to what the standard says.

I personally don't like SVA much and am pretty happy with only immediate assertions in my code. (One of the advantages of this is that the internal state of the assertion is observable when using hand written FSMs with immediate assertions.) If we could have immediate assertions in yosys and iverilog I'd be pretty happy. I'd just send users asking for more to this thread.. ;)

Contributor

cliffordwolf commented Aug 30, 2016

[..] are sampled in the preponed phase.

Clearly you've had a deeper look into that topic than I. Also: I'm approaching this from the point of view of formal verification, which is essentially is synthesis as far as the verilog interface is concerned. So I have not really payed much attention to how this interfaces with the Verilog stratified event loop..

I still think that immediate assertions would be a useful addition that shouldn't be too hard to implement.

I also think that treating assert property (<expr>); like always @* assert (<expr>); (i.e. concurrent assertion with simple expression instead of sequence or property) could be useful, but I agree that it should be avoided if that results in any observable differences to what the standard says.

I personally don't like SVA much and am pretty happy with only immediate assertions in my code. (One of the advantages of this is that the internal state of the assertion is observable when using hand written FSMs with immediate assertions.) If we could have immediate assertions in yosys and iverilog I'd be pretty happy. I'd just send users asking for more to this thread.. ;)

@caryr

This comment has been minimized.

Show comment
Hide comment
@caryr

caryr Aug 31, 2016

Collaborator

Immediate assertions at the fundamental level are fairly trivial to implement. Like I said earlier the issue I ran into when I looked at this a year or so ago was related to adding statement labels to the grammar. I could not figure out a way to add them cleanly. Without a label, controlling the assertions using the various systems functions/VPI is not really possible. If we don't care about a label then adding basic immediate assertions and possibly even the deferred immediate assertions should be fairly easy. The other issue with skipping the label is it is usually used in the assert message to identify which assert is failing.

Conceptually, implementing preponed support and much of the rest of concurrent assertions is not too hard, but without a label this can become more of an issue since concurrent asserts are often disabled during power on, etc. to avoid false triggering. Yes they have support for a reset/disable, but knowing what this should be is often not trivial so people often just disable them until some global event happens (e.g. power on done).

I believe we need support for statement labels in the various places where an assert can be used before we can actually add the asserts. Verilog is hard to parse and yacc/bison may not have enough power to do it. I ran into an issue that I could not work around when looking at adding support for external methods (which are needed to support SVUnit). We may be hitting the limits of what can be done with yacc/bison or maybe it's just my knowledge limits.

Collaborator

caryr commented Aug 31, 2016

Immediate assertions at the fundamental level are fairly trivial to implement. Like I said earlier the issue I ran into when I looked at this a year or so ago was related to adding statement labels to the grammar. I could not figure out a way to add them cleanly. Without a label, controlling the assertions using the various systems functions/VPI is not really possible. If we don't care about a label then adding basic immediate assertions and possibly even the deferred immediate assertions should be fairly easy. The other issue with skipping the label is it is usually used in the assert message to identify which assert is failing.

Conceptually, implementing preponed support and much of the rest of concurrent assertions is not too hard, but without a label this can become more of an issue since concurrent asserts are often disabled during power on, etc. to avoid false triggering. Yes they have support for a reset/disable, but knowing what this should be is often not trivial so people often just disable them until some global event happens (e.g. power on done).

I believe we need support for statement labels in the various places where an assert can be used before we can actually add the asserts. Verilog is hard to parse and yacc/bison may not have enough power to do it. I ran into an issue that I could not work around when looking at adding support for external methods (which are needed to support SVUnit). We may be hitting the limits of what can be done with yacc/bison or maybe it's just my knowledge limits.

@cliffordwolf

This comment has been minimized.

Show comment
Hide comment
@cliffordwolf

cliffordwolf Sep 1, 2016

Contributor

We may be hitting the limits of what can be done with yacc/bison

jfyi: Bison can generate GLR parsers. With that bison can parse any context-free grammar, not just LR(1) grammars.

Contributor

cliffordwolf commented Sep 1, 2016

We may be hitting the limits of what can be done with yacc/bison

jfyi: Bison can generate GLR parsers. With that bison can parse any context-free grammar, not just LR(1) grammars.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment