examples/smtbmc/demo8.v

   1 // Simple exists-forall demo
   2
   3 module demo8;
   4         wire [7:0] prime = $anyconst;
   5         wire [3:0] factor = $allconst;
   6
   7         always @* begin
   8                 if (1 < factor && factor < prime)
   9                         assume((prime % factor) != 0);
  10                 assume(prime > 1);
  11         end
  12 endmodule