diff --git a/bin/verilator b/bin/verilator index 40da3e063..27c0df5de 100755 --- a/bin/verilator +++ b/bin/verilator @@ -1711,8 +1711,8 @@ assertion clocks. =head2 Synthesis Directive Assertion Support With the --assert switch, Verilator reads any "//synopsys full_case" or "// -synopsys parallel_case" directives. The same applies to any "//cadence" or -"// ambit synthesis" directives of the same form. +synopsys parallel_case" directives. The same applies to any "// ambit +synthesis", "//cadence" or "//pragma" directives of the same form. When these synthesis directives are discovered, Verilator will either formally prove the directive to be true, or failing that, will insert the diff --git a/src/V3PreProc.cpp b/src/V3PreProc.cpp index ef333fc6d..b11695f2c 100644 --- a/src/V3PreProc.cpp +++ b/src/V3PreProc.cpp @@ -393,6 +393,9 @@ void V3PreProcImp::comment(const string& text) { } else if (0==(strncmp(cp,"cadence",strlen("cadence")))) { cp+=strlen("cadence"); synth = true; + } else if (0==(strncmp(cp,"pragma",strlen("pragma")))) { + cp+=strlen("pragma"); + synth = true; } else if (0==(strncmp(cp,"ambit synthesis",strlen("ambit synthesis")))) { cp+=strlen("ambit synthesis"); synth = true;