2
// Copyright (C) 2008-2014 Centaur Technology
5
// Centaur Technology Formal Verification Group
6
// 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
7
// http://www.centtech.com/
9
// License: (An MIT/X11-style license)
11
// Permission is hereby granted, free of charge, to any person obtaining a
12
// copy of this software and associated documentation files (the "Software"),
13
// to deal in the Software without restriction, including without limitation
14
// the rights to use, copy, modify, merge, publish, distribute, sublicense,
15
// and/or sell copies of the Software, and to permit persons to whom the
16
// Software is furnished to do so, subject to the following conditions:
18
// The above copyright notice and this permission notice shall be included in
19
// all copies or substantial portions of the Software.
21
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
24
// THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
26
// FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
27
// DEALINGS IN THE SOFTWARE.
29
// Original author: Jared Davis <jared@centtech.com>
73
&& (impl_o2 === spec_o2)
74
&& (impl_o3 === spec_o3)
75
&& (impl_o4 === spec_o4)
76
&& (impl_o5 === spec_o5);
82
for(i = 0; i < 'd 1_000_000; i = i + 1)
84
{a, n1, n2} = $random(seed);
88
$display("Failure for %b, %b, %b:", a, n1, n2);
89
if (impl_o1 !== spec_o1) $display("fail o1: impl %b, spec %b", impl_o1, spec_o1);
90
if (impl_o2 !== spec_o2) $display("fail o2: impl %b, spec %b", impl_o2, spec_o2);
91
if (impl_o3 !== spec_o3) $display("fail o3: impl %b, spec %b", impl_o3, spec_o3);
92
if (impl_o4 !== spec_o4) $display("fail o4: impl %b, spec %b", impl_o4, spec_o4);
93
if (impl_o5 !== spec_o5) $display("fail o5: impl %b, spec %b", impl_o5, spec_o5);