mirror of
https://github.com/lowRISC/ibex.git
synced 2025-04-23 21:39:13 -04:00
55 lines
2 KiB
Text
55 lines
2 KiB
Text
// Copyright lowRISC contributors.
|
|
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
|
// SPDX-License-Identifier: Apache-2.0
|
|
|
|
// LEC dofile for script lec_sv2v.sh. A similar script is used in
|
|
// OpenTitan, any updates or fixes here may need to be reflected in the
|
|
// OpenTitan script as well:
|
|
// https://github.com/lowRISC/opentitan/blob/master/hw/formal/lec_sv2v.do
|
|
|
|
//-------------------------------------------------------------------------
|
|
// read in golden (SystemVerilog) and revised (Verilog)
|
|
//-------------------------------------------------------------------------
|
|
|
|
// map all multi-dimensional ports (including structs) onto 1-dim. ports
|
|
set naming rule -mdportflatten
|
|
|
|
read design -golden -sv09 -f flist_gold -rootonly -root $LEC_TOP
|
|
read design -revised -sys -f flist_rev -rootonly -root $LEC_TOP
|
|
// TODO: instead of using switch -sys (for old SystemVerilog,
|
|
// older than sv2009) we should use -ve (for Verilog). But
|
|
// this currently doesn't work because sv2v doesn't translate
|
|
// .* port connections. Is that an sv2v bug?
|
|
|
|
//-------------------------------------------------------------------------
|
|
// pre-LEC reports
|
|
//-------------------------------------------------------------------------
|
|
report rule check -verbose
|
|
report design data
|
|
report black box
|
|
report module
|
|
|
|
//-------------------------------------------------------------------------
|
|
// compare
|
|
//-------------------------------------------------------------------------
|
|
set system mode lec
|
|
set parallel option -threads 8
|
|
|
|
// map unreachable points
|
|
set mapping method -nets -mem -unreach
|
|
map key points
|
|
report unmapped points
|
|
|
|
add compare point -all
|
|
compare -threads 8 -noneq_stop 1
|
|
analyze abort -compare
|
|
|
|
//-------------------------------------------------------------------------
|
|
// reports
|
|
//-------------------------------------------------------------------------
|
|
report compare data -class nonequivalent -class abort -class notcompared
|
|
report verification -verbose
|
|
report statistics
|
|
usage
|
|
|
|
exit -force
|