data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv
1: b'%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:8: Cannot find include file: prim_assert.sv\n`include "prim_assert.sv" \n         ^~~~~~~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip,data/full_repos/permissive/509468557/prim_assert.sv\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip,data/full_repos/permissive/509468557/prim_assert.sv.v\n             data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip,data/full_repos/permissive/509468557/prim_assert.sv.sv\n             prim_assert.sv\n             prim_assert.sv.v\n             prim_assert.sv.sv\n             obj_dir/prim_assert.sv\n             obj_dir/prim_assert.sv.v\n             obj_dir/prim_assert.sv.sv\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:55: Define or directive not defined: \'`ASSUME_FPV\'\n  `ASSUME_FPV(PingReqDeassert_M,\n  ^~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:55: syntax error, unexpected \'(\'\n  `ASSUME_FPV(PingReqDeassert_M,\n              ^~~~~~~~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:60: Define or directive not defined: \'`ASSUME_FPV\'\n  `ASSUME_FPV(PingReqStaysAsserted0_M,\n  ^~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:66: Define or directive not defined: \'`ASSUME_FPV\'\n  `ASSUME_FPV(PingReqStaysLowFor3Cycles_M,\n  ^~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:67: Unsupported or unknown PLI call: $fell\n      $fell(ping_req_i)\n      ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:75: Define or directive not defined: \'`ASSUME_FPV\'\n  `ASSUME_FPV(FiniteEsc_M,\n  ^~~~~~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:78: Unsupported: SystemVerilog 2009 reserved word not implemented: \'strong\'\n      strong(##[1:$] !esc_req_i [*3]))\n      ^~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:82: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(PingRespCheck_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:83: Unsupported or unknown PLI call: $rose\n      $rose(ping_req_i) &&\n      ^~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:93: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(EscRespCheck_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:103: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(EscCheck_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:112: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(SingleSigIntDetected0_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:117: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(SingleSigIntDetected1_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:124: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(FsmLivenessSender_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:128: Unsupported: SystemVerilog 2009 reserved word not implemented: \'strong\'\n      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_sender.state_q\n      ^~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:131: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(FsmLivenessReceiver_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:135: Unsupported: SystemVerilog 2009 reserved word not implemented: \'strong\'\n      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_receiver.state_q\n      ^~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:143: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(AutoEscalation0_A,\n  ^~~~~~~\n%Error: data/full_repos/permissive/509468557/generators/ibex/src/main/resources/vsrc/ibex/vendor/lowrisc_ip/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv:157: Define or directive not defined: \'`ASSERT\'\n  `ASSERT(AutoEscalation1_A,\n  ^~~~~~~\n%Error: Cannot continue\n'
module prim_esc_rxtx_assert_fpv (
  input        clk_i,
  input        rst_ni,

  input        resp_err_pi,
  input        resp_err_ni,
  input        esc_err_pi,
  input        esc_err_ni,

  input        esc_req_i,
  input        ping_req_i,
  input        ping_ok_o,
  input        integ_fail_o,
  input        esc_en_o
);

  logic error_present;
  assign error_present = resp_err_pi ||
                         resp_err_ni ||
                         esc_err_pi  ||
                         esc_err_ni;


  logic error_d, error_q;
  assign error_d = error_q || error_present;
  always_ff @(posedge clk_i or negedge rst_ni) begin : p_error_reg
    if (!rst_ni) begin
      error_q <= 1'b0;
    end else begin
      error_q <= error_d;
    end
  end


  logic esc_d, esc_q;
  assign esc_d = esc_q || esc_req_i;
  always_ff @(posedge clk_i or negedge rst_ni) begin : p_esc_reg
    if (!rst_ni) begin
      esc_q <= 1'b0;
    end else begin
      esc_q <= esc_d;
    end
  end


  `ASSUME_FPV(PingReqDeassert_M,
      ping_req_i &&
      ping_ok_o
      |=>
      !ping_req_i)
  `ASSUME_FPV(PingReqStaysAsserted0_M,
      ping_req_i &&
      !ping_ok_o
      |=>
      ping_req_i)

  `ASSUME_FPV(PingReqStaysLowFor3Cycles_M,
      $fell(ping_req_i)
      |->
      !ping_req_i [*3])





  `ASSUME_FPV(FiniteEsc_M,
      esc_req_i
      |->
      strong(##[1:$] !esc_req_i [*3]))



  `ASSERT(PingRespCheck_A,
      $rose(ping_req_i) &&
      !esc_req_i
      |->
      ##[0:4] ping_ok_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_req_i)


  `ASSERT(EscRespCheck_A,
      ##1 esc_req_i
      |->
      ##[0:1] prim_esc_rxtx_fpv.esc_rx_out.resp_p
      ##1 !prim_esc_rxtx_fpv.esc_rx_out.resp_p,
      clk_i,
      !rst_ni ||
      error_present)


  `ASSERT(EscCheck_A,
      ##1 esc_req_i
      |->
      ##[0:1] esc_en_o,
      clk_i,
      !rst_ni ||
      error_present)


  `ASSERT(SingleSigIntDetected0_A,
      {esc_err_pi, esc_err_ni} == '0 ##1
      $onehot({resp_err_pi, resp_err_ni})
      |->
      integ_fail_o)
  `ASSERT(SingleSigIntDetected1_A,
      $onehot({esc_err_pi, esc_err_ni}) ##1
      {resp_err_pi, resp_err_ni} == '0
      |->
      integ_fail_o)


  `ASSERT(FsmLivenessSender_A,
      (prim_esc_rxtx_fpv.u_prim_esc_sender.state_q !=
      prim_esc_rxtx_fpv.u_prim_esc_sender.Idle)
      |->
      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_sender.state_q
      == prim_esc_rxtx_fpv.u_prim_esc_sender.Idle)))

  `ASSERT(FsmLivenessReceiver_A,
      (prim_esc_rxtx_fpv.u_prim_esc_receiver.state_q !=
      prim_esc_rxtx_fpv.u_prim_esc_receiver.Idle)
      |->
      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_receiver.state_q
      == prim_esc_rxtx_fpv.u_prim_esc_receiver.Idle)),
      clk_i,
      rst_ni ||
      error_present)



  `ASSERT(AutoEscalation0_A,
      ping_req_i &&
      ping_ok_o &&
      !esc_en_o ##1
      !ping_req_i [*0 : 2**prim_esc_rxtx_fpv.u_prim_esc_receiver.TimeoutCntDw - 4]
      |->
      !esc_en_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_d)



  `ASSERT(AutoEscalation1_A,
      ping_req_i &&
      ping_ok_o &&
      !esc_en_o ##1
      !ping_req_i [* 2**prim_esc_rxtx_fpv.u_prim_esc_receiver.TimeoutCntDw - 3 : $]
      |->
      esc_en_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_d)


endmodule
module prim_esc_rxtx_assert_fpv (
  input        clk_i,
  input        rst_ni,

  input        resp_err_pi,
  input        resp_err_ni,
  input        esc_err_pi,
  input        esc_err_ni,

  input        esc_req_i,
  input        ping_req_i,
  input        ping_ok_o,
  input        integ_fail_o,
  input        esc_en_o
);


  logic error_present;
  assign error_present = resp_err_pi ||
                         resp_err_ni ||
                         esc_err_pi  ||
                         esc_err_ni;


  logic error_d, error_q;
  assign error_d = error_q || error_present;
  always_ff @(posedge clk_i or negedge rst_ni) begin : p_error_reg
    if (!rst_ni) begin
      error_q <= 1'b0;
    end else begin
      error_q <= error_d;
    end
  end


  logic esc_d, esc_q;
  assign esc_d = esc_q || esc_req_i;
  always_ff @(posedge clk_i or negedge rst_ni) begin : p_esc_reg
    if (!rst_ni) begin
      esc_q <= 1'b0;
    end else begin
      esc_q <= esc_d;
    end
  end


  `ASSUME_FPV(PingReqDeassert_M,
      ping_req_i &&
      ping_ok_o
      |=>
      !ping_req_i)
  `ASSUME_FPV(PingReqStaysAsserted0_M,
      ping_req_i &&
      !ping_ok_o
      |=>
      ping_req_i)

  `ASSUME_FPV(PingReqStaysLowFor3Cycles_M,
      $fell(ping_req_i)
      |->
      !ping_req_i [*3])





  `ASSUME_FPV(FiniteEsc_M,
      esc_req_i
      |->
      strong(##[1:$] !esc_req_i [*3]))



  `ASSERT(PingRespCheck_A,
      $rose(ping_req_i) &&
      !esc_req_i
      |->
      ##[0:4] ping_ok_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_req_i)


  `ASSERT(EscRespCheck_A,
      ##1 esc_req_i
      |->
      ##[0:1] prim_esc_rxtx_fpv.esc_rx_out.resp_p
      ##1 !prim_esc_rxtx_fpv.esc_rx_out.resp_p,
      clk_i,
      !rst_ni ||
      error_present)


  `ASSERT(EscCheck_A,
      ##1 esc_req_i
      |->
      ##[0:1] esc_en_o,
      clk_i,
      !rst_ni ||
      error_present)


  `ASSERT(SingleSigIntDetected0_A,
      {esc_err_pi, esc_err_ni} == '0 ##1
      $onehot({resp_err_pi, resp_err_ni})
      |->
      integ_fail_o)
  `ASSERT(SingleSigIntDetected1_A,
      $onehot({esc_err_pi, esc_err_ni}) ##1
      {resp_err_pi, resp_err_ni} == '0
      |->
      integ_fail_o)


  `ASSERT(FsmLivenessSender_A,
      (prim_esc_rxtx_fpv.u_prim_esc_sender.state_q !=
      prim_esc_rxtx_fpv.u_prim_esc_sender.Idle)
      |->
      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_sender.state_q
      == prim_esc_rxtx_fpv.u_prim_esc_sender.Idle)))

  `ASSERT(FsmLivenessReceiver_A,
      (prim_esc_rxtx_fpv.u_prim_esc_receiver.state_q !=
      prim_esc_rxtx_fpv.u_prim_esc_receiver.Idle)
      |->
      strong(##[1:$] (prim_esc_rxtx_fpv.u_prim_esc_receiver.state_q
      == prim_esc_rxtx_fpv.u_prim_esc_receiver.Idle)),
      clk_i,
      rst_ni ||
      error_present)



  `ASSERT(AutoEscalation0_A,
      ping_req_i &&
      ping_ok_o &&
      !esc_en_o ##1
      !ping_req_i [*0 : 2**prim_esc_rxtx_fpv.u_prim_esc_receiver.TimeoutCntDw - 4]
      |->
      !esc_en_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_d)



  `ASSERT(AutoEscalation1_A,
      ping_req_i &&
      ping_ok_o &&
      !esc_en_o ##1
      !ping_req_i [* 2**prim_esc_rxtx_fpv.u_prim_esc_receiver.TimeoutCntDw - 3 : $]
      |->
      esc_en_o,
      clk_i,
      !rst_ni ||
      error_d ||
      esc_d)


endmodule