Handling non-LRM system functions

[abradd]

If I have the following code in test.sv:

module test (
    input logic clock
);

    logic test1 = 1'b0;
    wire  test2 = 1'b0;

    always @(posedge clock) begin
        if (!$initstate) begin
        end
    end
    
endmodule : test

and I run slang -Weverything test.sv I receive the following error:

tb/test.sv:9:14: error: unknown system name '$initstate'
        if (!$initstate) begin
             ^~~~~~~~~~

Given that $initstate is not in the LRM, the error is valid. $initstate is provided by sby and used as part of formal verification.

I had two questions:

1. Is it possible to filter this error? I found a warning reference in the docs and methods for filtering warnings, but couldn't find anything about filtering errors.

2. Are errors supposed to mask warnings? In the above example I have an unused-net and unused-variable warning that are masked unless I comment out the conditional containing $initstate.

[MikePopoloski]

There is currently no way to filter the error (by definition, errors cannot be filtered out). Typically tool-specific code is hidden behind an ifdef so that it can still be run through other tools, but you may have good reasons for not wanting to do that. I could change the error to be a warning that is by default promoted to an error; that would allow you to demote it back down to a warning or ignore it using typical warning options.

Errors do not in general mask all warnings, but slang does avoid issuing warnings when there are errors that could make such warnings ambiguous and therefore unhelpful noise. In particular if there are any errors slang won't check for unused nets and variables because it's often the case that such warnings are just nonsensical when there are real errors in the code.

[MikePopoloski]

Made this suppressible in fe10323

[abradd]

Typically tool-specific code is hidden behind an ifdef so that it can still be run through other tools, but you may have good reasons for not wanting to do that.

Apologies for the confusion. In my attempt to create a minimal example I accidentally obfuscated the way this system function is typically used. As you say it is typically placed within an ifdef as below:

module test (
    input logic clock
);

    // design code purposefully left out

    `ifdef FORMAL
    logic test1 = 1'b0;
    wire  test2 = 1'b0;

    always @(posedge clock) begin
        if (!$initstate) begin
        end
    end
    `endif
    
endmodule : test

You don't have to specify the ifdef to use the formal tool, but the simulator would likely throw an error as $initstate is a formal-specific system function only defined in sby as far as I know. For context, if you are using the free version (oss cad suite) of these formal tools you don't have access to SV commands like bind so the formal commands are usually written inline with your design (or included). Beyond the use of the $initstate function, the formal code is LRM-compliant (at least what I have seen so far) which is why I'm using slang to check it for issues.

It may be better to not treat all such unknown system functions the same as that could cause you to miss actual unknown system functions.

My original thought was to have some sort of valid-list for custom system functions, but I have no sense for how difficult that would be to implement and maintain. A commercial linting tool I've used in the past would allow you to define a configuration file and filter warnings/errors based on the contents of the warning message. So any unknown system function error containing "$initstate" would be filtered.

Errors do not in general mask all warnings, but slang does avoid issuing warnings when there are errors that could make such warnings ambiguous and therefore unhelpful noise.

Makes sense.

[abradd]

I did some additional testing using the code below:

module test (
    input logic clock
);

    // design code purposefully left out

    `ifdef FORMAL
    logic test1 = 1'b0;
    wire  test2 = 1'b0;

    always @(posedge clock) begin
        `pragma diagnostic ignore="-Wunknown-sys-name"
        if (!$initstate) begin
        `pragma diagnostic warn="-Wunknown-sys-name"
        //`pragma diagnostic error="-Wunknown-sys-name"
        end
    end
    `endif
    
endmodule

If i run slang with:

slang -Weverything -DFORMAL test.sv

I can filter each of the errors/warning of $initstate using diagnostic pragmas. After filtering I can reassert the warning/error. This is a little verbose, but works for slang. Unfortunately, sby errors out as pragma is undefined.

[MikePopoloski]

You need to put the pragmas behind an ifdef as well. Alternatively you can define it away with a common macro. Something like:

`ifdef __slang__
`define SBY(x) 1
`else
`define SBY(x) x
`endif

module m;
    always @(posedged clk) begin
        if (!`SBY($initstate)) begin end
    end
endmodule

[abradd]

Thanks for the ifdef __slang__ suggestion.

`ifdef __slang__
`define SBY(x) 1
`else
`define SBY(x) x
`endif

Does slang track the use of specific system functions in the AST? If so, would this structure prevent the system function from being in the AST by setting it to "1"?

I don't have any specific use-case, but it seems reasonable to keep the use of $initstate (or any unknown system function) in the tree in case it has some use in the future.

Here is an option that ifdefs the pragmas and is working for me:

`define unknownSys(handle) \
  `ifdef __slang__\
  `pragma diagnostic handle="-Wunknown-sys-name"\
  `endif

module m;
  always @(posedged clk) begin
    `unknownSys(ignore)    
    if ($initstate) begin 
    `unknownSys(error)  
    end  
  end
endmodule

[abradd]

I discovered that slang doesn't detect a lack of `endif in conditional compilation directives. My interpretation of Sec 22.6 of the LRM is that the `endif is mandatory. So the following should be invalid:

`define unknownSys(handle) \
  `ifdef __slang__\
  `pragma diagnostic handle="-Wunknown-sys-name"

I can submit this as a separate issue/discussion if preferred.

[abradd]

Yeah, that's odd, you can submit an issue for it.

Will do.

To answer your other question, yes the system function is represented in the AST, but only if slang actually knows what it is. Otherwise you're going to have an error node in the expression tree where it's called.

In that case it seems like either the idef + pragma or defining it away with a macro are equally suitable.

Maybe this doesn't matter because all of the ones you would want to add are just normal old functions.

Indeed in this case the function doesn't take any arguments. But it is also the only non-LRM system function I use (or know of) for formal so it isn't a burden to handle it with pragmas or macros.

but it's tricky because some system functions can't actually be declared using SystemVerilog syntax so how would you represent them?

I'm afraid I don't understand this. I understand that arguments to system functions like $typename are not of fixed types and their return values could change, but I don't see how that prevents them from being declared using SystemVerilog syntax. Are the system functions being mapped to normal functions which require pre-defined types?

[MikePopoloski]

What I meant is that if you wanted to provide a file defining extra system functions that slang should know about, what kind of syntax would you use in that file to declare special functions that have unrepresentable return types or have other effects on the AST that normal functions can't have.

Like you could have this:

function bit $initstate();

easily enough, but if your special tool defined a function akin to $bits or $typename, what would you write in that file?

function ??? $bits(???);

[abradd]

I see your point.

Perhaps a more generic solution like a filter based on a regexp of the error/warning message would be workable.

The error/warning category and the name of the offending symbol is provided in the message:

tb/formal.v:89:14: error: unknown system name '$initstate' [-Wunknown-sys-name]
        if (!$initstate && !$past(reset)) begin

So one could declare a filter for any Wunknown-sys-name error that contains "$initstate" and this warning wouldn't be generated. Even the line number could be specified, if desired.

[abradd]

It seems Verilator implements the filtering I described as waivers.

[MikePopoloski]

Yeah, I'm not a big fan of separate lint filtering files because it's easy for them to get out of date with minor modifications of the source; you want the context for the filter to be in the source itself and move with it. Still though, if there is strong demand I could look into adding support for it. Otherwise the pragma approach is the way to go IMO (as a general thing; I could still see adding a separate feature to allow defining additional built-in system functions to handle them more gracefully).