mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 11:42:30 +00:00
83dd99efb7
This option allows you to process a design that includes unsupported SVA. Unsupported SVA gets imported as formal cells using 'x inputs and with the `unsupported_sva` attribute set. This allows you to get a complete list of defined properties or to check only a supported subset of properties. To ensure no properties are unintentionally skipped for actual verification, even in cases where `-sva-continue-on-error` is used by default to read and inspect a design, `hierarchy -simcheck` and `hierarchy -smtcheck` (run by SBY) now ensure that no `unsupported_sva` property cells remain in the design.
9 lines
244 B
Text
9 lines
244 B
Text
|
|
verific -sv <<EOF
|
|
module top(input clk, input a, input b);
|
|
prop_unsupported: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a);
|
|
endmodule;
|
|
EOF
|
|
|
|
logger -expect error "Mixed clocking is currently not supported" 1
|
|
verific -import top
|