Skip to content

Commit 714e447

Browse files
kroeningkroening
committed
SystemVerilog: distinguish assertions
This changes the front-end to distinguish three kinds of assertions/assumptions: 1) concurrent assertions/assumptions ("assert property"), which can be module items or statements, 2) immediate assertion/assumption statements, and 3) SMV-style assertions/assumptions. Front-end and BMC back-end support for initial concurrent assertion statements is added.
1 parent fbfde77 commit 714e447

File tree

14 files changed

+192
-98
lines changed

14 files changed

+192
-98
lines changed

‎regression/verilog/SVA/initial1.desc

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
KNOWNBUG
1+
CORE
22
initial1.sv
33
--module main --bound 1
4-
^EXIT=0$
4+
^\[main\.property\.1\] main\.counter == 0: PROVED up to bound 1$
5+
^\[main\.property\.2\] main\.counter == 100: REFUTED$
6+
^\[main\.property\.3\] ##1 main\.counter == 1: PROVED up to bound 1$
7+
^\[main\.property\.4\] ##1 main\.counter == 100: REFUTED$
8+
^\[main\.property\.5\] s_nexttime main\.counter == 1: FAILURE: property not supported by BMC engine$
9+
^EXIT=10$
510
^SIGNAL=0$
611
--
712
^warning: ignoring
813
--
9-
Syntax is missing for initial label: assert property (...);

‎regression/verilog/SVA/initial1.sv

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,16 @@ module main(input clk);
1414
// expected to pass
1515
initial p0: assert property (counter == 0);
1616

17+
// expected to fail
18+
initial p1: assert property (counter == 100);
19+
20+
// expected to pass
21+
initial p2: assert property (##1 counter == 1);
22+
23+
// expected to fail
24+
initial p2: assert property (##1 counter == 100);
25+
1726
// expected to pass if there are timeframes 0 and 1
18-
initial p1: assert property (s_nexttime counter == 1);
27+
initial p3: assert property (s_nexttime counter == 1);
1928

2029
endmodule

‎regression/verilog/modules/parameters2.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module test(in1, in2);
1010

1111
my_m #( .Ptop(P), .Qtop(Q) ) m_instance(in1, in2, o1, o2);
1212

13-
assert property1: tmp == 4; // should pass
13+
always assert property1: tmp == 4; // should pass
1414

1515
endmodule
1616

@@ -25,6 +25,6 @@ module my_m(a, b, c, d);
2525

2626
wire [3:0] tmp_in_m = Ptop; // tmp1 should be 4 now
2727

28-
assert property2: tmp_in_m == 4; // should pass
28+
always assert property2: tmp_in_m == 4; // should pass
2929

3030
endmodule

‎regression/verilog/tasks/tasks1.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@ module main;
1212
some_task(x, y);
1313
end
1414

15-
assert p1: y==x+1;
15+
always assert p1: y==x+1;
1616

1717
endmodule

‎src/hw-cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \
3535
$(CPROVER_DIR)/solvers/solvers$(LIBEXT) \
3636
$(CPROVER_DIR)/util/util$(LIBEXT) \
3737
$(CPROVER_DIR)/json/json$(LIBEXT) \
38+
../temporal-logic/temporal-logic$(LIBEXT) \
3839
../trans-netlist/trans_trace$(OBJEXT) \
3940
../trans-word-level/trans-word-level$(LIBEXT)
4041

‎src/hw_cbmc_irep_ids.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,11 @@ IREP_ID_ONE(force)
6666
IREP_ID_ONE(deassign)
6767
IREP_ID_ONE(continuous_assign)
6868
IREP_ID_ONE(wait)
69+
IREP_ID_ONE(verilog_assert_property)
70+
IREP_ID_ONE(verilog_assume_property)
71+
IREP_ID_ONE(verilog_cover_property)
72+
IREP_ID_ONE(verilog_smv_assert)
73+
IREP_ID_ONE(verilog_smv_assume)
6974
IREP_ID_ONE(verilog_always)
7075
IREP_ID_ONE(verilog_always_comb)
7176
IREP_ID_ONE(verilog_always_ff)
@@ -76,7 +81,6 @@ IREP_ID_ONE(initial)
7681
IREP_ID_ONE(verilog_label_statement)
7782
IREP_ID_ONE(disable)
7883
IREP_ID_ONE(fork)
79-
IREP_ID_ONE(cover)
8084
IREP_ID_ONE(instance)
8185
IREP_ID_ONE(named_parameter_assignment)
8286
IREP_ID_ONE(parameter_assignment)

‎src/trans-word-level/property.cpp

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/symbol_table.h>
1515

1616
#include <temporal-logic/temporal_expr.h>
17+
#include <temporal-logic/temporal_logic.h>
1718
#include <verilog/sva_expr.h>
1819

1920
#include "instantiate_word_level.h"
@@ -34,8 +35,8 @@ Function: bmc_supports_property
3435

3536
bool bmc_supports_property(const exprt &expr)
3637
{
37-
if(expr.is_constant())
38-
return true;
38+
if(!has_temporal_operator(expr))
39+
return true; // initial state only
3940
else if(expr.id() == ID_AG)
4041
return true;
4142
else if(expr.id() == ID_G)
@@ -68,9 +69,23 @@ void property(
6869
{
6970
messaget message(message_handler);
7071

71-
if(property_expr.is_true())
72+
// Initial state only property?
73+
if(!has_temporal_operator(property_expr))
7274
{
73-
prop_handles.resize(no_timeframes, true_exprt());
75+
for(std::size_t t = 0; t < no_timeframes; t++)
76+
{
77+
exprt prop_handle;
78+
if(t == 0)
79+
{
80+
exprt tmp = instantiate(property_expr, t, no_timeframes, ns);
81+
prop_handle = solver.handle(tmp);
82+
}
83+
else
84+
prop_handle = true_exprt();
85+
86+
prop_handles.push_back(std::move(prop_handle));
87+
}
88+
7489
return;
7590
}
7691

‎src/verilog/parser.y

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1954,10 +1954,10 @@ concurrent_assertion_statement:
19541954

19551955
assert_property_statement:
19561956
TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block
1957-
{ init($$, ID_assert); mto($$, $4); mto($$, $6); }
1957+
{ init($$, ID_verilog_assert_property); mto($$, $4); mto($$, $6); }
19581958
| /* this one is in because SMV does it */
19591959
TOK_ASSERT property_identifier TOK_COLON expression ';'
1960-
{ init($$, ID_assert); stack_expr($$).operands().resize(2);
1960+
{ init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2);
19611961
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19621962
to_binary_expr(stack_expr($$)).op1().make_nil();
19631963
stack_expr($$).set(ID_identifier, stack_expr($2).id());
@@ -1966,18 +1966,18 @@ assert_property_statement:
19661966

19671967
assume_property_statement:
19681968
TOK_ASSUME TOK_PROPERTY '(' property_expr ')' action_block
1969-
{ init($$, ID_assume); mto($$, $4); mto($$, $6); }
1969+
{ init($$, ID_verilog_assume_property); mto($$, $4); mto($$, $6); }
19701970
| /* this one is in because SMV does it */
19711971
TOK_ASSUME property_identifier TOK_COLON expression ';'
1972-
{ init($$, ID_assume); stack_expr($$).operands().resize(2);
1972+
{ init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2);
19731973
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19741974
to_binary_expr(stack_expr($$)).op1().make_nil();
19751975
stack_expr($$).set(ID_identifier, stack_expr($2).id());
19761976
}
19771977
;
19781978

19791979
cover_property_statement: TOK_COVER TOK_PROPERTY '(' expression ')' action_block
1980-
{ init($$, ID_cover); mto($$, $4); mto($$, $6); }
1980+
{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
19811981
;
19821982

19831983
assertion_item_declaration:

‎src/verilog/verilog_elaborate.cpp

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -628,6 +628,17 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
628628
if(statement.id() == ID_assert || statement.id() == ID_assume)
629629
{
630630
}
631+
else if(
632+
statement.id() == ID_verilog_assert_property ||
633+
statement.id() == ID_verilog_assume_property ||
634+
statement.id() == ID_verilog_cover_property)
635+
{
636+
}
637+
else if(
638+
statement.id() == ID_verilog_smv_assert ||
639+
statement.id() == ID_verilog_smv_assume)
640+
{
641+
}
631642
else if(statement.id() == ID_block)
632643
{
633644
// These may be named
@@ -758,7 +769,10 @@ void verilog_typecheckt::collect_symbols(
758769
else if(module_item.id() == ID_continuous_assign)
759770
{
760771
}
761-
else if(module_item.id() == ID_assert || module_item.id() == ID_assume)
772+
else if(
773+
module_item.id() == ID_verilog_assert_property ||
774+
module_item.id() == ID_verilog_assume_property ||
775+
module_item.id() == ID_verilog_cover_property)
762776
{
763777
}
764778
else if(module_item.id() == ID_parameter_override)

‎src/verilog/verilog_expr.h

Lines changed: 34 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1598,11 +1598,12 @@ inline verilog_non_blocking_assignt &to_verilog_non_blocking_assign(exprt &expr)
15981598
return static_cast<verilog_non_blocking_assignt &>(expr);
15991599
}
16001600

1601-
/// Verilog concurrent assertions
1601+
/// Verilog concurrent assertion module item
16021602
class verilog_assert_module_itemt : public verilog_module_itemt
16031603
{
16041604
public:
1605-
verilog_assert_module_itemt() : verilog_module_itemt(ID_assert)
1605+
verilog_assert_module_itemt()
1606+
: verilog_module_itemt(ID_verilog_assert_property)
16061607
{
16071608
operands().resize(2);
16081609
}
@@ -1631,24 +1632,25 @@ class verilog_assert_module_itemt : public verilog_module_itemt
16311632
inline const verilog_assert_module_itemt &
16321633
to_verilog_assert_module_item(const verilog_module_itemt &module_item)
16331634
{
1634-
PRECONDITION(module_item.id() == ID_assert);
1635+
PRECONDITION(module_item.id() == ID_verilog_assert_property);
16351636
binary_exprt::check(module_item);
16361637
return static_cast<const verilog_assert_module_itemt &>(module_item);
16371638
}
16381639

16391640
inline verilog_assert_module_itemt &
16401641
to_verilog_assert_module_item(verilog_module_itemt &module_item)
16411642
{
1642-
PRECONDITION(module_item.id() == ID_assert);
1643+
PRECONDITION(module_item.id() == ID_verilog_assert_property);
16431644
binary_exprt::check(module_item);
16441645
return static_cast<verilog_assert_module_itemt &>(module_item);
16451646
}
16461647

1647-
/// Verilog concurrent assumptions
1648+
/// Verilog concurrent assumption module item
16481649
class verilog_assume_module_itemt : public verilog_module_itemt
16491650
{
16501651
public:
1651-
verilog_assume_module_itemt() : verilog_module_itemt(ID_assume)
1652+
verilog_assume_module_itemt()
1653+
: verilog_module_itemt(ID_verilog_assume_property)
16521654
{
16531655
operands().resize(2);
16541656
}
@@ -1677,20 +1679,23 @@ class verilog_assume_module_itemt : public verilog_module_itemt
16771679
inline const verilog_assume_module_itemt &
16781680
to_verilog_assume_module_item(const verilog_module_itemt &module_item)
16791681
{
1680-
PRECONDITION(module_item.id() == ID_assume);
1682+
PRECONDITION(module_item.id() == ID_verilog_assume_property);
16811683
binary_exprt::check(module_item);
16821684
return static_cast<const verilog_assume_module_itemt &>(module_item);
16831685
}
16841686

16851687
inline verilog_assume_module_itemt &
16861688
to_verilog_assume_module_item(verilog_module_itemt &module_item)
16871689
{
1688-
PRECONDITION(module_item.id() == ID_assume);
1690+
PRECONDITION(module_item.id() == ID_verilog_assume_property);
16891691
binary_exprt::check(module_item);
16901692
return static_cast<verilog_assume_module_itemt &>(module_item);
16911693
}
16921694

1693-
// Intermediate assertion statements, and SMV-style assertions.
1695+
// Can be one of three:
1696+
// 1) Intermediate assertion statement
1697+
// 2) Concurrent assertion statement
1698+
// 3) SMV-style assertion statement
16941699
class verilog_assert_statementt : public verilog_statementt
16951700
{
16961701
public:
@@ -1725,20 +1730,29 @@ class verilog_assert_statementt : public verilog_statementt
17251730
inline const verilog_assert_statementt &
17261731
to_verilog_assert_statement(const verilog_statementt &statement)
17271732
{
1728-
PRECONDITION(statement.id() == ID_assert);
1733+
PRECONDITION(
1734+
statement.id() == ID_assert ||
1735+
statement.id() == ID_verilog_assert_property ||
1736+
statement.id() == ID_verilog_smv_assert);
17291737
binary_exprt::check(statement);
17301738
return static_cast<const verilog_assert_statementt &>(statement);
17311739
}
17321740

17331741
inline verilog_assert_statementt &
17341742
to_verilog_assert_statement(verilog_statementt &statement)
17351743
{
1736-
PRECONDITION(statement.id() == ID_assert);
1744+
PRECONDITION(
1745+
statement.id() == ID_assert ||
1746+
statement.id() == ID_verilog_assert_property ||
1747+
statement.id() == ID_verilog_smv_assert);
17371748
binary_exprt::check(statement);
17381749
return static_cast<verilog_assert_statementt &>(statement);
17391750
}
17401751

1741-
// Intermediate assumption statements, and SMV-style assumptions.
1752+
// Can be one of three:
1753+
// 1) Intermediate assumption statement
1754+
// 2) Concurrent assumption statement
1755+
// 3) SMV-style assumption statement
17421756
class verilog_assume_statementt : public verilog_statementt
17431757
{
17441758
public:
@@ -1773,15 +1787,21 @@ class verilog_assume_statementt : public verilog_statementt
17731787
inline const verilog_assume_statementt &
17741788
to_verilog_assume_statement(const verilog_statementt &statement)
17751789
{
1776-
PRECONDITION(statement.id() == ID_assume);
1790+
PRECONDITION(
1791+
statement.id() == ID_assume ||
1792+
statement.id() == ID_verilog_assume_property ||
1793+
statement.id() == ID_verilog_smv_assume);
17771794
binary_exprt::check(statement);
17781795
return static_cast<const verilog_assume_statementt &>(statement);
17791796
}
17801797

17811798
inline verilog_assume_statementt &
17821799
to_verilog_assume_statement(verilog_statementt &statement)
17831800
{
1784-
PRECONDITION(statement.id() == ID_assume);
1801+
PRECONDITION(
1802+
statement.id() == ID_assume ||
1803+
statement.id() == ID_verilog_assume_property ||
1804+
statement.id() == ID_verilog_smv_assume);
17851805
binary_exprt::check(statement);
17861806
return static_cast<verilog_assume_statementt &>(statement);
17871807
}

0 commit comments

Comments
 (0)