• API
• FAQ
• Tools
• Archive
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.

Top