From c368dd6867fc14463a0f35672a5a7f38693474ed Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 19 Jul 2017 14:11:30 +0200 Subject: Adds "real" property: Find combinational processes --- data/property/combinational_processes.pro | 37 +++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 data/property/combinational_processes.pro (limited to 'data/property/combinational_processes.pro') diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro new file mode 100644 index 0000000..9300672 --- /dev/null +++ b/data/property/combinational_processes.pro @@ -0,0 +1,37 @@ +(tag_existing + ( + (ps process STRUCT_COMBINATIONAL_PROCESS) + ) + (forall sl1 signal + (and + (CTL_verifies ps + (implies + (EF (expr_writes sl1)) + (AF (expr_writes sl1)) + ) + ) + (implies + (exists target signal + (CTL_verifies ps + (EF + (and + (expr_reads sl1) + (not + (and + (expr_writes target) + (AX + (AF + (expr_writes target) + ) + ) + ) + ) + ) + ) + ) + ) + (is_in_sensitivity_list ps sl1) + ) + ) + ) +) -- cgit v1.2.3-70-g09d2