tests/various/submod.ys

   1 read_verilog <<EOT
   2 module top(input a, output b);
   3 wire c;
   4 (* submod="bar" *) sub s1(a, c);
   5 assign b = c;
   6 endmodule
   7
   8 module sub(input a, output c);
   9 assign c = a;
  10 endmodule
  11 EOT
  12
  13 hierarchy -top top
  14 proc
  15 design -save gold
  16
  17 submod
  18 check -assert
  19 design -stash gate
  20
  21 design -import gold -as gold
  22 design -import gate -as gate
  23
  24 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  25 sat -verify -prove-asserts -show-ports miter
  26
  27
  28 design -reset
  29 read_verilog <<EOT
  30 module top(input a, output [1:0] b);
  31 (* submod="bar" *) sub s1(a, b[1]);
  32 assign b[0] = 1'b0;
  33 endmodule
  34
  35 module sub(input a, output c);
  36 assign c = a;
  37 endmodule
  38 EOT
  39
  40 hierarchy -top top
  41 proc
  42 design -save gold
  43
  44 submod
  45 check -assert top
  46 design -stash gate
  47
  48 design -import gold -as gold
  49 design -import gate -as gate
  50
  51 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  52 sat -verify -prove-asserts -show-ports miter
  53
  54
  55 design -reset
  56 read_verilog <<EOT
  57 module top(input a, output [1:0] b, c);
  58 (* submod="bar" *) sub s1(a, b[0]);
  59 (* submod="bar" *) sub s2(a, c[1]);
  60 assign c = b;
  61 endmodule
  62
  63 module sub(input a, output c);
  64 assign c = a;
  65 endmodule
  66 EOT
  67
  68 hierarchy -top top
  69 proc
  70 design -save gold
  71
  72 submod
  73 check -assert top
  74 design -stash gate
  75
  76 design -import gold -as gold
  77 design -import gate -as gate
  78
  79 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  80 sat -verify -prove-asserts -show-ports miter
  81
  82
  83 design -reset
  84 read_verilog <<EOT
  85 module top(input d, c, (* init = 3'b011 *) output reg [2:0] q);
  86 (* submod="bar" *) DFF s1(.D(d), .C(c), .Q(q[1]));
  87 DFF s2(.D(d), .C(c), .Q(q[0]));
  88 DFF s3(.D(d), .C(c), .Q(q[2]));
  89 endmodule
  90
  91 module DFF(input D, C, output Q);
  92 parameter INIT = 1'b0;
  93 endmodule
  94 EOT
  95
  96 hierarchy -top top
  97 proc
  98
  99 submod
 100 dffinit -ff DFF Q INIT
 101 check -noinit -assert
 102
 103
 104 design -reset
 105 read_verilog <<EOT
 106 module top(input d, c, output reg [2:0] q);
 107 (* submod="bar" *) DFF s1(.D(d), .C(c), .Q(q[1]));
 108 DFF s2(.D(d), .C(c), .Q(q[0]));
 109 DFF s3(.D(d), .C(c), .Q(q[2]));
 110 endmodule
 111 EOT
 112
 113 hierarchy -top top
 114 proc
 115
 116 submod
 117 flatten
 118
 119 read_verilog <<EOT
 120 module DFF(input D, C, output Q);
 121 endmodule
 122 EOT
 123
 124 check -assert