Interface and modport support bug ? #5366
Description
Version
Yosys 0.57+148 (git sha1 259bd6f, g++ 15.2.1 -march=x86-64 -mtune=generic -O2 -fno-plt -fexceptions -fstack-clash-protection -fcf-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -flto=auto -fPIC -O3)
On which OS did this happen?
Linux
Reproduction Steps
read_verilog -sv << EOF
interface simple_if;
logic data;
modport driver(output data);
modport receiver(input data);
endinterface
module driver_mod(simple_if.driver intf, input logic in);
assign intf.data = in;
endmodule
module receiver_mod(simple_if.receiver intf, output logic out);
assign out = intf.data;
endmodule
module simple_interface_mod(
input logic [1:0] inputs,
output logic [1:0] outputs
);
simple_if intf0();
simple_if intf1();
driver_mod d0(intf0, inputs[0]);
driver_mod d1(intf1, inputs[1]);
receiver_mod r0(intf0, outputs[0]);
receiver_mod r1(intf1, outputs[1]);
endmodule
EOF
prep -top simple_interface_modThen I run yosys -q test.ys And it says that there are problems with the interface and the modports... (On the documentation it says that interfaces and modports are supported so I am posting this issue here.
If this is not supported then this is the only problem of this issue.
If this is supposed to be supported then when I also write_cxxrtl test.cc and simulate it I have a problem as it is not outputing the right result.
Here is a yosys script that fails to prove the result
read_verilog -sv << EOF
interface simple_if;
logic data;
modport driver(output data);
modport receiver(input data);
endinterface
module driver_mod(simple_if.driver intf, input logic in);
assign intf.data = in;
endmodule
module receiver_mod(simple_if.receiver intf, output logic out);
assign out = intf.data;
endmodule
module simple_interface_test;
logic [1:0] inputs;
logic [1:0] outputs;
assign inputs = 2'b10; // inputs[1]=1, inputs[0]=0
simple_if intf0();
simple_if intf1();
driver_mod d0(intf0, inputs[0]);
driver_mod d1(intf1, inputs[1]);
receiver_mod r0(intf0, outputs[0]);
receiver_mod r1(intf1, outputs[1]);
always_comb assert(outputs[0] == 1'b0); // inputs[0] = 0, so outputs[0] should be 0
always_comb assert(outputs[1] == 1'b1); // inputs[1] = 1, so outputs[1] should be 1
always_comb assert(outputs == 2'b10); // Overall: outputs should equal inputs (2'b10)
endmodule
EOF
write_cxxrtl simple_interface_test.cc
prep -top simple_interface_test
write_verilog -noattr simple_interface_test-prepped.sv
chformal -lower
select simple_interface_test
sat -prove-asserts -verifyIf we replace the read_verilog -sv by read_slang then the proof works.
If you want I can also provide the testbench that I use with cxxrtl. When using slang this simulates correctly but not when I use yosys' frontend.
Expected Behavior
I would have expected not to have a warning or to simulate the correct result, or for the documentation to specify the partial support of interfaces
Actual Behavior
- Warnings
- Failure to prove the result
- Simulation error when using cxxrtl
Thanks for the work on yosys