From 512f93f8663dc438c2afa35872fa3b39b87e5323 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 14 Oct 2016 15:39:33 +0200 Subject: [PATCH] Added notes about some formal features to README --- README | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/README b/README index 32e9ba24a..8e43d4446 100644 --- a/README +++ b/README @@ -374,6 +374,27 @@ Verilog Attributes and non-standard features and constant values). The intended use for this is synthesis-time DRC. +Non-standard or SystemVerilog features for formal verification +============================================================== + +- Support for "assert", "assume", and "restrict" is enabled when + read_verilog is called with -formal. + +- The system task $initstate evaluates to 1 in the initial state and + to 0 otherwise. + +- The system task $anyconst evaluates to any constant value. + +- The system task $anyseq evaluates to any value, possibly a different + value in each cycle. + +- The SystemVerilog tasks $past, $stable, $rose and $fell are supported + in any clocked block. + +- The syntax @($global_clock) can be used to create FFs that have no + explicit clock input ($ff cells). + + Supported features from SystemVerilog ===================================== @@ -384,8 +405,8 @@ from SystemVerilog: form. In module context: "assert property ();" and within an always block: "assert();". It is transformed to a $assert cell. -- The "assume" statements from SystemVerilog are also supported. The same - limitations as with the "assert" statement apply. +- The "assume" and "restrict" statements from SystemVerilog are also + supported. The same limitations as with the "assert" statement apply. - The keywords "always_comb", "always_ff" and "always_latch", "logic" and "bit" are supported. -- 2.30.2