tests/various/chparam.sh

   1 #!/bin/bash
   2
   3 trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR
   4
   5 cat > chparam1.sv << "EOT"
   6 module top #(
   7         parameter [31:0] X = 0
   8 ) (
   9         input [31:0] din,
  10         output [31:0] dout
  11 );
  12         assign dout = X-din;
  13 endmodule
  14
  15 module top_props #(
  16         parameter [31:0] X = 0
  17 ) (
  18         input [31:0] dout
  19 );
  20         always @* assert (dout != X);
  21 endmodule
  22
  23 bind top top_props #(.X(123456789)) props (.*);
  24 EOT
  25
  26 cat > chparam2.sv << "EOT"
  27 module top #(
  28         parameter [31:0] X = 0
  29 ) (
  30         input [31:0] din,
  31         output [31:0] dout
  32 );
  33         assign dout = X-din;
  34         always @* assert (dout != 123456789);
  35 endmodule
  36 EOT
  37
  38 if ../../yosys -q -p 'verific -sv chparam1.sv'; then
  39         ../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
  40                         -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
  41                         -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
  42
  43         ../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
  44                         -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
  45                         -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
  46 fi
  47 ../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
  48                 -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
  49                 -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
  50
  51 rm chparam1.sv
  52 rm chparam2.sv