-- Extended locations for iir nodes -- Copyright (C) 2017-2021 Tristan Gingold -- -- This program is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program. If not, see . with Tables; with Vhdl.Nodes_Priv; with Vhdl.Elocations_Meta; use Vhdl.Elocations_Meta; package body Vhdl.Elocations is -- Format of a node. type Format_Type is ( Format_None, Format_L1, Format_L2, Format_L3, Format_L4, Format_L5, Format_L6 ); -- Common fields are: -- Fields of Format_None: -- Fields of Format_L1: -- Field1 : Location_Type -- Fields of Format_L2: -- Field1 : Location_Type -- Field2 : Location_Type -- Fields of Format_L3: -- Field1 : Location_Type -- Field2 : Location_Type -- Field3 : Location_Type -- Fields of Format_L4: -- Field1 : Location_Type -- Field2 : Location_Type -- Field3 : Location_Type -- Field4 : Location_Type -- Fields of Format_L5: -- Field1 : Location_Type -- Field2 : Location_Type -- Field3 : Location_Type -- Field4 : Location_Type -- Field5 : Location_Type -- Fields of Format_L6: -- Field1 : Location_Type -- Field2 : Location_Type -- Field3 : Location_Type -- Field4 : Location_Type -- Field5 : Location_Type -- Field6 : Location_Type function Get_Format (Kind : Iir_Kind) return Format_Type; type Location_Index_Type is new Types.Nat32; No_Location_Index : constant Location_Index_Type := 0; package Elocations_Index_Table is new Tables (Table_Component_Type => Location_Index_Type, Table_Index_Type => Iir, Table_Low_Bound => 2, Table_Initial => 1024); package Elocations_Table is new Tables (Table_Component_Type => Location_Type, Table_Index_Type => Location_Index_Type, Table_Low_Bound => 2, Table_Initial => 1024); procedure Create_Elocations (N : Iir) is use Vhdl.Nodes_Priv; Format : constant Format_Type := Get_Format (Get_Kind (N)); El : constant Iir := Elocations_Index_Table.Last; Len : Location_Index_Type; Idx : Location_Index_Type; begin pragma Assert (Format /= Format_None); if El < N then Elocations_Index_Table.Set_Last (N); Elocations_Index_Table.Table (El + 1 .. N) := (others => No_Location_Index); end if; -- Must be called once. pragma Assert (Elocations_Index_Table.Table (N) = No_Location_Index); case Format is when Format_None => raise Program_Error; when Format_L1 => Len := 1; when Format_L2 => Len := 2; when Format_L3 => Len := 3; when Format_L4 => Len := 4; when Format_L5 => Len := 5; when Format_L6 => Len := 6; end case; Idx := Elocations_Table.Last + 1; Elocations_Index_Table.Table (N) := Idx; Elocations_Table.Set_Last (Idx + Len - 1); Elocations_Table.Table (Idx .. Idx + Len - 1) := (others => No_Location); end Create_Elocations; procedure Delete_Elocations (N : Iir) is use Vhdl.Nodes_Priv; Old : Location_Index_Type; begin -- Cannot delete an already deleted location. if N > Elocations_Index_Table.Last then return; end if; Old := Elocations_Index_Table.Table (N); if Old = No_Location_Index then return; end if; -- Clear the corresponding index. Elocations_Index_Table.Table (N) := No_Location_Index; -- FIXME: keep free slots in chained list ? end Delete_Elocations; procedure Free_Hook (N : Iir) is begin Delete_Elocations (N); end Free_Hook; generic Off : Location_Index_Type; function Get_FieldX (N : Iir) return Location_Type; generic Off : Location_Index_Type; procedure Set_FieldX (N : Iir; Loc : Location_Type); function Get_FieldX (N : Iir) return Location_Type is use Vhdl.Nodes_Priv; Idx : Location_Index_Type; begin pragma Assert (N <= Elocations_Index_Table.Last); Idx := Elocations_Index_Table.Table (N); return Elocations_Table.Table (Idx + Off - 1); end Get_FieldX; procedure Set_FieldX (N : Iir; Loc : Location_Type) is use Vhdl.Nodes_Priv; Idx : Location_Index_Type; begin pragma Assert (N <= Elocations_Index_Table.Last); Idx := Elocations_Index_Table.Table (N); Elocations_Table.Table (Idx + Off - 1) := Loc; end Set_FieldX; function Get_Field1 is new Get_FieldX (1); procedure Set_Field1 is new Set_FieldX (1); function Get_Field2 is new Get_FieldX (2); procedure Set_Field2 is new Set_FieldX (2); function Get_Field3 is new Get_FieldX (3); procedure Set_Field3 is new Set_FieldX (3); function Get_Field4 is new Get_FieldX (4); procedure Set_Field4 is new Set_FieldX (4); function Get_Field5 is new Get_FieldX (5); procedure Set_Field5 is new Set_FieldX (5); function Get_Field6 is new Get_FieldX (6); procedure Set_Field6 is new Set_FieldX (6); -- Subprograms function Get_Format (Kind : Iir_Kind) return Format_Type is begin 
#!/usr/bin/env bash

if [ $# -lt 3 ]; then
    echo "Usage: $0 prefix nextpnr_mode solve_mode"
    exit -1
fi

if grep -q "OSCH" $1.v; then
    echo "$1.v uses blackbox primitive OSCH and cannot be simulated."
    exit -2
fi

case $2 in
    "pack")
        NEXTPNR_MODE="--pack-only"
        ;;
    "place")
        NEXTPNR_MODE="--no-route"
        ;;
    "pnr")
        NEXTPNR_MODE=""
        ;;
    *)
        echo "nextpnr_mode string must be \"pack\", \"place\", or \"pnr\""
        exit -3
        ;;
esac

case $3 in
    "sat")
        SAT=1
        ;;
    "smt")
        SMT=1
        ;;
    *)
        echo "solve_mode string must be \"sat\", or \"smt\""
        exit -4
        ;;
esac

do_sat() {
    ${YOSYS:-yosys} -l ${2}${1}_miter_sat.log -p "read_verilog ${1}.v
                        rename top gold
                        read_verilog ${2}${1}.v
                        rename top gate
                        read_verilog +/machxo2/cells_sim.v

                        miter -equiv -make_assert -flatten gold gate ${2}${1}_miter
                        hierarchy -top ${2}${1}_miter
                        sat -verify -prove-asserts -tempinduct ${2}${1}_miter"
}

do_smt() {
    ${YOSYS:-yosys} -l ${2}${1}_miter_smt.log -p "read_verilog ${1}.v
                        rename top gold
                        read_verilog ${2}${1}.v
                        rename top gate
                        read_verilog +/machxo2/cells_sim.v

                        miter -equiv -make_assert gold gate ${2}${1}_miter
                        hierarchy -top ${2}${1}_miter; proc;
                        opt_clean
                        write_verilog ${2}${1}_miter.v
                        write_smt2 ${2}${1}_miter.smt2"

    yosys-smtbmc -s z3 --dump-vcd ${2}${1}_miter_bmc.vcd ${2}${1}_miter.smt2
    yosys-smtbmc -s z3 -i --dump-vcd ${2}${1}_miter_tmp.vcd ${2}${1}_miter.smt2
}

set -ex

${YOSYS:-yosys} -p "read_verilog ${1}.v
                    synth_machxo2 -noiopad -json ${1}.json"
${NEXTPNR:-../../nextpnr-machxo2} $NEXTPNR_MODE --1200 --package QFN32 --no-iobs --json ${1}.json --write ${2}${1}.json
${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
                    read_json ${2}${1}.json
                    clean -purge
                    write_verilog -noattr -norename ${2}${1}.v"

if [ $3 = "sat" ]; then
    do_sat $1 $2
elif [ $3 = "smt" ]; then
    do_smt $1 $2
fi
generated by cgit v1.2.3 (git 2.25.1) at 2025-12-19 12:37:00 +0000
e Set_Start_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Start_Location (Get_Kind (N)), "no field Start_Location"); Set_Field1 (N, Loc); end Set_Start_Location; function Get_Right_Paren_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Right_Paren_Location (Get_Kind (N)), "no field Right_Paren_Location"); return Get_Field1 (N); end Get_Right_Paren_Location; procedure Set_Right_Paren_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Right_Paren_Location (Get_Kind (N)), "no field Right_Paren_Location"); Set_Field1 (N, Loc); end Set_Right_Paren_Location; function Get_End_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_End_Location (Get_Kind (N)), "no field End_Location"); return Get_Field2 (N); end Get_End_Location; procedure Set_End_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_End_Location (Get_Kind (N)), "no field End_Location"); Set_Field2 (N, Loc); end Set_End_Location; function Get_Is_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Is_Location (Get_Kind (N)), "no field Is_Location"); return Get_Field4 (N); end Get_Is_Location; procedure Set_Is_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Is_Location (Get_Kind (N)), "no field Is_Location"); Set_Field4 (N, Loc); end Set_Is_Location; function Get_Begin_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Begin_Location (Get_Kind (N)), "no field Begin_Location"); return Get_Field3 (N); end Get_Begin_Location; procedure Set_Begin_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Begin_Location (Get_Kind (N)), "no field Begin_Location"); Set_Field3 (N, Loc); end Set_Begin_Location; function Get_Then_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Then_Location (Get_Kind (N)), "no field Then_Location"); return Get_Field3 (N); end Get_Then_Location; procedure Set_Then_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Then_Location (Get_Kind (N)), "no field Then_Location"); Set_Field3 (N, Loc); end Set_Then_Location; function Get_Use_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Use_Location (Get_Kind (N)), "no field Use_Location"); return Get_Field3 (N); end Get_Use_Location; procedure Set_Use_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Use_Location (Get_Kind (N)), "no field Use_Location"); Set_Field3 (N, Loc); end Set_Use_Location; function Get_Loop_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Loop_Location (Get_Kind (N)), "no field Loop_Location"); return Get_Field3 (N); end Get_Loop_Location; procedure Set_Loop_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Loop_Location (Get_Kind (N)), "no field Loop_Location"); Set_Field3 (N, Loc); end Set_Loop_Location; function Get_Generate_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generate_Location (Get_Kind (N)), "no field Generate_Location"); return Get_Field3 (N); end Get_Generate_Location; procedure Set_Generate_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generate_Location (Get_Kind (N)), "no field Generate_Location"); Set_Field3 (N, Loc); end Set_Generate_Location; function Get_Generic_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generic_Location (Get_Kind (N)), "no field Generic_Location"); return Get_Field5 (N); end Get_Generic_Location; procedure Set_Generic_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generic_Location (Get_Kind (N)), "no field Generic_Location"); Set_Field5 (N, Loc); end Set_Generic_Location; function Get_Port_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Port_Location (Get_Kind (N)), "no field Port_Location"); return Get_Field6 (N); end Get_Port_Location; procedure Set_Port_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Port_Location (Get_Kind (N)), "no field Port_Location"); Set_Field6 (N, Loc); end Set_Port_Location; function Get_Generic_Map_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generic_Map_Location (Get_Kind (N)), "no field Generic_Map_Location"); return Get_Field3 (N); end Get_Generic_Map_Location; procedure Set_Generic_Map_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Generic_Map_Location (Get_Kind (N)), "no field Generic_Map_Location"); Set_Field3 (N, Loc); end Set_Generic_Map_Location; function Get_Port_Map_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Port_Map_Location (Get_Kind (N)), "no field Port_Map_Location"); return Get_Field2 (N); end Get_Port_Map_Location; procedure Set_Port_Map_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Port_Map_Location (Get_Kind (N)), "no field Port_Map_Location"); Set_Field2 (N, Loc); end Set_Port_Map_Location; function Get_Arrow_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Arrow_Location (Get_Kind (N)), "no field Arrow_Location"); return Get_Field1 (N); end Get_Arrow_Location; procedure Set_Arrow_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Arrow_Location (Get_Kind (N)), "no field Arrow_Location"); Set_Field1 (N, Loc); end Set_Arrow_Location; function Get_Colon_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Colon_Location (Get_Kind (N)), "no field Colon_Location"); return Get_Field2 (N); end Get_Colon_Location; procedure Set_Colon_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Colon_Location (Get_Kind (N)), "no field Colon_Location"); Set_Field2 (N, Loc); end Set_Colon_Location; function Get_Assign_Location (N : Iir) return Location_Type is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Assign_Location (Get_Kind (N)), "no field Assign_Location"); return Get_Field3 (N); end Get_Assign_Location; procedure Set_Assign_Location (N : Iir; Loc : Location_Type) is begin pragma Assert (N /= Null_Iir); pragma Assert (Has_Assign_Location (Get_Kind (N)), "no field Assign_Location"); Set_Field3 (N, Loc); end Set_Assign_Location; begin Vhdl.Nodes.Register_Free_Hook (Free_Hook'Access); end Vhdl.Elocations;