Jonathan Certes

Research and teaching in information system security

Home Research Resources Teaching

Home / Research / Extension for LTL_Coq library

Abstract

This tool extends the work An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs; technical insights are provided here. It is a Coq library which aims at easing manual demonstration of theorems related to PSL properties. This includes definitions to extend the LTL_coq library: definitions of PSL extended next operators and definitions of bit vectors. Also, this includes theorems to compare bit vectors similarly to if they were integer numbers. It provides lemmas that are useful to prove complex theorems.

Source code of the library, along with a program to convert PSL properties expressed with SMV, is available here . In this webpage, we list some available features.

Prerequisites

The source code of the library is written in Gallina: specification language for Coq.

In order to work properly, the following command must be available:

Debian package coq provides coqc. Also, library LTL_Coq must be available. It can be downloaded here

Description

Program psl2coq is program written in Python that converts PSL properties expressed with SMV. It creates a Coq syntax file from a SMV module where all properties from PSLSPEC, LTLSPEC and INVARSPEC are converted to coq Axioms.

The output Coq file uses operators which semantics are described in library LTL_Coq. It also uses operators which semantics are described in the associated library.

Here are some definitions and notations regarding bit vectors that are provided by this associated library:

(* definition of a bit: *)
Inductive Bit : Set :=
  | Z : Bit   (* zero *)
  | O : Bit.  (* one  *)

(* definition of a bit vector: *)
Inductive BitVect : nat -> Set :=
  | bnil  : BitVect 0
  | bcons : forall (n : nat), Bit -> BitVect n -> BitVect (S n).

(* comparison lower or equal between two bit vectors of the same size: *)
Definition le_BitVector {size : nat} (v1 v2 : BitVect size) : (* ... *).
Notation "a '<= b" := (le_BitVector a b) (at level 100).

(* equality between two bit vectors of the same size: *)
Definition eq_BitVector {size : nat} (v1 v2 : BitVect size) : (* ... *).
Notation "a '== b" := (eq_BitVector a b) (at level 100).

(* Selection of a range in a BitVector with implicit size: *)
Definition range_BitVector {size : nat} (v : BitVect size) (from to : nat) := (* ... *).

(* Transforms a natural number into a bit vector of a given size: *)
Fixpoint nat2vect (size : nat) (value : nat) : BitVect size := (* ... *).

Here are some definitions and notations regarding PSL operators that are provided by this associated library:

(* implication between two PathF: *)
Infix "-->" := impP (at level 20).

(* Definition of PSL expression "next_event_a(b)[i:i](f)": *)
Fixpoint next_event (b: PathF) (i: nat) (f: PathF) := (* ... *).

(* Definition of PSL expression "next_event_a(b)[i:j](f)": *)
Fixpoint next_event_a (b: PathF) (i j: nat) (f: PathF) := (* ... *).

Finally, the library comes with a toolbox where useful theorems are proven. Here are some examples:

Theorem eventually_next:
  ∀ π : Path,
    ∀ P₀ : PathF,
      ( π ⊨ F(P₀) ) <-> ( π ⊨ P₀ ∨ (X (F(P₀))) ).

Theorem globally_next:
  ∀ π : Path,
    ∀ P₀ : PathF,
      ( π ⊨ G(P₀) ) <-> ( π ⊨ P₀ ∧ (X (G(P₀))) ).

Theorem globally_impP_x2:
  ∀ π : Path,
    ∀ A₀ A₁ A₂ P₁ P₂ : PathF,
      (π ⊨ G (A₀ ∧ A₁ --> P₁)) /\ (π ⊨ G (A₀ ∧ A₂ --> P₂))
    ->
      (π ⊨ G (A₀ ∧ A₁ ∧ A₂ --> (P₁ ∧ P₂))).

Theorem globally_impP_x2_to_disj:
  ∀ π : Path,
    ∀ A₀ A₁ A₂ P₁ P₂ : PathF,
      π ⊨ G(A₀ ∧ A₁ --> P₁) /\ π ⊨ G(A₀ ∧ A₂ --> P₂)
    ->
      π ⊨ G(A₀ ∧ (A₁ ∨ A₂) --> (P₁ ∨ P₂)).

Theorem eq_vect_tran:
  ∀ size : nat,
    ∀ V₀ V₁ V₂ : BitVect size,
      ∀ π : Path,
        ∀ s : State,
          path_up π s ⊨ (V₀ '== V₁) /\ path_up π s ⊨ (V₁ '== V₂)
        ->
          path_up π s ⊨ (V₀ '== V₂).

Theorem data_size_update:
  ∀ size i j : nat,
       (i < j)
    /\ (j < 2^size)
  ->
    ∀ π : Path,
    ∀ ф₀ ф₁ ф₂ ф₃ : PathF,
    ∀ bv : BitVect size,
      π ⊨ G( ф₀ ∧ X(ф₁ ∧ (next_event (('clk) ∧ ('ready)) 1 (uwconst(i, size) '<= bv)) ∧ ф₂) --> ф₃ )
    ->
      π ⊨ G( ф₀ ∧ X(ф₁ ∧ (next_event (('clk) ∧ ('ready)) 1 (uwconst(j, size) '<= bv)) ∧ ф₂) --> ф₃ ).

Complete examples that uses this library are available here and here . Just run make to compile and run the proof with coqc. One of these examples illustrates the manual proof of the theorem described in publication An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs. This theorem demonstrates that verifying 7 local properties implies a verification of the specification.

Recorded presentation

Associated publications


no cookie, no javascript, no external resource, KISS!