SHARE
TWEET

Untitled

a guest Oct 13th, 2017 56 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module  twotests(i_clk, i_ce, i_val, o_val);
  2.     input   wire    i_clk, i_ce, i_val;
  3.     output  reg o_val;
  4.  
  5.     initial o_val = 1'b0;
  6.     always @(posedge i_clk)
  7.         if (i_ce)
  8.             o_val <= i_val;
  9.  
  10. `ifdef  FORMAL
  11.   // Set up an assumed clock
  12.     reg prev_i_clk;
  13.  
  14.     initial assume(i_clk == 1'b0);
  15.     initial prev_i_clk  = 1;
  16.     always @($global_clock)
  17.     begin
  18.         prev_i_clk  <= i_clk;
  19.         assume(i_clk != prev_i_clk);
  20.     end
  21.  
  22.     initial assume(i_ce  == 1'b0);
  23.     initial assume(i_val == 1'b0);
  24.  
  25. `ifdef  THIS_FAILS
  26.     // Assert that, either i_ce was true on the last clock, or o_val
  27.     // has remained constant
  28.     always @(posedge i_clk)
  29.         assert(($past(i_ce)) || (o_val == $past(o_val)));
  30.  
  31.     // Assert that either i_ce was false, or (if true) the output
  32.     // value is now equal to the last output value.
  33.     //
  34.     // This assert fails ... why?
  35.     //
  36.     // When it fails, i_ce is a constant 0, so !$past(i_ce) should be true.
  37.     always @(posedge i_clk)
  38.         assert((!$past(i_ce))|| (o_val == $past(i_val)));
  39. `else
  40.  
  41.     reg past_i_ce, past_i_val, past_o_val;
  42.  
  43.     initial past_i_ce  = 1'b0;
  44.     initial past_i_val = 1'b0;
  45.     initial past_o_val = 1'b0;
  46.     always @(posedge i_clk)
  47.     begin
  48.         past_i_ce  <= i_ce;
  49.         past_i_val <= i_val;
  50.         past_o_val <= o_val;
  51.     end
  52.  
  53.     always @(posedge i_clk)
  54.         assert((past_i_ce) || (o_val == past_o_val));
  55.     always @(posedge i_clk)
  56.         assert((!past_i_ce)|| (o_val == past_i_val));
  57.  
  58. `endif // THIS_FAILS
  59.  
  60. `endif // FORMAL
  61. endmodule
RAW Paste Data
Top