Skip to content

Commit f77b914

Browse files
kroeningkroening
authored
Merge pull request #428 from diffblue/sva-cover
SystemVerilog: `cover property`
2 parents 73938ed + 4785f3c commit f77b914

10 files changed

+154
-124
lines changed

‎regression/verilog/SVA/cover1.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
cover1.sv
3+
--bound 10
4+
^\[main\.property\.p0\] cover main\.counter == 1: REFUTED$
5+
^\[main\.property\.p1\] cover main\.counter == 100: REFUTED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
Back-end support is missing.

‎regression/verilog/SVA/cover1.sv

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
module main(input clk);
2+
3+
// count up from 0 to 10
4+
reg [7:0] counter;
5+
6+
initial counter = 0;
7+
8+
always @(posedge clk)
9+
if(counter == 10)
10+
counter = 0;
11+
else
12+
counter = counter + 1;
13+
14+
// expected to pass
15+
p0: cover property (counter == 1);
16+
17+
// expected to fail
18+
p1: cover property (counter == 100);
19+
20+
endmodule

‎src/hw_cbmc_irep_ids.h

+1
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ IREP_ID_ONE(sva_sequence_throughout)
1616
IREP_ID_ONE(sva_sequence_concatenation)
1717
IREP_ID_ONE(sva_sequence_first_match)
1818
IREP_ID_ONE(sva_always)
19+
IREP_ID_ONE(sva_cover)
1920
IREP_ID_ONE(sva_nexttime)
2021
IREP_ID_ONE(sva_s_nexttime)
2122
IREP_ID_ONE(sva_eventually)

‎src/verilog/expr2verilog.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -1088,6 +1088,9 @@ std::string expr2verilogt::convert(
10881088
else if(src.id()==ID_sva_always)
10891089
return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
10901090

1091+
else if(src.id() == ID_sva_cover)
1092+
return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
1093+
10911094
else if(src.id()==ID_sva_nexttime)
10921095
return precedence = 0,
10931096
convert_sva("nexttime", to_sva_nexttime_expr(src).op());

‎src/verilog/sva_expr.h

+23
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,29 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
170170
return static_cast<sva_always_exprt &>(expr);
171171
}
172172

173+
class sva_cover_exprt : public unary_predicate_exprt
174+
{
175+
public:
176+
explicit sva_cover_exprt(exprt op)
177+
: unary_predicate_exprt(ID_sva_cover, std::move(op))
178+
{
179+
}
180+
};
181+
182+
static inline const sva_cover_exprt &to_sva_cover_expr(const exprt &expr)
183+
{
184+
PRECONDITION(expr.id() == ID_sva_cover);
185+
sva_cover_exprt::check(expr, validation_modet::INVARIANT);
186+
return static_cast<const sva_cover_exprt &>(expr);
187+
}
188+
189+
static inline sva_cover_exprt &to_sva_cover_expr(exprt &expr)
190+
{
191+
PRECONDITION(expr.id() == ID_sva_cover);
192+
sva_cover_exprt::check(expr, validation_modet::INVARIANT);
193+
return static_cast<sva_cover_exprt &>(expr);
194+
}
195+
173196
class sva_until_exprt : public binary_predicate_exprt
174197
{
175198
public:

‎src/verilog/verilog_expr.h

+29-53
Original file line numberDiff line numberDiff line change
@@ -1603,14 +1603,19 @@ inline verilog_non_blocking_assignt &to_verilog_non_blocking_assign(exprt &expr)
16031603
return static_cast<verilog_non_blocking_assignt &>(expr);
16041604
}
16051605

1606-
/// Verilog concurrent assertion module item
1607-
class verilog_assert_module_itemt : public verilog_module_itemt
1606+
/// Verilog assert/assume/cover property module item
1607+
class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt
16081608
{
16091609
public:
1610-
verilog_assert_module_itemt()
1611-
: verilog_module_itemt(ID_verilog_assert_property)
1610+
verilog_assert_assume_cover_module_itemt(
1611+
irep_idt __id,
1612+
exprt __condition,
1613+
verilog_statementt __action)
1614+
: verilog_module_itemt(__id)
16121615
{
16131616
operands().resize(2);
1617+
condition() = std::move(__condition);
1618+
action() = std::move(__action);
16141619
}
16151620

16161621
inline exprt &condition()
@@ -1623,51 +1628,14 @@ class verilog_assert_module_itemt : public verilog_module_itemt
16231628
return op0();
16241629
}
16251630

1626-
const irep_idt &identifier() const
1631+
inline exprt &action()
16271632
{
1628-
return get(ID_identifier);
1629-
}
1630-
1631-
void identifier(irep_idt __identifier)
1632-
{
1633-
set(ID_identifier, __identifier);
1634-
}
1635-
};
1636-
1637-
inline const verilog_assert_module_itemt &
1638-
to_verilog_assert_module_item(const verilog_module_itemt &module_item)
1639-
{
1640-
PRECONDITION(module_item.id() == ID_verilog_assert_property);
1641-
binary_exprt::check(module_item);
1642-
return static_cast<const verilog_assert_module_itemt &>(module_item);
1643-
}
1644-
1645-
inline verilog_assert_module_itemt &
1646-
to_verilog_assert_module_item(verilog_module_itemt &module_item)
1647-
{
1648-
PRECONDITION(module_item.id() == ID_verilog_assert_property);
1649-
binary_exprt::check(module_item);
1650-
return static_cast<verilog_assert_module_itemt &>(module_item);
1651-
}
1652-
1653-
/// Verilog concurrent assumption module item
1654-
class verilog_assume_module_itemt : public verilog_module_itemt
1655-
{
1656-
public:
1657-
verilog_assume_module_itemt()
1658-
: verilog_module_itemt(ID_verilog_assume_property)
1659-
{
1660-
operands().resize(2);
1661-
}
1662-
1663-
inline exprt &condition()
1664-
{
1665-
return op0();
1633+
return op1();
16661634
}
16671635

1668-
inline const exprt &condition() const
1636+
inline const exprt &action() const
16691637
{
1670-
return op0();
1638+
return op1();
16711639
}
16721640

16731641
const irep_idt &identifier() const
@@ -1681,20 +1649,28 @@ class verilog_assume_module_itemt : public verilog_module_itemt
16811649
}
16821650
};
16831651

1684-
inline const verilog_assume_module_itemt &
1685-
to_verilog_assume_module_item(const verilog_module_itemt &module_item)
1652+
inline const verilog_assert_assume_cover_module_itemt &
1653+
to_verilog_assert_assume_cover_module_item(
1654+
const verilog_module_itemt &module_item)
16861655
{
1687-
PRECONDITION(module_item.id() == ID_verilog_assume_property);
1656+
PRECONDITION(
1657+
module_item.id() == ID_verilog_assert_property ||
1658+
module_item.id() == ID_verilog_assume_property ||
1659+
module_item.id() == ID_verilog_cover_property);
16881660
binary_exprt::check(module_item);
1689-
return static_cast<const verilog_assume_module_itemt &>(module_item);
1661+
return static_cast<const verilog_assert_assume_cover_module_itemt &>(
1662+
module_item);
16901663
}
16911664

1692-
inline verilog_assume_module_itemt &
1693-
to_verilog_assume_module_item(verilog_module_itemt &module_item)
1665+
inline verilog_assert_assume_cover_module_itemt &
1666+
to_verilog_assert_assume_cover_module_item(verilog_module_itemt &module_item)
16941667
{
1695-
PRECONDITION(module_item.id() == ID_verilog_assume_property);
1668+
PRECONDITION(
1669+
module_item.id() == ID_verilog_assert_property ||
1670+
module_item.id() == ID_verilog_assume_property ||
1671+
module_item.id() == ID_verilog_cover_property);
16961672
binary_exprt::check(module_item);
1697-
return static_cast<verilog_assume_module_itemt &>(module_item);
1673+
return static_cast<verilog_assert_assume_cover_module_itemt &>(module_item);
16981674
}
16991675

17001676
// Can be one of three:

‎src/verilog/verilog_synthesis.cpp

+25-9
Original file line numberDiff line numberDiff line change
@@ -1838,8 +1838,8 @@ Function: verilog_synthesist::synth_assert
18381838
18391839
\*******************************************************************/
18401840

1841-
void verilog_synthesist::synth_assert(
1842-
const verilog_assert_module_itemt &module_item)
1841+
void verilog_synthesist::synth_assert_cover(
1842+
const verilog_assert_assume_cover_module_itemt &module_item)
18431843
{
18441844
const irep_idt &identifier = module_item.identifier();
18451845
symbolt &symbol=symbol_table_lookup(identifier);
@@ -1848,9 +1848,19 @@ void verilog_synthesist::synth_assert(
18481848

18491849
auto cond = synth_expr(module_item.condition(), symbol_statet::SYMBOL);
18501850

1851-
// concurrent assertions come with an implicit 'always'
1852-
if(cond.id() != ID_sva_always)
1853-
cond = sva_always_exprt(cond);
1851+
if(module_item.id() == ID_verilog_assert_property)
1852+
{
1853+
// Concurrent assertions come with an implicit 'always'.
1854+
if(cond.id() != ID_sva_always)
1855+
cond = sva_always_exprt(cond);
1856+
}
1857+
else if(module_item.id() == ID_verilog_cover_property)
1858+
{
1859+
// 'cover' requirements are existential.
1860+
cond = sva_cover_exprt(cond);
1861+
}
1862+
else
1863+
PRECONDITION(false);
18541864

18551865
symbol.value = std::move(cond);
18561866
}
@@ -1891,7 +1901,7 @@ Function: verilog_synthesist::synth_assume
18911901
\*******************************************************************/
18921902

18931903
void verilog_synthesist::synth_assume(
1894-
const verilog_assume_module_itemt &module_item)
1904+
const verilog_assert_assume_cover_module_itemt &module_item)
18951905
{
18961906
auto condition = synth_expr(to_binary_expr(module_item).op0(), symbol_statet::SYMBOL);
18971907

@@ -2688,10 +2698,16 @@ void verilog_synthesist::synth_module_item(
26882698
synth_module_item(block_item, trans);
26892699
}
26902700
}
2691-
else if(module_item.id() == ID_verilog_assert_property)
2692-
synth_assert(to_verilog_assert_module_item(module_item));
2701+
else if(
2702+
module_item.id() == ID_verilog_assert_property ||
2703+
module_item.id() == ID_verilog_cover_property)
2704+
{
2705+
synth_assert_cover(to_verilog_assert_assume_cover_module_item(module_item));
2706+
}
26932707
else if(module_item.id() == ID_verilog_assume_property)
2694-
synth_assume(to_verilog_assume_module_item(module_item));
2708+
{
2709+
synth_assume(to_verilog_assert_assume_cover_module_item(module_item));
2710+
}
26952711
else if(module_item.id()==ID_task)
26962712
{
26972713
// ignore for now

‎src/verilog/verilog_synthesis_class.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -220,8 +220,8 @@ class verilog_synthesist:
220220
void synth_module_item(const verilog_module_itemt &, transt &);
221221
void synth_always_base(const verilog_always_baset &);
222222
void synth_initial(const verilog_initialt &);
223-
void synth_assert(const verilog_assert_module_itemt &);
224-
void synth_assume(const verilog_assume_module_itemt &);
223+
void synth_assert_cover(const verilog_assert_assume_cover_module_itemt &);
224+
void synth_assume(const verilog_assert_assume_cover_module_itemt &);
225225
void synth_continuous_assign(const verilog_continuous_assignt &);
226226
void synth_force_rec(exprt &lhs, exprt &rhs, transt &);
227227
void synth_module_instance(const verilog_instt &, transt &);

0 commit comments

Comments
 (0)