Skip to content

Commit a4c1904

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 a4c1904

File tree

15 files changed

+206
-135
lines changed

15 files changed

+206
-135
lines changed

‎regression/ebmc/Output-Register-Passing/main.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,12 @@ module main(in1, in2);
1313

1414
and1 A1 (in1, in2, o1, o2);
1515

16-
assert property1: o1 == (in1 & in2);
16+
always assert property1: o1 == (in1 & in2);
1717
/* A2 is another instance of
1818
ports are referenced to the
1919
declaration by name. */
2020
and1 A2 (.c(o1),.d(o2),.a(o1),.b(in2));
21-
assert property2: o1 == (in1 & in2);
21+
always assert property2: o1 == (in1 & in2);
2222
endmodule
2323

2424
// MODULE DEFINITION

‎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: 17 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1952,32 +1952,34 @@ concurrent_assertion_statement:
19521952
| cover_property_statement
19531953
;
19541954

1955-
assert_property_statement:
1956-
TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block
1957-
{ init($$, ID_assert); mto($$, $4); mto($$, $6); }
1958-
| /* this one is in because SMV does it */
1955+
/* This one mimicks functionality in Cadence SMV */
1956+
smv_assertion_statement:
19591957
TOK_ASSERT property_identifier TOK_COLON expression ';'
1960-
{ init($$, ID_assert); stack_expr($$).operands().resize(2);
1958+
{ init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2);
19611959
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19621960
to_binary_expr(stack_expr($$)).op1().make_nil();
19631961
stack_expr($$).set(ID_identifier, stack_expr($2).id());
19641962
}
1965-
;
1966-
1967-
assume_property_statement:
1968-
TOK_ASSUME TOK_PROPERTY '(' property_expr ')' action_block
1969-
{ init($$, ID_assume); mto($$, $4); mto($$, $6); }
1970-
| /* this one is in because SMV does it */
1971-
TOK_ASSUME property_identifier TOK_COLON expression ';'
1972-
{ init($$, ID_assume); stack_expr($$).operands().resize(2);
1963+
| TOK_ASSUME property_identifier TOK_COLON expression ';'
1964+
{ init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2);
19731965
to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4));
19741966
to_binary_expr(stack_expr($$)).op1().make_nil();
19751967
stack_expr($$).set(ID_identifier, stack_expr($2).id());
19761968
}
19771969
;
19781970

1971+
assert_property_statement:
1972+
TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block
1973+
{ init($$, ID_verilog_assert_property); mto($$, $4); mto($$, $6); }
1974+
;
1975+
1976+
assume_property_statement:
1977+
TOK_ASSUME TOK_PROPERTY '(' property_expr ')' action_block
1978+
{ init($$, ID_verilog_assume_property); mto($$, $4); mto($$, $6); }
1979+
;
1980+
19791981
cover_property_statement: TOK_COVER TOK_PROPERTY '(' expression ')' action_block
1980-
{ init($$, ID_cover); mto($$, $4); mto($$, $6); }
1982+
{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
19811983
;
19821984

19831985
assertion_item_declaration:
@@ -2646,32 +2648,6 @@ par_block:
26462648
addswap($$, ID_base_name, $3); }
26472649
;
26482650

2649-
concurrent_assert_statement:
2650-
assert_property_statement
2651-
| block_identifier TOK_COLON assert_property_statement
2652-
{
2653-
$$=$3;
2654-
stack_expr($$).set(ID_identifier, stack_expr($1).id());
2655-
}
2656-
;
2657-
2658-
concurrent_assume_statement:
2659-
assume_property_statement
2660-
| block_identifier TOK_COLON assume_property_statement
2661-
{
2662-
$$=$3;
2663-
stack_expr($$).set(ID_identifier, stack_expr($1).id());
2664-
}
2665-
;
2666-
2667-
concurrent_cover_statement: cover_property_statement
2668-
| block_identifier TOK_COLON cover_property_statement
2669-
{
2670-
$$=$3;
2671-
stack_expr($$).set(ID_identifier, stack_expr($1).id());
2672-
}
2673-
;
2674-
26752651
// System Verilog standard 1800-2017
26762652
// A.6.4 Statements
26772653

@@ -2894,6 +2870,7 @@ procedural_assertion_statement:
28942870
concurrent_assertion_statement
28952871
| immediate_assertion_statement
28962872
/* | checker_instantiation */
2873+
| smv_assertion_statement
28972874
;
28982875

28992876
immediate_assertion_statement:

‎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)

0 commit comments

Comments
 (0)