Cannot read verilog code with property statements in yosys after sv2v

[mmxsrup]

I am trying to convert a property statement using the seqprop branch . I would like to read the converted code with yosys, but I get an error. Can you tell me where the problem is? The associated issue is https://github.com/zachjs/sv2v/issues/214.

1. Convert test.sv to verilog code using command: sv2v -E Assert test.sv.
2. Error when reading test.v in Yosys.

   
   yosys> read_verilog -sv test.v  

3. Executing Verilog-2005 frontend: test.v Parsing SystemVerilog input from `test.v' to AST representation. test.v:3: ERROR: syntax error, unexpected TOK_PROPERTY

test.sv:

module test(
    input logic clock
);
    property p1;
        @(posedge clock) 1 |-> 1;
        endproperty
endmodule

test.v:

module test (clock);
    input wire clock;
    property p1;
        @(posedge clock) 
            (1 |-> 1)
    endproperty
endmodule

The experimental environment is as follows.

$sv2v --version
sv2v v0.0.9-40-ge1d9117

$yosys --version
Yosys 0.20+11 (git sha1 51f67e55f, clang 10.0.0-4ubuntu1 -fPIC -Os)

[yodalee]

With my latest yosys

$ yosys -version
Yosys 0.20+22 (git sha1 556d008ed, gcc 12.1.1 -march=x86-64 -mtune=generic -O2 -fstack-protector-strong -fno-plt -fPIC -Os)

The error message is improved:

$ yosys> read_verilog test.v

1. Executing Verilog-2005 frontend: test.v
Parsing Verilog input from `test.v' to AST representation.
Lexer warning: The SystemVerilog keyword `property' (at test.v:3) is not recognized unless read_verilog is called with -sv!
test.v:3: ERROR: syntax error, unexpected ';', expecting '(' or '['

It seems that property is not valid token in verilog. Maybe sv2v should remove the token.

[zachjs]

I'm guessing you're using the branch from #214 if you are successfully running these inputs through sv2v.

If you are not intending to use the assertions downstream, please try not passing -E assert to sv2v, as this will cause sv2v to drop the SystemVerilog assertions in the output.

On @mmxsrup's input, simply running sv2v without -E assert, I get:

module test (clock);
    input wire clock;
endmodule

[mmxsrup]

@zachjs Thanks for the reply.

I'm guessing you're using the branch from https://github.com/zachjs/sv2v/issues/214

Yes, I used seqprop branch.

If you are not intending to use the assertions downstream, please try not passing -E assert to sv2v, as this will cause sv2v to drop the SystemVerilog assertions in the output.

I understand this. However, I want to include assert expressions in the verilog code generated by yosys write_verilog. So I want to successfully convert my code using t -E assert option. More specifically, I would like to use sv2v to read the Cores-SweRV code with assert enabled into yosys.

[zachjs]

@mmxsrup sv2v focusses on converting synthesizable language constructs. As such, certain high-level assertions cannot currently be parsed, let alone converted into Yosys-compatible SystemVerilog. Can you help me understand the rest of your flow? Right now, it sounds like: sv2v -> Yosys read_verilog -> Yosys write_verilog -> ???.

[zachjs]

@mmxsrup @yodalee I'm still very interested in better understanding your flow so that it can be supported by sv2v. Please let me know what you think!