daily pastebin goal
63%
SHARE
TWEET

Untitled

a guest Oct 13th, 2017 57 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
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top