Generation of test sequences for accelerating assertions
type: Dataset
description: With the increasing complexity of SoC, the verification process becomes a task more crucial at all levels of the design cycle, and monopolize a large share of development time. In this context, the assertion-based verification (ABV) has gained considerable popularity in recent years. This is to specify the behavior of the system through logico-temporal properties and check these properties by semiformal or formal methods. Specification languages such as PSL or SVA (IEEE) are commonly used to express these properties. Static verification techniques (model checking) or dynamic (during simulation) can be implemented. We are placed in the context of dynamic verification. Our assertions are expressed in PSL or SVA, and synthesizable descriptions VHDL or Verilog hardware surveillance monitors can be produced (Horus tool). These components can be used for design (simulation and/or emulation for circuit debug and validation) or as embedded components for monitoring the behavior of critical systems. For analysis in the design phase, either in simulation or emulation, the problem of generating test sequences arises. In effect, sequences of randomly generated test can lead to a low coverage conditions of activation monitors and, therefore, may be indicative of little satisfaction assertions. The methods of generation of test sequences under constraints do not provide real solution because the constraints can not be linked to temporal conditions. New methods must be specified and implemented, this's what we propose to study in this thesis.
identifier: NNT: 2012GRENT065
issued: 2026-05-10T04:48:10.635728
language: fr
modified: 2026-05-10T04:48:10.635732
contact point: Organization
  fn: CCSD
keyword: assertion-based-verification
keyword: formal-verification
keyword: infoeu-reposemanticsdoctoralthesis
keyword: spiotherengineering-sciences-physicsother
keyword: theses
keyword: verification-a-base-dassertions
keyword: verification-formelle
landing page: https://theses.hal.science/tel-00838669

Generation of test sequences for accelerating assertions
type: Distribution
format: HTML
issued: 2026-05-10T04:48:10.638959
modified: 2026-05-10T04:48:10.625001
access URL: https://theses.hal.science/tel-00838669

test_moissonnage_selune
type: Agent